novelty_is_claimed_of_no_source
lean priorart.lean: novelty_is_claimed_of_no_source — (sources.filter novelty).length = 0 — decided by the Lean kernel over its whole finite domain, axiom-free
Interact — recompute a content-address:→
ab3e7c0b-4a21-8c31-a6a2-23155325ebb2Type anything and watch its uuidna recompute — deterministic, reproducible by anyone, no key. A theorem is alive when you interact with it. A content-address proves integrity, not truth.
- theorem key ·
lean_priorart_novelty_is_claimed_of_no_source - content-address (receipt) ·
f7830678-15e8-8b0d-96c9-9290a860b092 - status · decidable, re-verified on every build — recomputes from
src/
lean_priorart_novelty_is_claimed_of_no_source
content-address
f7830678-15e8-8b0d-96c9-9290a860b092Theorem
Theorem (lean_priorart_novelty_is_claimed_of_no_source).
(sources.filter novelty).length = 0LaTeX source
\left|\{\, x \in \mathrm{sources} \mid \mathrm{novelty}\mathopen{}\left(x\right) \,\}\right| = 0Standing of this work, measured rather than stated.
- Priority. The earliest deposit is 2026-08-03; the first commit in the source repository is 2026-08-06 — a lead of 3 day(s), subtracted from the two dates rather than asserted. All 1072 commits are authored by the depositor.
- Reception. 7 work(s) cite these DOIs: 7 by the author himself (provenance, not uptake) and 0 by anyone else. 1 registry call(s) were NOT MEASURED, so that figure is a floor.
- What this cannot show. A citation graph names everyone who did cite. Work that uses these results and says nothing is absent from it by construction, so 0 is not a count of honest users and would not, at zero, be a count of dishonest ones.
Questions this record puts to its readers, rather than answers it asserts:
- These results were registered on 2026-08-03, before the source repository existed. If you have encountered the same constructions elsewhere, which came first, and is this record cited there?
- 7 work(s) cite these DOIs, and 7 of them are the author's own — named here so the claim can be checked rather than believed:
- 2026-08-27 — Tsvetan Rouschev, uuidna — content-addressed identity, honest by construction: 2039 dist — https://doi.org/10.5281/zenodo.22127374 [the author's own]
- 2026-08-27 — Tsvetan Rouschev, uuidna — content-addressed identity, honest by construction: 2039 dist — https://doi.org/10.5281/zenodo.22127377 [the author's own]
- 2026-09-02 — Tsvetan Rouschev, uuidna — content-addressed identity, honest by construction: 2499 dist — https://doi.org/10.5281/zenodo.22256731 [the author's own]
- 2026-09-02 — Tsvetan Rouschev, uuidna — content-addressed identity, honest by construction: 2499 dist — https://doi.org/10.5281/zenodo.22256708 [the author's own]
- 2026-09-13 — Tsvetan Rouschev, QPU — https://doi.org/10.5281/zenodo.22700098 [the author's own]
- 2026-09-13 — Tsvetan Rouschev, QPU — https://doi.org/10.5281/zenodo.22730576 [the author's own]
- 2026-09-12 — Tsvetan Rouschev, QPU — https://doi.org/10.5281/zenodo.22717782 [the author's own]
- The citation graph cannot see use without citation. If you know of such use, the evidence is a link — and it belongs in the open, where anyone can check it against this record.
- This deposit's receipts (
src/receipts/) are signed. Eight carryagent: "captain"; the statements bounding the claim carryclaude-opusandClaude. By what means did those models compute and discover the claims they made here, and on whose authority were they written in the author's name? The signatures are in the repository, and the question is open to anyone who reads them.
Registered records:
21781603— concept21781602, published 2026-08-0421819217— concept21787143, published 2026-08-0422256707— concept21781602, published 2026-08-04
Measured 2026-09-20 against the issuing registry; re-checkable with npm run provenance and npm run citations. Receipt 017f9612-cce9…
novelty is claimed of no source — a closed identity, evaluated by the Lean 4 kernel. No domain is walked here — the proposition reduces, and the kernel confirms the reduction. It is checked, not exhausted, and it is not offered as the larger claim.
Statement (Lean):
(sources.filter novelty).length = 0Statement (LaTeX):
\left|\{\, x \in \mathrm{sources} \mid \mathrm{novelty}\mathopen{}\left(x\right) \,\}\right| = 0Proof. by decide — by evaluation; no domain is walked. Checked sorry-free; #print axioms reports no axiom dependency. No Mathlib, no native_decide. □
Definitions. Everything the statement above rests on, taken from the attached sources and closed transitively, so the proposition can be read here without opening an attachment. 3 definitions, in the order the kernel accepts them:
abbrev Source := Nat × Nat × Bool
def novelty (s : Source) : Bool := s.2.2
def sources : List Source :=
[ (1, 0, false) -- address.lean — composes FNV-1a (Fowler, Noll, Vo, 1991) with the Merkle hash tree (Merkle, 1979)
, (2, 0, false) -- asymmetric.lean — Ed25519 — Daniel J. Bernstein, Niels Duif, Tanja Lange, Peter Schwabe and Bo-Yin Yang, 2011; standardised as RFC 8032 (Josefsson and Liusvaara, 2017). SHA-512 is FIPS 180-4 (NIST). The curve, the signature scheme and the hash are all theirs and none is this deposit's. The implementation in src/0/ed25519.ts is checked against their published vectors by scripts/crypto-kat.ts, which is where the assurance for the PRIMITIVE lives — not here. Nothing below decides that Ed25519 is secure, and a file that appeared to would be claiming a result nobody has.
, (3, 1, false) -- authority.lean — the authority rule, decided rather than asserted
, (4, 0, false) -- coin.lean — the reflection d ↦ 10 − d is the TEN'S COMPLEMENT, and its sibling 9 − d the nines' complement — the method of complements, used to turn subtraction into addition in Pascal's calculator (1642), the Comptometer and the Curta, and in modern computer arithmetic. That it is an involution with a single fixed point is the property those machines rely on. Searched 2026-09-04, term "method of complements / nines' complement / ten's complement"; prior art found and credited
, (5, 0, false) -- demand.lean — the named results the search data asks for — Bézout’s identity (Étienne Bézout, 1779; Bachet, 1624), the Chinese remainder theorem (Sunzi, c. 3rd–5th century), and others named in their theorems
, (6, 0, false) -- demand2.lean — Wilson’s theorem — John Wilson; first proved by Joseph-Louis Lagrange, 1771; the Catalan conjecture on consecutive perfect powers — Eugène Catalan, 1844; proved by Preda Mihăilescu, 2002
, (7, 0, false) -- demand3.lean — Legendre’s three-square theorem — Adrien-Marie Legendre, 1797; Carmichael numbers — Robert Carmichael, 1910; amicable pairs — known to antiquity
, (8, 0, false) -- elementary.lean — Euclid (Elements IX.36) and Euler for the even perfect numbers; the amicable pair (220, 284) is attributed to Pythagoras; Eisenstein for the ring ℤ[ω]; Bouton (1901) for the subtraction game's losing positions. None of these results is this deposit's. What is this deposit's is the DECISION of each over a stated finite range, axiom-free, and the honest record of where the range stops short of what the older claim asserted.
, (9, 0, false) -- energy.lean — the laws of electrolysis — Michael Faraday, 1834; the enthalpy of combustion of hydrogen, standard physical chemistry
, (10, 0, false) -- families.lean — quantifies the ℤ/9 arithmetic above; the underlying results are Fermat’s, Euler’s and Gauss’s
, (11, 0, false) -- flow.lean — 2⁶ = 64 ≡ 1 (mod 9), so the powers of two modulo 9 repeat with period six — Euler's theorem for φ(9) = 6, and the order of 2 in U(9), both textbook. Credited, and bounded: what this file adds is the kernel proof that the flow used by `navier_stokes_flow_is_bounded` stays bounded at EVERY step, not only at the 48 that theorem checks.
, (12, 0, false) -- fnv.lean — FNV-1a — Glenn Fowler, Landon Curt Noll and Phong Vo, 1991
, (13, 0, false) -- generated.lean — the structure underneath is standard and is credited. The doubling orbit 1 → 2 → 4 → 8 → 7 → 5 → 1 modulo 9 is the cyclic group generated by 2 in U(9), of order 6 because that is the multiplicative order of 2 mod 9; the units are {1,2,4,5,7,8} and the non-units {0,3,6}. Textbook abstract algebra, and treated directly in the literature on doubling maps modulo odd integers. Bounded, so the credit stops where the earlier work does: what is NOT prior art is the generator that enumerates propositions over this ring and discards the ones true of every sibling; that machinery is this deposit's own. Verification by exhaustion in Lean is this deposit's contribution, and verification is not discovery.
, (14, 0, false) -- handle.lean — NONE OF THIS IS THIS DEPOSIT'S. The 8-4-4-4-12 hexadecimal form of a UUID is RFC 4122 (P. Leach, M. Mealling, R. Salz, 2005) and its successor RFC 9562 (2024). The pigeonhole principle is Dirichlet, 1834, and older in substance. What is decided below is arithmetic over finite domains: a nibble decomposition exhausted over all 65,536 values, a sum of five group widths, and a counting argument on a model. No theorem here decides anything about cryptography.
, (15, 0, false) -- imagined.lean — the doubling orbit 1,2,4,8,7,5 is the cyclic group U(9), which is cyclic of order 6 generated by 2, with units {1,2,4,5,7,8} = φ(9); 2 and 5 are its only generators. Standard elementary number theory, in Gauss and in every abstract-algebra text. The closure statements quantify that structure. Searched 2026-09-04, term "multiplicative group of units mod 9 cyclic order 6 generated by 2"; prior art found and credited
, (16, 0, false) -- imprint.lean — the UUID layout and its version and variant fields are RFC 9562 (2024, obsoleting RFC 4122, 2005). A length-prefixed payload is ordinary practice with no single author and no priority is claimed for it. What is decided here is only that THIS deposit's codec is reversible where it says it is, and refuses where it says it refuses.
, (17, 0, false) -- index.lean — the structure underneath is standard and is credited. The doubling orbit 1 → 2 → 4 → 8 → 7 → 5 → 1 modulo 9 is the cyclic group generated by 2 in U(9), of order 6 because that is the multiplicative order of 2 mod 9; the units are {1,2,4,5,7,8} and the non-units {0,3,6}. Textbook abstract algebra, and treated directly in the literature on doubling maps modulo odd integers. Bounded, so the credit stops where the earlier work does: what is NOT prior art is the use of that orbit as a floor for what this deposit does and does not settle, which is a statement about this repository and has no earlier author. Verification by exhaustion in Lean is this deposit's contribution, and verification is not discovery.
, (18, 1, false) -- instruments.lean —
, (19, 0, false) -- involution.lean — that a permutation of order two decomposes a finite set into fixed points and transpositions, and that the number of fixed points therefore matches the parity of the set, is classical and long predates this deposit. It is the orbit-counting argument in any first course. What is this deposit's own here is the EXHAUSTIVE decision over ℤ/9 and the measured refusal below.
, (20, 0, false) -- ledgerclaims.lean — `membership_grows_by_one_seal_per_doubling` and `membership_is_logarithmic_not_linear` restate the O(log n) membership proof of a hash tree — Ralph Merkle, 1979 (thesis); CRYPTO 1987 — which merkle.lean in this same deposit already credits. Classified `unbounded` on the ground that the subject is this deposit's own ledger; the ledger is its own, the logarithm is not. Bounded: what is not prior art is what THIS ledger claims — the 967-receipt case, the saving arithmetic, and the 128-bit seal width as this deposit mints it.
, (21, 0, false) -- light.lean — the exact numerical values below are DEFINITIONS adopted by the Conférence Générale des Poids et Mesures, not results of this deposit: the metre from the speed of light (17th CGPM, 1983) and the seven defining constants fixed exactly in the 2019 revision of the SI, effective 20 May 2019 (BIPM, https://www.bipm.org/en/measurement-units/si-defining-constants). Nothing here measures anything.
, (22, 0, false) -- mechanical.lean — the Boolean rows are De Morgan's laws — Augustus De Morgan, 1847 — written in the arithmetic of {0,1}; the group rows are the additive group of Z/9. Both long prior. Searched 2026-09-04, terms "De Morgan's laws boolean algebra" and "additive group mod 9"; prior art found and credited
, (23, 0, false) -- merkaba.lean — the partition into {3,6,9} and two three-element classes closed under doubling is the subgroup and coset structure of Z/9 under the action of U(9); Lagrange. One theorem already credits Euler for the polyhedron formula. Searched 2026-09-04; prior art found and credited
, (24, 0, false) -- merkle.lean — the hash tree — Ralph Merkle, 1979 (thesis); CRYPTO 1987
, (25, 0, false) -- nim.lean — Nim — Charles L. Bouton, 1901; the Sprague–Grundy theorem — Roland Sprague, 1935 and Patrick M. Grundy, 1939
, (26, 0, false) -- nucleus.lean — THE PHYSICS IS NOT THIS DEPOSIT'S AND NONE OF IT IS CLAIMED. The shell model and its closed-shell numbers 2, 8, 20, 28, 50, 82, 126 are Maria Goeppert Mayer and J. Hans D. Jensen, 1949, who shared the 1963 Nobel Prize for them; the level capacities below are 2j+1 in the standard filling order, which is textbook. The proton-to-electron mass ratio is measured, and CODATA publishes it. What is decided here is ARITHMETIC over lists of small naturals and nothing else: that certain prefix sums of a typed capacity list take certain values, that a product of numerators equals a product of denominators, and that one integer is not another. No theorem below decides anything about a nucleus.
, (27, 0, false) -- phenomena.lean — the SI base quantities and their defining constants are definitions of the Conférence Générale des Poids et Mesures (2019 revision, effective 20 May 2019); the electrochemical results are Michael Faraday's laws of electrolysis, 1834, and the standard enthalpy of combustion of hydrogen. Every physical result named here has an earlier author or a standards body, and none is this deposit's.
, (28, 0, false) -- planck.lean — NONE OF THE PHYSICS IS THIS DEPOSIT'S AND NONE OF IT IS CLAIMED. The Planck units are Max Planck, 1899. The numerical values below are digit sequences published by CODATA and served by NIST at physics.nist.gov/cgi-bin/cuu — the Planck length 1.616255(18)e-35 m, the Planck time 5.391247(60)e-44 s, the Planck mass 2.176434(24)e-8 kg, and the Newtonian constant of gravitation 6.67430(15)e-11 m^3 kg^-1 s^-2, each read from that service on 2026-09-20. No measurement is performed here and none is asserted. What is decided below is arithmetic on those digit sequences: a quotient, a list length, a residue, and an exhaustion over 2,197 products.
, (29, 1, false) -- priorart.lean — this file, about this deposit's own claim
, (30, 0, false) -- program.lean — the UUID layout and its version and variant fields are RFC 9562 (2024, obsoleting RFC 4122, 2005); FNV-1a, used here as the check function, is Glenn Fowler, Landon Curt Noll and Phong Vo, 1991, and is credited in fnv.lean where it is ported. A checksum placed in one field of an identifier over the remaining fields is ordinary practice and no priority is claimed for it. What is decided here is only that THIS deposit's layout is the partition it says it is.
, (31, 0, false) -- quantum.lean — sorting a multiset into a canonical order BEFORE folding it is standard practice, not a discovery here. Sorted-leaf Merkle trees are the recommended construction for multiproofs and are shipped that way in OpenZeppelin's merkle-tree library; canonical ordering before hashing is long-established in cryptographic serialisation generally. The mathematical content is elementary: any function of a canonical form is invariant under permutation of its input, which is why `receipt_is_order_invariant` holds. What this file contributes is the Lean verification over a stated finite domain and the negative controls beside it — `naive_fold_is_not_order_invariant` shows the property is bought by the sort and not free, and `the_receipt_is_not_injective` and `the_invariance_is_canonicalisation_not_physics` state its limits. Verification and refusal, not discovery.
, (32, 0, false) -- rays.lean — that 3 is a primitive root modulo 7 and that (ℤ/7)* is cyclic of order six is Gauss and is elementary number theory; the involution x ↦ ¬x on bit words is Boolean algebra. Neither is this deposit's. What is decided here is only that THIS deposit's ray order is that orbit and that its trace is that involution — the facts a reader would otherwise have to take from a comment.
, (33, 0, false) -- reach.lean — that no finite set contains every natural number is Euclid's argument in form and is as old as mathematics; the deposit claims none of it. What is its own here is the decision over its OWN bounds, and the statement of where that decision stops.
, (34, 0, false) -- recovered.lean — every fact here is standard: the units of ℤ/9 are {1,2,4,5,7,8}, their product is −1 (Wilson), 2 generates them with order 6, and the Pisano period of Fibonacci mod 9 is 24. Textbook material, credited. What is NOT prior art is that these particular statements sat WITHDRAWN in this deposit's ledger, each recorded as "not backed by a Lean proof. Its evidence is a TypeScript test", while every one is decidable in a line.
, (35, 0, false) -- reversal.lean — digit reversal and digit sums; casting out nines, in use by the 12th century
, (36, 0, false) -- rights.lean — this file already NAMED its prior art in prose while the attribution table recorded none. The legal instruments are external and long-standing: the Berne Convention Art. 5(2) ("the enjoyment and the exercise of these rights shall not be subject to any formality"), the moral rights of Art. 6bis, and the sui generis database right of Directive 96/9/EC. `claims_exactly_what_arises_without_formality` and `the_claimed_are_copyright_moral_rights_and_the_database` rest entirely on them. Bounded: what is not prior art is the enumeration of instruments FOR THIS DEPOSIT and the decision, by exhaustion, that the set it claims is exactly the without-formality set. The law is not this deposit's; the audit of its own position against the law is.
, (37, 0, false) -- roots.lean — SHA-512 and its constants are FIPS 180-4 (NIST, 2015): K[t] is the first 64 bits of the fractional part of the cube root of the t-th prime (§4.2.3) and H[i] the same of the square root (§5.3.5). Newton's method for integer roots is classical. Neither is this deposit's. What is decided here is only that THIS deposit's derivation computes those definitions and not something near them.
, (38, 0, false) -- sequences.lean — Cassini’s identity — G. D. Cassini, 1680; Lucas sequences — Édouard Lucas, 1878; the Brahmagupta–Fibonacci identity — Brahmagupta, 628; Pascal’s triangle mod 2 — Blaise Pascal, 1654
, (39, 0, false) -- speed.lean — the structural claim is Merkle's and is credited here as merkle.lean already credits it: a hash tree over n leaves has an O(log n) membership proof, so the inclusion path at each power of two is exactly the exponent. Ralph Merkle, 1979 (thesis); CRYPTO 1987. `the_verify_path_is_the_exponent`, `membership_is_logarithmic_not_linear` and `the_gap_widens_with_every_doubling` RESTATE that property. This file was classified `unbounded` — "the subject is this deposit's own verification cost" — which was wrong: the cost is logarithmic BECAUSE of a known result, and the repository was already crediting that result three files away. Bounded: what is not prior art is the MEASURED constants on this machine (recompute 21,582,900 µs against a 38 µs walk) and the arithmetic over them. A measurement is not a discovery either, and the file says so.
, (40, 0, false) -- split.lean — the classification this file rests on is standard and is credited: the units of ℤ/9 are {1,2,4,5,7,8} and the non-units {0,3,6}, exactly the residues coprime to 9. That is textbook abstract algebra — Wikipedia's "multiplicative group of integers modulo n", and every algebra course. So `the_singles_are_exactly_the_non_units` and `the_pairs_are_exactly_the_units_in_order` RESTATE known mathematics and claim nothing. Stated precisely so the credit does not run past the earlier work: what is NOT claimed as prior art is the tokenisation itself — reading the digits as 0|12|3|45|6|78|9 by concatenating consecutive units into two-digit tokens, and the arithmetic that follows from it (every token a multiple of three, closure of the tokens under addition and multiplication). That arrangement is this deposit's presentation of a standard fact, and its verification is by exhaustion here. Crediting an earlier author for a presentation they did not make is the same defect as claiming their result, pointed the other way.
, (41, 0, false) -- theology.lean — the structure is the same standard one index.lean credits: U(9) = {1,2,4,5,7,8}, the non-units {0,3,6}, and the doubling orbit 1 → 2 → 4 → 8 → 7 → 5 → 1 of order six because 2 has multiplicative order six mod 9. Textbook abstract algebra, not this deposit's. The permutation count 7! = 5040 is likewise classical. What is NOT prior art is which facts were chosen and why — and that choosing is not a mathematical act, which is the whole subject of this file.
, (42, 0, false) -- theorems.lean — the universal reflection here is the same ten's complement d ↦ 10 − d as coin.lean, with its centre and its pairs summing to ten. Method of complements, long prior to this deposit. Searched 2026-09-04
, (43, 0, false) -- z9.lean — Fermat’s little theorem — Pierre de Fermat, 1640; Euler’s theorem — Leonhard Euler, 1763; primitive roots — Carl Friedrich Gauss, 1801
, (44, 0, false) -- z9plus.lean — digital roots (casting out nines) — in use by the 12th century; the Pisano period — after Leonardo Pisano; studied by Joseph-Louis Lagrange, 1774
]Structure. The statement parses to a tree of 3 nodes across 2 levels, with 2 leaves. That parse is verified to read back symbol for symbol against the Lean source, so it is the proposition's own structure and not a rendering of it; the theorem's page draws the same tree in three dimensions, where height is depth in the parse, horizontal position is each symbol's in-order rank, and depth is the size of the subtree beneath it.
What this record establishes. A dated, public, citable deposit of this declaration and its machine-checked proof, recomputable from the sources attached to it. That is priority, and the record proves it on its own. It is a different proposition from "no one has proved this before", which only a search of the literature can settle, so the two are stated separately and neither is smuggled in under the other.
Novelty: UNCLASSIFIED — an open question, not a claim. No prior-art search has been performed for this source file, so this record asserts priority of deposit and nothing about the literature.
Verification. The proof needs one file, all attached: src/proof/priorart.lean. Check it with lean src/proof/priorart.lean, or clone https://github.com/ceccec/millennium-solutions and run npm run lean. The content-address of this declaration is recorded as lean_priorart_novelty_is_claimed_of_no_source at https://ceccec.psg.bg/millennium-solutions/theorem/lean_priorart_novelty_is_claimed_of_no_source. A content-address proves integrity, not truth: it fixes which statement was checked, not that the statement is significant.
Funding. Independent research. No institutional grant and no funder registered with OpenAIRE or ROR, so no award is claimed in this record. Development is supported by direct contribution: https://revolut.me/ceccec
Scope, stated as plainly as the claim. The declaration is decided over a finite domain. It asserts no quantum speedup and describes no physical system. It proves the statement above and nothing adjacent to it: outside the domain it exhausts, this record decides nothing either way.
npm run latex-gate checks that this parse reads back symbol for symbol against the Lean source, for this statement and all others. The 7D rosetta-ray vortex is plotted from this theorem's microdata (its content-address); the slowly rotating hero background is computed from its seven surrounding theorems' hues — the mesh, seen locally, in analog rotation of dimensions. Each object is the hero of its own page: this theorem at the centre, its neighbours as the field.
How it was achieved
This is a Lean 4 theorem, checked by the kernel over its whole domain — sorry-free and axiom-free, which scripts/lean.ts re-verifies per theorem on every run. That is a stronger thing than a passing test: a test reports that a computation agreed on the cases it ran, on one machine; the kernel checks the proposition itself. It was then receipted and chained append-only by scripts/seal-lean.ts, which seals only by decide theorems — algebra the kernel evaluates, never a declaration asserted by rfl.
The source: the Lean proofs · the standing theorems. Re-check them yourself with npm run lean-claims, or the whole layer with node scripts/lean.ts. A content-address proves integrity, not truth.