Prior art — what is restated, what is claimed, and the difference
Of 549 machine-checked declarations, 540 restate work that already has an author and 9 are about this deposit's own construction. Each source file declares which it is, in its own frontmatter; src/proof/priorart.lean holds the same partition as a table the kernel decides over, and the build fails if the two disagree.
What is claimed
Priority, which is evidenced. A dated, content-addressed publication: the DOI fixes the date, the append-only receipt chain fixes which statement was published, and anyone can recompute either. Priority says this was published, in this form, by this date.
Not novelty, which is not. Nothing here can decide that no earlier work states a result — a kernel decides propositions over finite domains, it does not search the literature. noveltyEstablished = 0 is a theorem in priorart.lean for the same reason provenHere = 0 is one: the boundary is checked on every run rather than remembered. No prior art known to the author is a fact about the author. No prior art exists is a fact about the world, and this deposit does not assert it.
The partition, which must be read as three numbers and never as one
| theorems | |
|---|---|
| attributed to named earlier work | 540 |
| unclassified — no search performed, status unknown | 9 |
| claimed as novel | 0 |
Zero claims is not full attribution. Stated alone, "this deposit claims no novelty" reads as a concession that everything here already has an author. It is not that. 9 theorems have had no prior-art search at all, so their status is unknown rather than conceded — and of the 25 distinct years the attributions carry, 23 predate the DOI system (2000); the earliest is 628. "Every theorem has registered prior art" is therefore not merely unproven here, it is impossible. The zero has exactly one meaning: nobody has looked. It is a statement about work not done, not about work found.
zero_claims_is_not_full_attribution decides those two facts together in the kernel, so the count and its caveat cannot be separated by an edit.
A source may claim novelty only if it names a prior-art search that was actually performed — what was searched, where, and when. An earlier version of this page claimed novelty for 1 sources and 9 theorems on the strength of their own self-description, with nobody having looked. Asserting that nothing earlier exists because no one went to check is the same defect as asserting a proof because no one went to read it.
Restated from named earlier work — 29 sources, 540 theorems
No novelty is claimed over any of these. What is done here is to decide each over a stated finite domain, which is a contribution of verification, not of discovery.
| source | theorems | domain | whose work |
|---|---|---|---|
address.lean | 18 | content addressing | composes FNV-1a (Fowler, Noll, Vo, 1991) with the Merkle hash tree (Merkle, 1979) |
coin.lean | 12 | the method of complements | 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 |
demand.lean | 8 | elementary number theory | 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 |
demand2.lean | 8 | elementary number theory, second tier | 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 |
demand3.lean | 7 | elementary number theory, named results | Legendre’s three-square theorem — Adrien-Marie Legendre, 1797; Carmichael numbers — Robert Carmichael, 1910; amicable pairs — known to antiquity |
energy.lean | 18 | electrochemistry and combustion | the laws of electrolysis — Michael Faraday, 1834; the enthalpy of combustion of hydrogen, standard physical chemistry |
families.lean | 12 | modular arithmetic, quantified | quantifies the ℤ/9 arithmetic above; the underlying results are Fermat’s, Euler’s and Gauss’s |
fnv.lean | 13 | non-cryptographic hashing | FNV-1a — Glenn Fowler, Landon Curt Noll and Phong Vo, 1991 |
generated.lean | 14 | elementary number theory — the unit group of ℤ/9 and the doubling orbit | the structure underneath is standard and is credited. The doubling orbit |
imagined.lean | 120 | elementary number theory — the unit group of Z/9 | 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 |
index.lean | 11 | elementary number theory — the unit group of ℤ/9 and the doubling orbit | the structure underneath is standard and is credited. The doubling orbit |
involution.lean | 8 | elementary group theory — orbit decomposition of an order-two permutation | that a permutation of order two decomposes a finite set into fixed points and |
ledgerclaims.lean | 8 | hash trees and membership proofs | `membership_grows_by_one_seal_per_doubling` and `membership_is_logarithmic_not_linear` |
light.lean | 11 | metrology — the International System of Units | the exact numerical values below are DEFINITIONS adopted by the Conférence Générale des |
mechanical.lean | 107 | Boolean algebra and elementary modular arithmetic | 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 |
merkaba.lean | 8 | elementary group theory — subgroups and cosets of Z/9 | 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 |
merkle.lean | 9 | hash trees and membership proofs | the hash tree — Ralph Merkle, 1979 (thesis); CRYPTO 1987 |
nim.lean | 8 | combinatorial game theory | Nim — Charles L. Bouton, 1901; the Sprague–Grundy theorem — Roland Sprague, 1935 and Patrick M. Grundy, 1939 |
phenomena.lean | 4 | metrology and classical physical chemistry | the SI base quantities and their defining constants are definitions of the Conférence |
quantum.lean | 12 | canonical forms and order-invariant commitments | sorting a multiset into a canonical order BEFORE folding it is standard practice, not a |
reach.lean | 5 | elementary set theory — the naturals are not exhausted by any finite list | that no finite set contains every natural number is Euclid's argument in form and is as |
reversal.lean | 9 | elementary arithmetic | digit reversal and digit sums; casting out nines, in use by the 12th century |
rights.lean | 8 | copyright law — rights arising without formality | this file already NAMED its prior art in prose while the attribution table recorded none. |
sequences.lean | 12 | integer sequences and identities | 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 |
speed.lean | 10 | hash trees and membership proofs | the structural claim is Merkle's and is credited here as merkle.lean already credits it: |
split.lean | 19 | elementary number theory — the unit group of ℤ/9 | the classification this file rests on is standard and is credited: the units of ℤ/9 are |
theorems.lean | 8 | the method of complements | 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 |
z9.lean | 21 | modular arithmetic | Fermat’s little theorem — Pierre de Fermat, 1640; Euler’s theorem — Leonhard Euler, 1763; primitive roots — Carl Friedrich Gauss, 1801 |
z9plus.lean | 32 | modular arithmetic and periodicity | digital roots (casting out nines) — in use by the 12th century; the Pisano period — after Leonardo Pisano; studied by Joseph-Louis Lagrange, 1774 |
The domains this touches
- Boolean algebra and elementary modular arithmetic — 107 theorems, in
mechanical.lean - canonical forms and order-invariant commitments — 12 theorems, in
quantum.lean - combinatorial game theory — 8 theorems, in
nim.lean - content addressing — 18 theorems, in
address.lean - copyright law — rights arising without formality — 8 theorems, in
rights.lean - electrochemistry and combustion — 18 theorems, in
energy.lean - elementary arithmetic — 9 theorems, in
reversal.lean - elementary group theory — orbit decomposition of an order-two permutation — 8 theorems, in
involution.lean - elementary group theory — subgroups and cosets of Z/9 — 8 theorems, in
merkaba.lean - elementary number theory — 8 theorems, in
demand.lean - elementary number theory — the unit group of Z/9 — 120 theorems, in
imagined.lean - elementary number theory — the unit group of ℤ/9 — 19 theorems, in
split.lean - elementary number theory — the unit group of ℤ/9 and the doubling orbit — 25 theorems, in
generated.lean,index.lean - elementary number theory, named results — 7 theorems, in
demand3.lean - elementary number theory, second tier — 8 theorems, in
demand2.lean - elementary set theory — the naturals are not exhausted by any finite list — 5 theorems, in
reach.lean - hash trees and membership proofs — 27 theorems, in
ledgerclaims.lean,merkle.lean,speed.lean - integer sequences and identities — 12 theorems, in
sequences.lean - metrology and classical physical chemistry — 4 theorems, in
phenomena.lean - metrology — the International System of Units — 11 theorems, in
light.lean - modular arithmetic — 21 theorems, in
z9.lean - modular arithmetic and periodicity — 32 theorems, in
z9plus.lean - modular arithmetic, quantified — 12 theorems, in
families.lean - non-cryptographic hashing — 13 theorems, in
fnv.lean - the method of complements — 20 theorems, in
coin.lean,theorems.lean
Each is a field with an existing literature, and each is where this deposit's contribution actually sits: not a new result, but an exhaustive machine-checked decision of a known one over a stated finite domain. That is worth saying precisely, because it is both smaller than a discovery claim and more checkable than one.
Author and year are given rather than a resolver identifier. Asserting a DOI for someone else's paper without verifying it would be a fabricated citation, and this is the worst document in the deposit to put one in.
This deposit's own construction — 1 sources, 9 theorems, none claimed
The ℤ/9 vortex framework, its ledger, its receipts, and the enumeration its own generators proposed. These are unclassified: no prior-art search has been performed for them, so nothing is claimed about them either way. They are listed because a reader deserves to know which parts of the deposit are its own construction — not as an assertion that no one has been here before.
To move a source out of this table, add -- prior_art_search: to it naming the search performed; the build refuses a none-known declaration that does not carry one.
| source | theorems | note |
|---|---|---|
priorart.lean | 9 | THE PRACTICE IS PRIOR ART AND IS CREDITED. Recording provenance and attribution per |
Defensive publication
These are decidable mathematical facts, and mathematical methods as such are excluded subject matter under EPC Art. 52(2)(a) — see Rights. Publishing them openly and with a date is defensive publication: it keeps them available to everyone rather than granting anyone a monopoly. That is the purpose of the priority claim above, and it is the whole of it.
Partition seal b93f0448-5b0e-8a0f-99f8-9efe9388a8b5 · recompute with node scripts/priorart.ts · the kernel re-decides priorart.lean on every run. A content-address proves integrity, not truth. entails → 0/7.