Prior art — what is restated, what is claimed, and the difference

Of 26,213 machine-checked declarations, 26,166 restate work that already has an author and 47 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	26,166
unclassified — no search performed, status unknown	47
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. 47 theorems have had no prior-art search at all, so their status is unknown rather than conceded — and of the 41 distinct years the attributions carry, 32 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 7 sources and 47 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 — 118 sources, 26,166 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	33	content addressing by cryptographic hash — SHA-256 digests as immutable identifiers	composes FNV-1a (Fowler, Noll, Vo, 1991) with the Merkle hash tree (Merkle, 1979)
answer.lean	8	primality certificates — a probable prime is not a proved prime (Miller–Rabin, 1976/1980; a proof is a certificate or a deterministic test)	the c2 rules restate that distinction and claim nothing of it; the c1 rules and the gate's own agreement with its rules are this deposit's answer system (src/answer), stated here so the TypeScript can be held to the file.
apis.lean	4	public API directories — the OpenAPI catalogue of APIs.guru	the counts are over the APIs.guru directory (apis.guru), which is the named source; the partition identities are this tree's own arithmetic over its run.
arith.lean	7	elementary number theory — trial division and primality	trial division is the classical method for finding a prime factor (Wikipedia, "Integer factorization"); Fermat's factorization method is a second classical route (Wikipedia, "Fermat's factorization method"). The file's decisions are kernel-checked instances of these; neither method is new here.
asymmetric.lean	11	public-key signatures on elliptic curves	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.
asymmetry.lean	8	the injectivity of a map on a finite set, and the involution; the one-way function of cryptography, whose whole content is that a relation is easy in one direction and not the other.	NONE OF IT IS THIS DEPOSIT'S. An involution is its own inverse by definition, a non-injective map loses information by definition, and "easy forwards, hard backwards" is the premise of public-key cryptography (Diffie–Hellman 1976). What is this deposit's is neither: it is that its own cross formulas are sorted into the two kinds and the difference is decided rather than assumed, on the ring it reasons about.
authority.lean	8	elementary set and order arithmetic over finite lists	NO NOVELTY IS CLAIMED AND NONE IS DENIED. Membership, set difference and monotonicity over finite lists are elementary and older than anyone could name. This row is kind 1 rather than kind 2 because kind 2 asserts a search was performed and found nothing, and none was performed for these. What is this deposit's is not the arithmetic: it is that a rule about WHOSE STATEMENT MAY STAND is decided by the kernel instead of argued inside the gate that applies it.
bridge.lean	8	digit roots (casting out nines) and linear congruential recurrences over Z/n	That 2^n mod 9 cycles with period 6, and that x -> ax+b mod n is the linear congruential map, are both standard. What is stated here is neither: it is that this deposit's OWN cross-subject families, computed in src/entangle, reduce to orbits of the affine maps its own src/proof/group.lean settles — the two halves of the deposit describing one object.
capacity.lean	8	the UUID layout and its version and variant fields — RFC 9562 (2024, obsoleting RFC 4122, 2005), which fixes 4 bits of version and 2 of variant. The birthday bound: a collision among uniformly drawn values from a space of size 2^n is expected near 2^(n/2) draws.	NEITHER IS THIS DEPOSIT'S. RFC 9562 reserves the six bits and the birthday bound is classical probability, older than computing. What is this deposit's is that the CONSEQUENCE of the reservation is decided here rather than left to prose — the capacity and the collision exponent that follow from a count this tree already seals in imprint.lean.
closure.lean	8	Cantor's diagonal argument again, turned on a vocabulary rather than a set; the observation that no finite list of definable predicates over a finite domain exhausts the predicates.	THE METHOD IS CANTOR'S AND THE FINITE CASE IS ELEMENTARY. What is this deposit's is the direction it is pointed: src/proof/diagonal.lean applies it to a diagram somebody else published, and this file applies the identical construction to THIS deposit's own vocabulary, over this deposit's own ring, using the nine properties its own files name. A limit exhibited rather than conceded.
coils.lean	50	extensional equality of predicates over a finite set — that two definitions picking out the same elements are the same subset. Elementary set theory and modular arithmetic.	NOT THIS DEPOSIT'S. "Two descriptions of the same set are equal" is the definition of a set. What is this deposit's is which descriptions in ITS vocabulary turn out to coincide, and that the clustering is derived rather than listed — this file is generated by scripts/coils.ts and hand-editing it would be overwritten.
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
combinatorics.lean	8	standard enumerative combinatorics — the factorial n!, the binomial coefficient C(n,k) with Pascal's rule C(n+1,k+1) = C(n,k+1) + C(n,k) and the symmetry C(n,k) = C(n,n−k), the triangular (handshake) numbers n(n+1)/2, the row sum ∑_k C(n,k) = 2^n, and the two-colour Ramsey number R(2,n) = n. These are textbook (Pascal; Ramsey 1930). Read from qpu.uuidna.com's Combinatorics.lean (~/github/uuidna/qpu), where each is stated as an rfl certificate on a single input, on 2026-11-09 and ported here.	none of this is new and none of it is this deposit's — the laws are the oldest in counting. qpu certifies each value with rfl on one input; what is decided HERE is the same quantities as functions over a range, by exhaustion, each with a control. The honest bound: these are exact enumerative counts — orderings, subsets, handshakes — decided on the classical build device over a finite domain; they are the arithmetic a quantum circuit's amplitudes and gate counts obey, computed, not a physical quantum computer. Deciding C(5,2) = 10 on a CPU reaches no stage of a machine: the structure is carried, the device is not.
counting-rocks.lean	9	undergraduate enumerative combinatorics	Adams, Emmrich, Gillespie, Golden and Pries, "Counting Rocks! An Introduction to Combinatorics" (Colorado State University, May 4 2025), licensed CC BY 4.0 on its copyright page. Each theorem restates a formula or value the book gives, and the kernel decides it over a stated range. None of the results is this deposit's.
demand.lean	11	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	12	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	19	elementary number theory, named results	Legendre’s three-square theorem — Adrien-Marie Legendre, 1797; Carmichael numbers — Robert Carmichael, 1910; amicable pairs — known to antiquity
diagonal.lean	7	Cantor's diagonal argument (1891), in its finite form: no list of subsets of a finite set contains the subset built by disagreeing with the i-th listed subset at the i-th element. Equivalently |2^S| > |S|. Also the counting bound that L binary labels take at most 2^L values.	THE ARGUMENT IS CANTOR'S AND NOTHING HERE IMPROVES IT. It is one of the most cited arguments in mathematics and the finite case is the easy one. What is this deposit's is neither the argument nor its finite case: it is that a specific published ring of labels, drawn three times around three different subjects and captioned "THE ALGEBRA OF EVERYTHING", is put to it by the kernel and the subject it misses is exhibited rather than described.
diamond.lean	1	elementary algebra — involutions on a finite set	r(d) = 10 − d is a reflection of the digits 1..9 about 5, and every reflection x ↦ c − x is an involution (Wikipedia, "Involution (mathematics)"). The claim here is the kernel's decision of it over that finite list; the involution itself is not new.
digits.lean	8	the nines' and tens' complement, the basis of complement subtraction and of the check-digit arithmetic behind casting out nines. Repunits (1, 11, 111, …). Elementary place value.	COMPLEMENT ARITHMETIC IS NOT THIS DEPOSIT'S AND IS OLDER THAN THE DECIMAL POINT. That a number and its digitwise ten's-complement sum to a repunit-times-ten is a consequence of place value that any accountant's method already relies on. What is this deposit's is the accounting below: that the ring's four reflection pairs, written as two-digit numbers, are all congruent to one mod nine, and that zero's exception reappears one place up as an excursion rather than a failure.
dimensions.lean	8	dimensional analysis and the Buckingham π theorem (Buckingham, 1914; the method is older). Planck's construction of natural units from ħ, c and G, 1899. The exponents themselves are in NIST's definitions and in every textbook that derives them.	NOTHING HERE IS NEW AND THE DERIVATION IS THE STANDARD ONE. Solving three linear equations for three exponents is what dimensional analysis IS, and the answers have been known since 1899. What this deposit adds is the quantifier: the textbook SOLVES for the exponents, and this EXHAUSTS every alternative in range and finds exactly one, so "these exponents" becomes "no others".
discount.lean	6	the false-positive rate of a classifier, and the correction of a raw count by a negative control. Signal detection theory; a blank in analytical chemistry; a scrambled-label baseline.	NOT THIS DEPOSIT'S, AND OLD. Subtracting what a control already produces is what a blank is for and has been since titration. What is this deposit's is that the rule is decided by the kernel and sits beside the measurement it governs, so the raw figure cannot be quoted without it.
domain.lean	8	Cantor's diagonal argument, and the elementary fact that a diagonal over a domain of n points separates a list of at most n. Modular reduction 9 ≡ 0 (mod 9) and the tens-complement 10 − d.	THE BOUND IS NOT NEW AND IS NOT CLAIMED. "One point per property" is the counting that makes Cantor work and it is older than any of this. What this deposit adds is which DOMAIN its own structure offers: the sequence it already defines is eleven positions and not nine, and the two extra ones are exactly the fold and the return.
elementary.lean	40	elementary number theory and combinatorial game theory	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.
energy.lean	28	electrochemistry and combustion	the laws of electrolysis — Michael Faraday, 1834; the enthalpy of combustion of hydrogen, standard physical chemistry
entangled.lean	8	siteswap notation for juggling (Klimek, Tiemann and Magnusson, independently c. 1985; the average theorem and the permutation criterion are due to Buhler, Eisenbud, Graham and Wright, 1994); the Pythagorean comma (antiquity); Maekawa's and Kawasaki's theorems on flat-foldable vertices (1980s); the crystallographic restriction theorem (19th century, Bravais and after); the moment of inertia and angular acceleration (Euler, Newton); the least common multiple (Euclid).	NONE OF IT IS THIS DEPOSIT'S, and every result below is older than this file and credited above. What is this deposit's is only the selection and the framing: that each pair named here is not an analogy between a craft and a science but ONE STATEMENT that both of them are, and that the statement is decidable over a finite domain so the claim can be checked rather than admired.
equivalence.lean	8	the equivalence relation and its quotient — reflexivity, symmetry, transitivity, and that a relation with those three properties partitions its set. Leibniz's principle of substitution of identicals. Extensional equality of predicates.	NONE OF IT IS THIS DEPOSIT'S AND ALL OF IT IS FOUNDATIONAL. That an equivalence relation partitions a set is the first theorem anyone proves about equivalence relations. What is this deposit's is that ITS OWN substitution licence — scripts/coils.ts, which tells a reader two formulas may stand for one another — is put to those three properties instead of being assumed to have them.
extension.lean	11	extensional equality of functions over a finite domain; the pigeonhole principle; the fibre of a map. All three are elementary and none is this deposit's.	NOT THIS DEPOSIT'S. That two functions agreeing at every point of a finite domain are the same function is the definition of extensionality; that a map from a larger finite set to a smaller one repeats a value is Dirichlet's pigeonhole. What is this deposit's is only the application: deciding that its OWN cross-formula machinery rests on the first and that its OWN addresses are excluded by the second.
families.lean	63	modular arithmetic, quantified	quantifies the ℤ/9 arithmetic above; the underlying results are Fermat’s, Euler’s and Gauss’s
flow.lean	16	elementary number theory — the multiplicative order of 2 modulo 9	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.
fnv.lean	14	non-cryptographic hashing	FNV-1a — Glenn Fowler, Landon Curt Noll and Phong Vo, 1991
generated.lean	13	elementary number theory — the unit group of ℤ/9 and the doubling orbit	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.
group.lean	8	the one-dimensional affine group AGL(1,n) over Z/n — standard finite group theory	AGL(1,n) has order phi(n)*n, which for n=9 is 6*9=54. Nothing here claims the group is new. What is new is that this deposit's own derived map table is stated as the monoid it is, with the group inside it named, generated to closure, and checked against invertibility.
handle.lean	8	the UUID text format, and the pigeonhole principle	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.
hexbit_route.lean	3	positional notation and the counting of subsets — powers of two	positional notation (Wikipedia, "Positional notation") and the 2^n count of subsets (Wikipedia, "Power set") are classical; the file's decisions are kernel-checked instances of them.
imagined.lean	1000	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
imagined_10.lean	1000	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
imagined_11.lean	1000	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
imagined_12.lean	1000	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
imagined_13.lean	1000	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
imagined_14.lean	1000	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
imagined_15.lean	1000	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
imagined_16.lean	1000	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
imagined_17.lean	1000	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
imagined_18.lean	1000	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
imagined_19.lean	1000	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
imagined_2.lean	1000	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
imagined_20.lean	1000	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
imagined_21.lean	1000	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
imagined_22.lean	1000	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
imagined_23.lean	1000	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
imagined_24.lean	1000	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
imagined_25.lean	742	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
imagined_3.lean	1000	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
imagined_4.lean	1000	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
imagined_5.lean	1000	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
imagined_6.lean	1000	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
imagined_7.lean	1000	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
imagined_8.lean	1000	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
imagined_9.lean	1000	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
imprint.lean	9	identifier formats and length-prefixed encodings	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.
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 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.
instruments.lean	28	elementary order theory, list processing and string matching	NO NOVELTY IS CLAIMED AND NONE IS DENIED. The three rules are elementary — a strict order with an unknown value, a partition of a list at its last marked position, and removal of every occurrence of a substring — and each is standard enough that naming one author would be arbitrary. This row is kind 1 rather than kind 2 because kind 2 asserts that a search was performed and found nothing, and no such search was performed for these. What is this deposit's is not the rules: it is that three of its own instruments hold them by decision of the kernel, instead of by a block of reasoning written inside the instrument that needs them and checked by that same instrument.
interference.lean	2	GHZ states and the X-basis parity witness (Greenberger, Horne, Zeilinger 1989)	the GHZ state, its X-basis parity, and the fact that a classical mixture cannot reproduce it are established physics. This file adds no discovery. It states the mechanism over the three-qubit domain and decides it, so the captain's coin of coin.lean is placed on one side of the line by a theorem and not by prose.
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 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.
ledgerclaims.lean	8	hash trees and membership proofs	`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.
light.lean	17	metrology — the International System of Units	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.
mechanical.lean	127	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	16	hash trees and membership proofs	the hash tree — Ralph Merkle, 1979 (thesis); CRYPTO 1987
mirror.lean	8	an involution on a finite set decomposes into fixed points and transpositions — the cycle structure of an order-2 permutation. The tens-complement d ↦ 10 − d. 2 × 90° = 3 × 60° = 180°.	NONE OF IT IS THIS DEPOSIT'S. That an involution is fixed points plus 2-cycles is the first thing anyone proves about involutions, and the tens-complement is how children subtract. What is this deposit's is the accounting below — which residues pair, which is the centre, and which one the reflection carries out of the ring so that it must fold instead.
nim.lean	28	combinatorial game theory	Nim — Charles L. Bouton, 1901; the Sprague–Grundy theorem — Roland Sprague, 1935 and Patrick M. Grundy, 1939
nucleus.lean	8	the nuclear shell model, and the proton-to-electron mass ratio	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.
pauli_paths.lean	8	the Heisenberg picture and Pauli propagation; the Gottesman–Knill theorem and the stabilizer tableau's conjugation rules, including the CNOT phase rule (Gottesman 1998; Aaronson, Gottesman 2004, "Improved simulation of stabilizer circuits"); the T gate's action T†XT = (X − Y)/√2 and the cost of non-Clifford gates in Pauli-path and stabilizer-rank methods (Bravyi, Gosset 2016).	none of these rules is new. What is decided HERE is each rule src/quantum/paulipath.ts applies, checked against the actual 2×2 and 4×4 matrices over ℤ[ω] — every single-qubit Pauli through H, S, T and T†, every one of the sixteen two-qubit Paulis through CNOT and CZ against the tableau's own bit-and-sign formula — and the cost law: a Clifford gate maps one Pauli to one, T to at most two. The width never appears, because every rule is local to the qubits a gate touches; that is why the engine has no width bound and its bound is the T-count instead.
phenomena.lean	4	metrology and classical physical chemistry	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.
planck.lean	35	the CODATA recommended values, and the SI's 2019 definition of the seven base constants	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.
preimage.lean	8	the second-preimage weakness of unpadded Merkle trees, and the standard remedy of domain separation between leaf and internal hashes (Certificate Transparency, RFC 6962 §2.1, uses 0x00 for leaves and 0x01 for nodes). Also the Kelsey–Schneier style length-extension family.	NOT THIS DEPOSIT'S AND WELL KNOWN. That a Merkle tree without domain separation lets an internal node be presented as a leaf is textbook, and RFC 6962 fixes it with one prefix byte. What is this deposit's is the finding: that ITS OWN fold has the weakness, in a specific shape, and that the shape is decided here rather than asserted.
program.lean	21	identifier formats and error-detecting codes	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.
qec.lean	8	the rotated surface code and its parameters [[2d² − 2d + 1, 1, d]] (Kitaev 1997; Bombín & Martín-Delgado 2007); Shor's nine-qubit code [[9, 1, 3]] as a 3×3 concatenation (Shor 1995); the stabilizer formalism and the order of the n-qubit Pauli group with phases, 2^(2n+2) (Gottesman 1997). Read from qpu.uuidna.com's Surfacecode.lean and Stabilizer.lean (~/github/uuidna/qpu) on 2026-11-08 and ported here.	none of this is new and none of it is this deposit's — the codes are standard and the values are qpu's. qpu states them as rfl certificates on single inputs; what is decided HERE is the same parameters as a FUNCTION of the distance, over a range, by exhaustion, each with a control — and the honest bound that these are the codes' COUNTS, decided over a finite domain, not a physically fault-tolerant device. The ISO audit's fault-tolerance score measures error correction on physical qubits; deciding this arithmetic provides none.
qpu.lean	24	the constants on the left are qpu.uuidna.com's, read from the served JSON-LD on 2026-09-28. They are that service's declarations about its own unit and none of them is this deposit's. The arithmetic relating them is elementary multiplication and powers of two, older than both.	NEITHER SIDE IS BEING CREDITED WITH THE OTHER'S WORK. qpu states faces = coins * rays and bits = vertices * hexbit in its own Lean; this deposit states DIMENSIONS = 2 * N and DIGITS_READ = 4 * N in rays.lean. What is decided here is only WHICH of those land on the same integers, and which do not.
qpu_crypto.lean	16	Fermat's difference-of-squares factorisation (1643); RSA (Rivest, Shamir, Adleman, 1977) on the textbook modulus 91 = 7 · 13 with φ(91) = 72; the classical half of Shor's reduction (1994) — an even period r with a^(r/2) ≢ −1 (mod N) gives the factors gcd(a^(r/2) ± 1, N); Grover's square-root search cost (1996) and the birthday bound; the lifting-the-exponent lemma, v_3(2^n + 1) = v_3(3) + v_3(n) for odd n, and the algebraic split a^3 + 1 = (a + 1)(a^2 − a + 1); Fermat's little theorem as a compositeness witness; RFC 9562's version and variant fields; the 128-quantum-bit floor that qpu.uuidna.com reads from the Classic McEliece ISO page; the order of the general linear group over two elements, |GL(n, 2)| = ∏ (2^n − 2^i); Mersenne primes and the composite 2^11 − 1 = 23 · 89; triangular numbers T(q) = q(q + 1)/2 = C(q + 1, 2); and Zu Chongzhi's rational π = 355/113 (5th century), which qpu's own Grover.lean names as pi_zu.	NONE OF THE MATHEMATICS IS THIS DEPOSIT'S, AND NONE OF IT IS qpu's. qpu.uuidna.com's seal, σ-trapdoor, Shor run and thousand-bit surface are that service's constructions, read from ~/github/uuidna/qpu on 2026-11-08 (src/quantum/uuid/index.ts `version`, `seal`, `uuidQubits`; src/quantum/processing/algorithms.ts `createImpossible`, `decodeImpossible`; src/quantum/CRYPTO.md; the root README.md, committed at d0f1dd01, lines 49–81 for the scale table and the Grover comparison). What is decided here is only which NAMED LAW each construction is, on the same integers, and exactly where each one stops.
qpu_fold.lean	8	FNV-1a (Fowler, Noll, Vo, 1991), a 64-bit non-cryptographic hash; the pigeonhole principle (Dirichlet, 1834); the birthday bound, that a collision among values drawn from a space of size 2^n appears near 2^(n/2) draws; and Grover search (Grover, 1996), whose preimage cost on a space of size N is about √N. qpu's own README states the coin's Grover cost as 2^61 by taking the search space to be the 122-bit layout.	NONE OF THESE IS THIS DEPOSIT'S. FNV-1a, pigeonhole, the birthday bound and Grover are all named prior work. What is this deposit's is the decision — on qpu's own fold, read from ~/github/uuidna/qpu/src/quantum/uuid/index.ts at 4ce19dde6 on 2026-11-09 — that the content UUID is a function of a 64-bit state, so the coins qpu actually emits number at most 2^64, not the 2^122 the layout leaves open; and that the search floor a reader would measure is therefore the fold's width (64), not the layout's (122). The bound is an UPPER bound and needs only the fold's WIDTH: it does not depend on any property of FNV beyond that it produces a 64-bit value, so FNV's permutation is not modelled here. One step of the fold IS transcribed, and checked against the value qpu's code computes, so the width is read from the real function and not assumed.
qpu_gateway.lean	8	quantum teleportation (Bennett, Brassard, Crépeau, Jozsa, Peres, Wootters, Phys. Rev. Lett. 70, 1895, 1993), which sends two classical bits per teleported qubit and proves fewer than two would permit superluminal signalling, so the two bits are random and must be transmitted; and RFC 9562 (2024), which fixes the UUID variant field to the two-bit pattern 10.	NEITHER IS THIS DEPOSIT'S. The teleportation protocol and its two-bit minimum are Bennett et al.'s; the variant field is the RFC's. What is this deposit's is the decision, on qpu's own variant rule read from ~/github/uuidna/qpu/src/quantum/uuid/index.ts at 4ce19dde6 on 2026-11-08, that the two bits qpu calls "gateway" and offers as the carrier of a faster-than-light teleport are CONSTANT across every coin — so they are not the random, transmitted bits the protocol needs, and the analogy's premise fails by computation rather than by prose.
quantum.lean	11	canonical forms and order-invariant commitments	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.
quantum_circuits.lean	8	the CHSH inequality (Clauser, Horne, Shimony, Holt, 1969) and Tsirelson's bound 2√2 (1980); the ring of cyclotomic integers ℤ[ω], ω = e^{iπ/4}, ω⁴ = −1, and √2 = ω − ω³ in it; the native gate set rz, sx, cz of superconducting processors (IBM Quantum's published basis) and the H = RZ·SX·RZ, CX = H·CZ·H identities.	NONE OF THE PHYSICS OR THE ALGEBRA IS THIS DEPOSIT'S. What is decided here is only that the gate list src/quantum/hardware.ts `chshGates` sends — transcribed below gate for gate — prepares a Bell pair and gives the four CHSH correlations ±√2/2, so S = 2√2 for an ideal device, in exact arithmetic with no float anywhere.
quantum_hardware.lean	8	the CHSH inequality (Clauser, Horne, Shimony, Holt, 1969) — no local classical strategy gives |S| > 2 for S = E(a,b) + E(a,b') + E(a',b) − E(a',b'); Tsirelson's bound 2√2 (1980) for quantum strategies; ISO/IEC 4879:2024 §3.4.8 and §3.4.10 (quantum processor, quantum computer) and ISO/IEC 2382:2015 (hardware).	NONE OF THE PHYSICS OR THE INEQUALITY IS THIS DEPOSIT'S. What is decided here is only the integer form of the verdict src/quantum/hardware.ts `chshVerdict` applies to a device's counts, so that the rule a run on IBM Quantum is judged by is the kernel's, not a float comparison.
quantum_models.lean	8	ISO/IEC 4879:2024 — circuit-based §3.4.13 (decided in quantum_circuits.lean), one-way §3.4.14, adiabatic §3.4.15, topological §3.4.16, the quantum annealer §3.4.31 and boson sampling §3.5.8; measurement-based computation and gate teleportation on a cluster state (Raussendorf, Briegel, 2001); Ising anyons, whose braids give the Clifford gates and are not universal alone (Kitaev 2003; Bravyi, Kitaev 2005); the Hong–Ou–Mandel dip (1987) and the permanent as the amplitude of boson sampling (Aaronson, Arkhipov, 2011); the adiabatic theorem's gap condition (Farhi, Goldstone, Gutmann, Sipser, 2000); the frustrated antiferromagnetic triangle.	NONE OF THE PHYSICS IS THIS DEPOSIT'S. Each theorem decides one small, exact instance of a named model in ℤ[ω] (ω = e^{iπ/4}) or in the integers. That is §3.4.22 by definition — a classical program computing what a model's ideal device would — and never evidence that any device computes it.
quantum_octave_124.lean	8	Mermin's inequality for the n-qubit GHZ state (Mermin, 1990; values as restated in arXiv:0905.0151 §2, Eq. 5): quantum 2^(n−1), local hidden-variable maximum 2^(n/2) for even n.	NONE OF THE PHYSICS IS THIS DEPOSIT'S. 124 = 128 − 4 is the UUID's width without its version hex digit. Its Mermin sum over the 125 Pauli-string weights was first computed by src/quantum/hardware.ts; here it is a coin — eight particles of sixteen weights (the last holds 112 … 124), each its own theorem and ledger key, and quantum_uuid_cluster.lean recombines them.
quantum_octave_128.lean	9	Mermin's inequality for the n-qubit GHZ state (Mermin, 1990; values as restated in arXiv:0905.0151 §2, Eq. 5): quantum 2^(n−1), local hidden-variable maximum 2^(n/2) for even n.	NONE OF THE PHYSICS IS THIS DEPOSIT'S. quantum_octaves.lean decides the octaves 2 … 64 whole. At 128 qubits the same sum, over the 129 Pauli-string weights k, does not fit one theorem's default budget, so it is split into eight particles of sixteen weights each — each its own theorem, its own ledger key, its own UUID receipt — and the octave is their sum, rewritten from the eight sealed values rather than recomputed.
quantum_octaves.lean	7	Mermin's inequality for the n-qubit GHZ state (Mermin, 1990): the quantum value 2^(n−1) against the local hidden-variable maximum 2^(n/2) for even n, an exponential violation; the GHZ state (Greenberger, Horne, Zeilinger, 1989); the Pauli operators X and Y and their action on computational basis states.	NONE OF THE PHYSICS IS THIS DEPOSIT'S. What is decided here is Mermin's two numbers, derived exactly at each octave of qubits from 2 to 128 — 128 being the UUID width — from the operators' action and from every classical assignment's phase, so the claim "the quantum lead grows exponentially" is the kernel's at each octave, not a formula.
quantum_software.lean	8	superdense coding (Bennett, Wiesner 1992); the three-qubit bit-flip and phase-flip repetition codes and stabilizer syndrome measurement (Shor 1995; Gottesman 1997); the Toffoli gate and reversible classical computation (Toffoli 1980), with AND not affine over GF(2), which is why CNOT and NOT alone cannot compute it; the swap test (Buhrman, Cleve, Watrous, de Wolf 2001), whose ancilla reads 0 with probability (1 + |⟨ψ|φ⟩|²)/2; and the textbook circuit identities a compiler rewrites with — CNOT = (I⊗H)·CZ·(I⊗H) and SWAP = three alternating CNOTs (Nielsen, Chuang, Quantum Computation and Quantum Information, §4.2–4.3, §10.1).	none of this is new and none of it is this deposit's. What is decided HERE is each idea on exact integer amplitudes — the Hadamard is kept unnormalised (H·H = 2·I), so every equality is between integer vectors and no float or square root stands anywhere — over every input in a stated range, each beside a control that must come out the other way. It is the specification an ideal device meets, §3.4.22 of ISO/IEC 4879 by definition, not a device run.
quantum_textbooks.lean	8	Tsirelson's bound (1980); the single-qubit Clifford group ⟨H, S⟩ of order 24 modulo phase and the Eastin–Knill theorem (2009); the T gate of order 8 and Solovay–Kitaev (1997); Simon's algorithm (1994); Bernstein–Vazirani (1993); Deutsch–Jozsa (1992); Grover's search (1996), certain after one iteration at N = 4; the no-cloning theorem (Wootters, Zurek; Dieks, 1982) and the optimal universal cloner of fidelity 5/6 (Bužek, Hillery, 1996).	NONE OF THE PHYSICS IS THIS DEPOSIT'S, AND THE NUMBERS ARE qpu's. ~/github/uuidna/qpu src/quantum/processing/unit/lean/Qpu/Textbook.lean seals each law's characteristic number as integers — textbook_tsirelson (8 > 4), textbook_eastin_knill (24), textbook_solovay_kitaev (2³ = 8), textbook_simon (2 of 4), textbook_bernstein_vazirani (1 < 3), textbook_deutsch_jozsa (5 > 1), textbook_grover_one_iteration (90°), textbook_no_cloning (5 < 6) — and derives them in its TypeScript (chshValue, cliffordOrder, htUniversality, …). What is decided here is the same number DERIVED in the kernel from the operators themselves, in ℤ[ω] or ℤ, so each of qpu's numbers is cross-verified by an independent route.
quantum_uuid_cluster.lean	8	RFC 9562's UUID layout (a 4-bit version field — one hex digit — and a 2-bit variant field); Mermin's inequality and its odd-n bound 2^((n−1)/2) (arXiv:0905.0151 §2, Eq. 5); the cluster state and its stabilizers K_j = Z_{j−1} X_j Z_{j+1} (Briegel, Raussendorf, 2001); Pauli conjugation by CZ, X_a ↦ X_a Z_b, and the stabilizer tableau (Gottesman–Knill; Aaronson, Gottesman, 2004).	NONE OF THE PHYSICS IS THIS DEPOSIT'S. Every number here was first computed by hand or by src/quantum/hardware.ts this session — 124 = 128 − one hex digit, the 124-qubit Mermin lead, the odd-n bound at 3, 5, 7, 9, the 124-qubit cluster's stabilizers — and in this deposit a fact is a coin or it is nothing, so each is sealed. The tableau is Nat bit masks, which the kernel computes natively, so 124 qubits is 124 · 123 CZ steps.
ranking.lean	8	additive scoring over binary criteria — a weighted sum, the simplest form of multi-criteria decision analysis; and the pigeonhole counting that says a sum over few weights cannot separate many subsets.	NEITHER IS THIS DEPOSIT'S. A weighted sum of indicators is the oldest scoring rule there is, and counting how many subsets share a total is pigeonhole. What is this deposit's is that ITS OWN queue — which decides where the next prior-art search goes — is put to both, and that the second answer is unflattering and recorded anyway.
rays.lean	13	cyclic groups and primitive roots	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.
reach.lean	12	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 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.
reached.lean	80	elementary finite group theory over ℤ/9, and the hue circle of colour theory	NONE OF THE MATHEMATICS IS THIS DEPOSIT'S. That every element of a finite additive group has an inverse, that negation is an involution, that the cosets of a subgroup partition the group, and that the 3-cube has 8 vertices and 12 edges are all textbook and long prior — Lagrange for the cosets, the hypercube counts older still. The RGB/CMY hue relations are ordinary colour theory: complements sit 180° apart on the wheel. What is NOT prior art is that these particular statements sat WITHDRAWN in this deposit's ledger, each marked `portable` — its own judgement that a Lean proof was reachable — and each recorded as "not backed by a Lean proof. Its evidence is a TypeScript test" while nobody wrote one.
recovered.lean	15	elementary number theory — the unit group of ℤ/9	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.
reflection.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
resources.lean	8	D-Wave Chimera and Pegasus annealer qubit counts (vertices·m², vertices·n·m·(m−1)); the quantum Fourier transform's resource counts over q qubits — gate count q(q+1)/2 (a triangular number), swaps ⌊q/2⌋, depth 2q−1, dimension 2^q; and the classical rational convergents of π — Archimedes' 22/7 (upper bound) and Zu Chongzhi's 355/113 (5th century). Read from qpu.uuidna.com's Annealing.lean, Qft.lean and Pi.lean (~/github/uuidna/qpu) on 2026-11-08 and ported here.	none of this is new and none of it is this deposit's. qpu states each as an rfl certificate on a single input; what is decided HERE is the same quantities as functions over a range, by exhaustion, each with a control. The honest bound: these are exact integer counts and exact RATIONAL convergents — not a closed form for π (which is irrational) and not a physical annealer or QFT circuit; the counts are the structure, decided on silicon.
retained.lean	15	elementary number theory — the unit group of Z/9 and the closure of its residue subsets under affine maps	every theorem here is one residue subset of Z/9 carried into itself by one affine map d ↦ a·d + b, an instance of the monoid of 81 maps src/proof/group.lean settles. Standard elementary number theory; nothing here is claimed new.
reversal.lean	29	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. 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.
roots.lean	7	cryptographic hash standards and integer root extraction	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.
separation.lean	8	the separation of points by a family of functions — the notion behind a separating family, a faithful functor, and the Stone–Weierstrass hypothesis. Also elementary cancellation in ℕ.	NEITHER IDEA IS THIS DEPOSIT'S. "A family of maps is worth having when it tells two points apart" is as old as the definition of a separating family, and `x = x + y → y = 0` is cancellation, which predates notation. What is this deposit's is neither: it is that the test is run by the kernel, on a specific ring of labels published on a specific day, with a control that fires.
sequences.lean	28	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	28	hash trees and membership proofs	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
split.lean	22	elementary number theory — the unit group of ℤ/9	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.
synthesis.lean	8	the order of the symplectic group Sp(2n, 2) = 2^(n²)·∏(4^j − 1) and the n-qubit Clifford group (Gottesman 1997; used in randomized benchmarking); Fibonacci- and Ising-anyon fusion-space dimensions in topological quantum computation (Freedman–Kitaev–Larsen–Wang 2003) — the Fibonacci number and 2^(m−1); the [[15, 1, 3]] Reed–Muller magic-state distillation code with cubic error suppression (Bravyi–Kitaev 2005); and QAOA circuit resource counts (Farhi–Goldstone–Gutmann 2014). Read from qpu.uuidna.com's Clifford.lean, Anyon.lean, Magic.lean and Qaoa.lean (~/github/uuidna/qpu) on 2026-11-08 and ported here.	none of this is new and none of it is this deposit's. qpu states each value as an rfl certificate on a single input; what is decided HERE is the same quantities as functions, over a range, by exhaustion, each with a control, and the honest bound that these are exact ABSTRACT group orders and resource counts, decided on the classical build device — not physical quantum gates synthesised or executed on hardware.
t_count_wall.lean	8	the seven-T Toffoli decomposition (Nielsen, Chuang, Quantum Computation and Quantum Information, Fig. 4.9; its T-count of 7 shown optimal by Amy, Maslov, Mosca, Roetteler 2013); the Cuccaro ripple-carry adder of 2n Toffolis (Cuccaro, Draper, Kutin, Moulton 2004); schoolbook modular exponentiation for Shor's algorithm as 2n controlled modular multiplications of n controlled additions each (Vedral, Barenco, Ekert 1996); Beauregard's 2n + 3-qubit circuit (Beauregard 2003); and the Pauli-path cost of non-Clifford gates, at most doubling per T (src/proof/pauli_paths.lean).	none of this is new and none of it is a factoring. What is decided HERE is the COST: the seven-T Toffoli checked exactly against the Toffoli gate in ℤ[ω]; the T-count of one NAMED construction as a function of the bit length n — 28n³, an UNDERCOUNT for that construction because its modular reduction is left out, so the wall it shows is if anything lower than the true one; the Pauli-path worst case 2^T beside it; and the two facts that place the wall. The width is not it — 2n + 3 qubits fit in a handful of UUIDs' particles. The T-count is: at n = 1000 it is 28·10⁹, and the worst-case term bound passes 10⁸⁰ already at n = 3. Better constructions (windowed arithmetic) lower the count by constant factors and keep it polynomial in n, so the bound stays exponential in a polynomial of n. This decides no factoring, claims no quantum speedup, and leaves qpu_crypto.lean's floor exactly where it stands: the deposit does not factor a thousand-bit integer.
theology.lean	8	elementary number theory — the unit group of ℤ/9, the doubling map, and the ten's complement	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.
thousandbit.lean	8	elementary arithmetic of the integer 1000 (its factorisation 2^3·5^3 = 10^3, its residues mod 8 and mod 9), and the register-capacity formula reg(w) = 32w − w − 2 — qpu's uuidQubits, already sealed over the widths [4, 8, 16, 32] in src/proof/width.lean. This file applies that capacity to the one case the sealed width ladder does not reach: a 1000-bit integer (2^1000 − 1), the thousand-bit challenge's own size.	the arithmetic of 1000 is elementary and the capacity formula is qpu's, decided here before. What is new is only the APPLICATION to the 1000-bit case: that it is 125 octaves exactly yet 2^3·5^3 (so the octave is only the 2^3 and the 5^3 is the pentagram cubed), that it carries residue 1 mod 9 (not a whole number of nonets), and that it OVERFLOWS the sealed width ladder — reg(32) = 990 < 1000 ≤ 1021 = reg(33) — filling 97.94% of the minimal register that holds it. These are the answers to "how many octaves" and "what % utilisation", decided as coins rather than computed by hand. The honest bound: register-capacity utilisation of the address column, not a physical quantum computer — get_qc reads isQuantumComputer:false, and no stage of a machine is reached by this arithmetic.
turns.lean	8	the cycle decomposition of a permutation into disjoint cycles; the order of 2 in (ℤ/9)* being 6, which is Euler's theorem for this modulus. The Euler characteristic χ = 2 − 2g of an orientable closed surface of genus g.	NONE OF IT IS THIS DEPOSIT'S. Cycle decomposition is the first structure theorem for permutations, the order of 2 mod 9 is Euler, and χ = 2 − 2g is Euler again. What is this deposit's is the accounting: that doubling leaves exactly TWO non-trivial loops on this ring, that their step angles are 60° and 180°, and that both close at 360° — and theorem 8, which says plainly that the surface is an interpretation of the cycle structure and not a theorem about it.
verdict.lean	8	the classification of a test outcome under partial information — the distinction between a negative result and an absent one, which is ordinary experimental practice and older than statistics. Monotonicity of a decision rule in its evidence.	NEITHER IS THIS DEPOSIT'S. "Absence of evidence is not evidence of absence" is a commonplace, and requiring a decision rule to be total and exclusive is what a classification IS. What is this deposit's is that ITS OWN verdict rule — the one standing behind every novelty claim it makes — is decided by the kernel rather than left as a line of TypeScript nobody checks.
width.lean	8	the UUID 128-bit layout and its version/variant reservation (RFC 9562); qpu.uuidna.com's register formula 32·w − w − 2 and its four hexbit widths 4 / 8 / 16 / 32; the birthday/Grover square-root exponent; the ISO 128-bit post-quantum floor qpu reads from the Classic McEliece ISO page; and the 2^n cost of a classical state-vector over n qubits.	none of this mathematics is new. The register formula and the widths are qpu's; the square root and the ISO floor are standard. What is decided here is only that the floor is a FUNCTION of the width — a dial — so the 128-bit UUID (width 4) sitting 67 bits below it is one instance and a wider identifier clears it; and that the SAME dial is the exponent of the simulation cost, so capacity and the cost of simulating it rise together. The capability gap (quantum speedup) is untouched: a wider register is a bigger classical simulation, never a faster one.
widths.lean	24	the Ed25519 signature scheme's parameter sizes — 32-byte public key, 64-byte signature (Bernstein, Duif, Lange, Schwabe, Yang, 2011; RFC 8032). The 128-bit UUID layout, RFC 9562. A byte is eight bits.	EVERY CONSTANT HERE IS SOMEBODY ELSE'S AND IS CITED ABOVE. Ed25519's sizes are its designers'; the UUID's width is the RFC's; eight bits to a byte is older than both. What is this deposit's is neither: it is that its OWN two files state the same width in different units and had no theorem binding them, so either could have drifted while the other stayed green.
z9.lean	24	modular arithmetic	Fermat’s little theorem — Pierre de Fermat, 1640; Euler’s theorem — Leonhard Euler, 1763; primitive roots — Carl Friedrich Gauss, 1801
z9plus.lean	48	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 — 127 theorems, in mechanical.lean
• Cantor's diagonal argument (1891), in its finite form: no list of subsets of a finite set contains the subset built by disagreeing with the i-th listed subset at the i-th element. Equivalently |2^S| > |S|. Also the counting bound that L binary labels take at most 2^L values. — 7 theorems, in diagonal.lean
• Cantor's diagonal argument again, turned on a vocabulary rather than a set; the observation that no finite list of definable predicates over a finite domain exhausts the predicates. — 8 theorems, in closure.lean
• Cantor's diagonal argument, and the elementary fact that a diagonal over a domain of n points separates a list of at most n. Modular reduction 9 ≡ 0 (mod 9) and the tens-complement 10 − d. — 8 theorems, in domain.lean
• D-Wave Chimera and Pegasus annealer qubit counts (vertices·m², vertices·n·m·(m−1)); the quantum Fourier transform's resource counts over q qubits — gate count q(q+1)/2 (a triangular number), swaps ⌊q/2⌋, depth 2q−1, dimension 2^q; and the classical rational convergents of π — Archimedes' 22/7 (upper bound) and Zu Chongzhi's 355/113 (5th century). Read from qpu.uuidna.com's Annealing.lean, Qft.lean and Pi.lean (~/github/uuidna/qpu) on 2026-11-08 and ported here. — 8 theorems, in resources.lean
• FNV-1a (Fowler, Noll, Vo, 1991), a 64-bit non-cryptographic hash; the pigeonhole principle (Dirichlet, 1834); the birthday bound, that a collision among values drawn from a space of size 2^n appears near 2^(n/2) draws; and Grover search (Grover, 1996), whose preimage cost on a space of size N is about √N. qpu's own README states the coin's Grover cost as 2^61 by taking the search space to be the 122-bit layout. — 8 theorems, in qpu_fold.lean
• Fermat's difference-of-squares factorisation (1643); RSA (Rivest, Shamir, Adleman, 1977) on the textbook modulus 91 = 7 · 13 with φ(91) = 72; the classical half of Shor's reduction (1994) — an even period r with a^(r/2) ≢ −1 (mod N) gives the factors gcd(a^(r/2) ± 1, N); Grover's square-root search cost (1996) and the birthday bound; the lifting-the-exponent lemma, v_3(2^n + 1) = v_3(3) + v_3(n) for odd n, and the algebraic split a^3 + 1 = (a + 1)(a^2 − a + 1); Fermat's little theorem as a compositeness witness; RFC 9562's version and variant fields; the 128-quantum-bit floor that qpu.uuidna.com reads from the Classic McEliece ISO page; the order of the general linear group over two elements, |GL(n, 2)| = ∏ (2^n − 2^i); Mersenne primes and the composite 2^11 − 1 = 23 · 89; triangular numbers T(q) = q(q + 1)/2 = C(q + 1, 2); and Zu Chongzhi's rational π = 355/113 (5th century), which qpu's own Grover.lean names as pi_zu. — 16 theorems, in qpu_crypto.lean
• GHZ states and the X-basis parity witness (Greenberger, Horne, Zeilinger 1989) — 2 theorems, in interference.lean
• ISO/IEC 4879:2024 — circuit-based §3.4.13 (decided in quantum_circuits.lean), one-way §3.4.14, adiabatic §3.4.15, topological §3.4.16, the quantum annealer §3.4.31 and boson sampling §3.5.8; measurement-based computation and gate teleportation on a cluster state (Raussendorf, Briegel, 2001); Ising anyons, whose braids give the Clifford gates and are not universal alone (Kitaev 2003; Bravyi, Kitaev 2005); the Hong–Ou–Mandel dip (1987) and the permanent as the amplitude of boson sampling (Aaronson, Arkhipov, 2011); the adiabatic theorem's gap condition (Farhi, Goldstone, Gutmann, Sipser, 2000); the frustrated antiferromagnetic triangle. — 8 theorems, in quantum_models.lean
• Mermin's inequality for the n-qubit GHZ state (Mermin, 1990): the quantum value 2^(n−1) against the local hidden-variable maximum 2^(n/2) for even n, an exponential violation; the GHZ state (Greenberger, Horne, Zeilinger, 1989); the Pauli operators X and Y and their action on computational basis states. — 7 theorems, in quantum_octaves.lean
• Mermin's inequality for the n-qubit GHZ state (Mermin, 1990; values as restated in arXiv:0905.0151 §2, Eq. 5): quantum 2^(n−1), local hidden-variable maximum 2^(n/2) for even n. — 17 theorems, in quantum_octave_124.lean, quantum_octave_128.lean
• RFC 9562's UUID layout (a 4-bit version field — one hex digit — and a 2-bit variant field); Mermin's inequality and its odd-n bound 2^((n−1)/2) (arXiv:0905.0151 §2, Eq. 5); the cluster state and its stabilizers K_j = Z_{j−1} X_j Z_{j+1} (Briegel, Raussendorf, 2001); Pauli conjugation by CZ, X_a ↦ X_a Z_b, and the stabilizer tableau (Gottesman–Knill; Aaronson, Gottesman, 2004). — 8 theorems, in quantum_uuid_cluster.lean
• Tsirelson's bound (1980); the single-qubit Clifford group ⟨H, S⟩ of order 24 modulo phase and the Eastin–Knill theorem (2009); the T gate of order 8 and Solovay–Kitaev (1997); Simon's algorithm (1994); Bernstein–Vazirani (1993); Deutsch–Jozsa (1992); Grover's search (1996), certain after one iteration at N = 4; the no-cloning theorem (Wootters, Zurek; Dieks, 1982) and the optimal universal cloner of fidelity 5/6 (Bužek, Hillery, 1996). — 8 theorems, in quantum_textbooks.lean
• additive scoring over binary criteria — a weighted sum, the simplest form of multi-criteria decision analysis; and the pigeonhole counting that says a sum over few weights cannot separate many subsets. — 8 theorems, in ranking.lean
• an involution on a finite set decomposes into fixed points and transpositions — the cycle structure of an order-2 permutation. The tens-complement d ↦ 10 − d. 2 × 90° = 3 × 60° = 180°. — 8 theorems, in mirror.lean
• canonical forms and order-invariant commitments — 11 theorems, in quantum.lean
• combinatorial game theory — 28 theorems, in nim.lean
• content addressing by cryptographic hash — SHA-256 digests as immutable identifiers — 33 theorems, in address.lean
• copyright law — rights arising without formality — 8 theorems, in rights.lean
• cryptographic hash standards and integer root extraction — 7 theorems, in roots.lean
• cyclic groups and primitive roots — 13 theorems, in rays.lean
• digit roots (casting out nines) and linear congruential recurrences over Z/n — 8 theorems, in bridge.lean
• dimensional analysis and the Buckingham π theorem (Buckingham, 1914; the method is older). Planck's construction of natural units from ħ, c and G, 1899. The exponents themselves are in NIST's definitions and in every textbook that derives them. — 8 theorems, in dimensions.lean
• electrochemistry and combustion — 28 theorems, in energy.lean
• elementary algebra — involutions on a finite set — 1 theorems, in diamond.lean
• elementary arithmetic — 29 theorems, in reversal.lean
• elementary arithmetic of the integer 1000 (its factorisation 2^3·5^3 = 10^3, its residues mod 8 and mod 9), and the register-capacity formula reg(w) = 32w − w − 2 — qpu's uuidQubits, already sealed over the widths [4, 8, 16, 32] in src/proof/width.lean. This file applies that capacity to the one case the sealed width ladder does not reach: a 1000-bit integer (2^1000 − 1), the thousand-bit challenge's own size. — 8 theorems, in thousandbit.lean
• elementary finite group theory over ℤ/9, and the hue circle of colour theory — 80 theorems, in reached.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 — 11 theorems, in demand.lean
• elementary number theory and combinatorial game theory — 40 theorems, in elementary.lean
• elementary number theory — the multiplicative order of 2 modulo 9 — 16 theorems, in flow.lean
• elementary number theory — the unit group of Z/9 — 24742 theorems, in imagined.lean, imagined_10.lean, imagined_11.lean, imagined_12.lean, imagined_13.lean, imagined_14.lean, imagined_15.lean, imagined_16.lean, imagined_17.lean, imagined_18.lean, imagined_19.lean, imagined_2.lean, imagined_20.lean, imagined_21.lean, imagined_22.lean, imagined_23.lean, imagined_24.lean, imagined_25.lean, imagined_3.lean, imagined_4.lean, imagined_5.lean, imagined_6.lean, imagined_7.lean, imagined_8.lean, imagined_9.lean
• elementary number theory — the unit group of Z/9 and the closure of its residue subsets under affine maps — 15 theorems, in retained.lean
• elementary number theory — the unit group of ℤ/9 — 37 theorems, in recovered.lean, split.lean
• elementary number theory — the unit group of ℤ/9 and the doubling orbit — 24 theorems, in generated.lean, index.lean
• elementary number theory — the unit group of ℤ/9, the doubling map, and the ten's complement — 8 theorems, in theology.lean
• elementary number theory — trial division and primality — 7 theorems, in arith.lean
• elementary number theory, named results — 19 theorems, in demand3.lean
• elementary number theory, second tier — 12 theorems, in demand2.lean
• elementary order theory, list processing and string matching — 28 theorems, in instruments.lean
• elementary set and order arithmetic over finite lists — 8 theorems, in authority.lean
• elementary set theory — the naturals are not exhausted by any finite list — 12 theorems, in reach.lean
• extensional equality of functions over a finite domain; the pigeonhole principle; the fibre of a map. All three are elementary and none is this deposit's. — 11 theorems, in extension.lean
• extensional equality of predicates over a finite set — that two definitions picking out the same elements are the same subset. Elementary set theory and modular arithmetic. — 50 theorems, in coils.lean
• hash trees and membership proofs — 52 theorems, in ledgerclaims.lean, merkle.lean, speed.lean
• identifier formats and error-detecting codes — 21 theorems, in program.lean
• identifier formats and length-prefixed encodings — 9 theorems, in imprint.lean
• integer sequences and identities — 28 theorems, in sequences.lean
• metrology and classical physical chemistry — 4 theorems, in phenomena.lean
• metrology — the International System of Units — 17 theorems, in light.lean
• modular arithmetic — 24 theorems, in z9.lean
• modular arithmetic and periodicity — 48 theorems, in z9plus.lean
• modular arithmetic, quantified — 63 theorems, in families.lean
• non-cryptographic hashing — 14 theorems, in fnv.lean
• positional notation and the counting of subsets — powers of two — 3 theorems, in hexbit_route.lean
• primality certificates — a probable prime is not a proved prime (Miller–Rabin, 1976/1980; a proof is a certificate or a deterministic test) — 8 theorems, in answer.lean
• public API directories — the OpenAPI catalogue of APIs.guru — 4 theorems, in apis.lean
• public-key signatures on elliptic curves — 11 theorems, in asymmetric.lean
• quantum teleportation (Bennett, Brassard, Crépeau, Jozsa, Peres, Wootters, Phys. Rev. Lett. 70, 1895, 1993), which sends two classical bits per teleported qubit and proves fewer than two would permit superluminal signalling, so the two bits are random and must be transmitted; and RFC 9562 (2024), which fixes the UUID variant field to the two-bit pattern 10. — 8 theorems, in qpu_gateway.lean
• siteswap notation for juggling (Klimek, Tiemann and Magnusson, independently c. 1985; the average theorem and the permutation criterion are due to Buhler, Eisenbud, Graham and Wright, 1994); the Pythagorean comma (antiquity); Maekawa's and Kawasaki's theorems on flat-foldable vertices (1980s); the crystallographic restriction theorem (19th century, Bravais and after); the moment of inertia and angular acceleration (Euler, Newton); the least common multiple (Euclid). — 8 theorems, in entangled.lean
• standard enumerative combinatorics — the factorial n!, the binomial coefficient C(n,k) with Pascal's rule C(n+1,k+1) = C(n,k+1) + C(n,k) and the symmetry C(n,k) = C(n,n−k), the triangular (handshake) numbers n(n+1)/2, the row sum ∑_k C(n,k) = 2^n, and the two-colour Ramsey number R(2,n) = n. These are textbook (Pascal; Ramsey 1930). Read from qpu.uuidna.com's Combinatorics.lean (~/github/uuidna/qpu), where each is stated as an rfl certificate on a single input, on 2026-11-09 and ported here. — 8 theorems, in combinatorics.lean
• superdense coding (Bennett, Wiesner 1992); the three-qubit bit-flip and phase-flip repetition codes and stabilizer syndrome measurement (Shor 1995; Gottesman 1997); the Toffoli gate and reversible classical computation (Toffoli 1980), with AND not affine over GF(2), which is why CNOT and NOT alone cannot compute it; the swap test (Buhrman, Cleve, Watrous, de Wolf 2001), whose ancilla reads 0 with probability (1 + |⟨ψ|φ⟩|²)/2; and the textbook circuit identities a compiler rewrites with — CNOT = (I⊗H)·CZ·(I⊗H) and SWAP = three alternating CNOTs (Nielsen, Chuang, Quantum Computation and Quantum Information, §4.2–4.3, §10.1). — 8 theorems, in quantum_software.lean
• the CHSH inequality (Clauser, Horne, Shimony, Holt, 1969) and Tsirelson's bound 2√2 (1980); the ring of cyclotomic integers ℤ[ω], ω = e^{iπ/4}, ω⁴ = −1, and √2 = ω − ω³ in it; the native gate set rz, sx, cz of superconducting processors (IBM Quantum's published basis) and the H = RZ·SX·RZ, CX = H·CZ·H identities. — 8 theorems, in quantum_circuits.lean
• the CHSH inequality (Clauser, Horne, Shimony, Holt, 1969) — no local classical strategy gives |S| > 2 for S = E(a,b) + E(a,b') + E(a',b) − E(a',b'); Tsirelson's bound 2√2 (1980) for quantum strategies; ISO/IEC 4879:2024 §3.4.8 and §3.4.10 (quantum processor, quantum computer) and ISO/IEC 2382:2015 (hardware). — 8 theorems, in quantum_hardware.lean
• the CODATA recommended values, and the SI's 2019 definition of the seven base constants — 35 theorems, in planck.lean
• the Ed25519 signature scheme's parameter sizes — 32-byte public key, 64-byte signature (Bernstein, Duif, Lange, Schwabe, Yang, 2011; RFC 8032). The 128-bit UUID layout, RFC 9562. A byte is eight bits. — 24 theorems, in widths.lean
• the Heisenberg picture and Pauli propagation; the Gottesman–Knill theorem and the stabilizer tableau's conjugation rules, including the CNOT phase rule (Gottesman 1998; Aaronson, Gottesman 2004, "Improved simulation of stabilizer circuits"); the T gate's action T†XT = (X − Y)/√2 and the cost of non-Clifford gates in Pauli-path and stabilizer-rank methods (Bravyi, Gosset 2016). — 8 theorems, in pauli_paths.lean
• the UUID 128-bit layout and its version/variant reservation (RFC 9562); qpu.uuidna.com's register formula 32·w − w − 2 and its four hexbit widths 4 / 8 / 16 / 32; the birthday/Grover square-root exponent; the ISO 128-bit post-quantum floor qpu reads from the Classic McEliece ISO page; and the 2^n cost of a classical state-vector over n qubits. — 8 theorems, in width.lean
• the UUID layout and its version and variant fields — RFC 9562 (2024, obsoleting RFC 4122, 2005), which fixes 4 bits of version and 2 of variant. The birthday bound: a collision among uniformly drawn values from a space of size 2^n is expected near 2^(n/2) draws. — 8 theorems, in capacity.lean
• the UUID text format, and the pigeonhole principle — 8 theorems, in handle.lean
• the classification of a test outcome under partial information — the distinction between a negative result and an absent one, which is ordinary experimental practice and older than statistics. Monotonicity of a decision rule in its evidence. — 8 theorems, in verdict.lean
• the constants on the left are qpu.uuidna.com's, read from the served JSON-LD on 2026-09-28. They are that service's declarations about its own unit and none of them is this deposit's. The arithmetic relating them is elementary multiplication and powers of two, older than both. — 24 theorems, in qpu.lean
• the cycle decomposition of a permutation into disjoint cycles; the order of 2 in (ℤ/9) being 6, which is Euler's theorem for this modulus. The Euler characteristic χ = 2 − 2g of an orientable closed surface of genus g.* — 8 theorems, in turns.lean
• the equivalence relation and its quotient — reflexivity, symmetry, transitivity, and that a relation with those three properties partitions its set. Leibniz's principle of substitution of identicals. Extensional equality of predicates. — 8 theorems, in equivalence.lean
• the false-positive rate of a classifier, and the correction of a raw count by a negative control. Signal detection theory; a blank in analytical chemistry; a scrambled-label baseline. — 6 theorems, in discount.lean
• the injectivity of a map on a finite set, and the involution; the one-way function of cryptography, whose whole content is that a relation is easy in one direction and not the other. — 8 theorems, in asymmetry.lean
• the method of complements — 20 theorems, in coin.lean, reflection.lean
• the nines' and tens' complement, the basis of complement subtraction and of the check-digit arithmetic behind casting out nines. Repunits (1, 11, 111, …). Elementary place value. — 8 theorems, in digits.lean
• the nuclear shell model, and the proton-to-electron mass ratio — 8 theorems, in nucleus.lean
• the one-dimensional affine group AGL(1,n) over Z/n — standard finite group theory — 8 theorems, in group.lean
• the order of the symplectic group Sp(2n, 2) = 2^(n²)·∏(4^j − 1) and the n-qubit Clifford group (Gottesman 1997; used in randomized benchmarking); Fibonacci- and Ising-anyon fusion-space dimensions in topological quantum computation (Freedman–Kitaev–Larsen–Wang 2003) — the Fibonacci number and 2^(m−1); the [[15, 1, 3]] Reed–Muller magic-state distillation code with cubic error suppression (Bravyi–Kitaev 2005); and QAOA circuit resource counts (Farhi–Goldstone–Gutmann 2014). Read from qpu.uuidna.com's Clifford.lean, Anyon.lean, Magic.lean and Qaoa.lean (~/github/uuidna/qpu) on 2026-11-08 and ported here. — 8 theorems, in synthesis.lean
• the rotated surface code and its parameters [[2d² − 2d + 1, 1, d]] (Kitaev 1997; Bombín & Martín-Delgado 2007); Shor's nine-qubit code [[9, 1, 3]] as a 3×3 concatenation (Shor 1995); the stabilizer formalism and the order of the n-qubit Pauli group with phases, 2^(2n+2) (Gottesman 1997). Read from qpu.uuidna.com's Surfacecode.lean and Stabilizer.lean (~/github/uuidna/qpu) on 2026-11-08 and ported here. — 8 theorems, in qec.lean
• the second-preimage weakness of unpadded Merkle trees, and the standard remedy of domain separation between leaf and internal hashes (Certificate Transparency, RFC 6962 §2.1, uses 0x00 for leaves and 0x01 for nodes). Also the Kelsey–Schneier style length-extension family. — 8 theorems, in preimage.lean
• the separation of points by a family of functions — the notion behind a separating family, a faithful functor, and the Stone–Weierstrass hypothesis. Also elementary cancellation in ℕ. — 8 theorems, in separation.lean
• the seven-T Toffoli decomposition (Nielsen, Chuang, Quantum Computation and Quantum Information, Fig. 4.9; its T-count of 7 shown optimal by Amy, Maslov, Mosca, Roetteler 2013); the Cuccaro ripple-carry adder of 2n Toffolis (Cuccaro, Draper, Kutin, Moulton 2004); schoolbook modular exponentiation for Shor's algorithm as 2n controlled modular multiplications of n controlled additions each (Vedral, Barenco, Ekert 1996); Beauregard's 2n + 3-qubit circuit (Beauregard 2003); and the Pauli-path cost of non-Clifford gates, at most doubling per T (src/proof/pauli_paths.lean). — 8 theorems, in t_count_wall.lean
• undergraduate enumerative combinatorics — 9 theorems, in counting-rocks.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 — 7 sources, 47 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
answer_gate.lean	7	—
answer_route.lean	6	—
cern.lean	9	—
lanes.lean	8	NONE OF THE ARITHMETIC IS THIS DEPOSIT'S. min, ⌊a/b⌋ and truncating subtraction on the naturals are older than anyone could name. What is this deposit's is not the arithmetic: it is that the rule deciding how much of a machine a verification may take is DECIDED by the kernel rather than trusted because it has not yet swapped.
leads.lean	0	—
priorart.lean	9	THE PRACTICE IS PRIOR ART AND IS CREDITED. Recording provenance and attribution per artefact is long established and formalised: W3C PROV-O, the DataCite metadata schema, Dublin Core Metadata Terms, PREMIS for archived digital objects, the Open Provenance Model, and the software citation principles' credit-and-attribution requirement. Nothing about keeping an attribution table is new, and this deposit does not suggest otherwise.
settled.lean	8	THE ARITHMETIC IS NAMED, NOT CLAIMED. What is this deposit's is only the subject: that these particular files' self-declared counts agree with their own contents. The statement is about this tree and asserts nothing about anybody else's work.

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 92adfd64-f890-8db3-a180-8974830ab42b · recompute with node scripts/priorart.ts · the kernel re-decides priorart.lean on every run. A content-address proves integrity, not truth.