recomputable proof of concept — the figure is the math, drawn live (not a video)
Millennium Solutions — the ℤ/9 Vortex Framework
Author: Tsvetan Rouschev · License: CC BY-NC-ND 4.0 · DOI 10.5281/zenodo.21819217
npm install @ceccec/millennium-solutionsimport { toUuid, merkleFold } from '@ceccec/millennium-solutions'
const a = toUuid('hello') // the same input gives the same address, for anyone, with no key
const root = merkleFold([a, toUuid('world')]) // many addresses fold into one
console.log(a, root)An ES module with TypeScript types for Node 22.12 or later; import and require both work.
Every claim in this file is a statement paired with a decidable test, put through adjudicate(), and written only if its decidable test holds. It is generated by scripts/pages.ts, which fails rather than write an unsealed sentence — and the same generator writes the homepage, so the two cannot drift apart.
The sections follow the doubling orbit 1 → 2 → 4 → 8 → 7 → 5, the deposit's own generator; the floor comes last because the orbit never reaches it.
1 · What is proved
- The formal layer holds 984 kernel-accepted declarations across 44 files, and no file uses sorry or native_decide outside a comment. SEALED ·
e2937d6f-b578-8133-90aa-64f6548f8e34 - 782 of those 984 are THEOREMS by this deposit's own rule — they close by decide, which is to say the kernel evaluates the proposition over its whole finite domain rather than accepting a declaration; the remaining 202 close by rfl and are declarations. SEALED ·
97fe4301-84e4-8d59-bbea-bb0c07dcd005 - 1061 of them are sealed into the ledger, each carrying a receipt derived from the one before it. SEALED ·
505475ab-ec77-85c6-9105-afda93b42a54
2 · The ring
- The units are the 6 residues coprime to nine, the doubling orbit visits 1, 2, 4, 8, 7, 5 and closes on the seventh step, and it never lands on the triad. SEALED ·
52efa15a-c0ba-851e-97a7-2cbb72a9d257 - The reflection ten-minus-d carries 1, 4, 7 onto 9, 6, 3, so it covers the whole triad the orbit never reaches — the units and the triad are mirror images rather than separate populations. SEALED ·
af5b49c7-7c9e-83c4-9fed-3441236d9c76
4 · Entanglement
- Doubling alone reaches only the units and reflection alone only two residues, but together they grow 1, 3, 5, 7, 9 from the single seed one, reaching every residue on round 4. SEALED ·
67b99093-1ec7-8487-a06e-8b10513d8181
8 · Addressing
- The content-address is ported to the formal layer in fnv.lean, address.lean, merkle.lean — 55 theorems covering FNV-1a, the four seeded passes, the version and variant nibbles, and the fold, each agreeing with the shipped implementation at published values. SEALED ·
3bf5bc86-48a0-83f7-ad13-ede54ffef0b2 - The fold does not depend on the order its leaves arrive in, and that is not vacuous because merge itself is proved order-sensitive — the sort is what removes the dependence. SEALED ·
7ee1de7d-d218-88d4-8dc9-6eec451ced72
7 · The ledger
- The ledger records 2925 entries with 0 chain breaks, 0 duplicate keys and 0 duplicate receipts. SEALED ·
ac00aeae-fe6f-8712-8d96-bd1cedce0153 - The count is 2925, which is 365 octaves and 5 over — the octave is a target the theorems earn, never a quota they are invented to fill. SEALED ·
598ad522-bf64-8c05-87e7-766072f5e1b1
5 · What the gate does and does not do
- The gate is 1 lines of local logic — it re-exports the package implementation, which asks one recomputable question: does every theorem a claim cites exist, sealed, in the ledger. SEALED ·
37ab7769-a1ac-8ef6-9809-e214d6285057 - The gate does not decide whether a statement is true: "two plus two equals five" passes it, so holding means not drained, never correct. SEALED ·
f63cc6c5-44f9-8d92-afa7-ab9483573b28 - The tools are reachable from a program: 21 of them over 2 transport(s) — JSON-RPC on stdio for a model client, and the same surface over HTTP for a browser — of which 4 write to this tree and are refused unless the server is started with --allow-write. SEALED ·
e15edd81-96c8-81fa-8c15-b971c7cb49e5 - The stdio server advertises 2 of those 21 and reaches the rest through call_tool, because a model client pays for every tool description on every turn; the HTTP server lists them all, because a browser pays nothing for a list and cannot guess what it was not shown. SEALED ·
fd43fc14-9388-8bd2-ae57-e99b1c5c1b8e
The floor
- The ten digits read in order group as 0 | 12 | 3 | 45 | 6 | 78 | 9 — the singles 0,3,6,9 are exactly the non-units of ℤ/9 with the void, the pairs are the units in consecutive order, and every token is a multiple of 3. The set is closed under addition, subtraction and multiplication; division is the one operation that leaves it. SEALED ·
da5176d1-3e25-8421-81be-ddbcd34d988c - The fair-exchange unit is 2 coins, and deducting them from a token's multiplier deducts 6 from the token: 0, 12, 6, 78 reach the void by repeated payment and 3, 45, 9 halt on 3, the generator the coin cannot spend. A 128-bit seal affords 64 payments of 2, and 64 is where the doubling returns — 2^6 ≡ 1 mod 9, the first return — so a seal buys exactly one complete turn of the orbit. SEALED ·
97eba519-a1b0-85da-a316-3a5050c59281 - Verifying one receipt against a fold of 1048576 leaves walks 20 nodes rather than 1048576: 21582900 µs to recompute against 38 µs to verify, a ratio of 567971×, and the ratio widens at every doubling because the path is log₂ of the leaf count while the recomputation is the count itself. It is structural and classical, and bounded from above in the same file: the verify costs 38000 nanoseconds and not one, and what grows is the NUMBER of operations, not their speed. SEALED ·
a998f6d9-4ce5-8428-a988-c844b13abda8
Every one of the 14 registered claims above recomputes from the artefact it names.
5 · What the kernel decided the most of
Ranked by the size of the domain each theorem was decided over — the count of cases by decide actually walked, computed from the statements themselves. Nothing is chosen for this table.
| cases decided | theorem | file |
|---|---|---|
| 152,568,360,000 | bezouts_identity_is_attained_and_no_smaller_combination_exists | demand2.lean |
| 4,294,967,296 | the_nim_sum_is_a_gf2_vector_addition | nim.lean |
| 7,529,536 | gravity_holds_prose_code_and_paths | mechanical.lean |
| 96,000 | the_area_of_an_integer_right_triangle_is_a_multiple_of_six | elementary.lean |
| 95,048 | two_twenty_and_two_eighty_four_are_the_smallest_amicable_pair | demand2.lean |
| 80,000 | the_wythoff_sequences_partition_the_integers | elementary.lean |
| 65,536 | the_four_hex_field_round_trips_over_its_whole_space | handle.lean |
| 46,656 | the_powers_of_two_mod_nine_and_of_three_mod_seven_are_isomorphic | elementary.lean |
The largest domain settled here is 152,568,360,000 cases, and it is finite — as every entry in this ledger is, because by decide works by exhausting a domain and an infinite one cannot be exhausted. Each of the seven Clay conjectures ranges over an infinite domain. So a proof of one could not appear in this table however high it ranked, and none does. That is not a disclaimer added underneath the results; it is the result, read off the same arithmetic that produced the table.
7 · The proofs, as they document themselves
44 Lean files in 7 wings, 984 declarations of which 969 are theorems. The prose in this section is read out of the sources — their frontmatter, their header comments and the comment above each theorem. Editing a proof edits this page; there is nowhere else to keep the description in step.
the address
Addressing — address.lean, 26 theorem(s). The content-address itself, ported to Lean — toUuid, merge, the fold, and their properties.
What a signature is for, and where it cannot go — asymmetric.lean, 12 theorem(s). 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.
FNV-1a, the address function — fnv.lean, 15 theorem(s). FNV-1a, ported to Lean — the hash the whole deposit's addressing rests on.
The imprint — a uuid that carries a message and gives it back — imprint.lean, 10 theorem(s). 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.
What the ledger claims — ledgerclaims.lean, 8 theorem(s). 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. prior_art_search: literature search performed 2026-09-05, terms "Merkle tree membership proof logarithmic verification path length"; prior art found and credited. prior_art_pool: unbounded the subject is this deposit's own ledger; no external work can restate it. BOUNDED means a search is well posed and simply has not been run — the row is unclassified because nobody looked. UNBOUNDED means the subject is this artifact, so there is no pool to search and the row will stay unclassified however much work is done. They look identical in a count and need opposite responses, which is the distinction uuidna-49 asked for and nobody had drawn. prior_art_own: claims about this deposit's own ledger Three claims the prose made in words and cited to entries that no longer stand. Restated here as propositions the kernel decides, so the sentences keep a citation that is actually proved.
The fold — merkle.lean, 14 theorem(s). The fold, ported to Lean — merge, merkleFold, and the order-independence the deposit calls its receipt.
The uuid as a container — a checksum, a program, and a message — program.lean, 22 theorem(s). 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.
The rays, read forward and reverse, and the mark a life carries — rays.lean, 14 theorem(s). 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.
the floor
Who may speak, decided — authority.lean, 8 theorem(s). 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. prior_art_own: the authority rule, decided rather than asserted
What is actually being asked for — demand.lean, 11 theorem(s). THE ONE WING THAT DID NOT COME FROM THIS DEPOSIT'S OWN INTERESTS. Every other file here proves what the ℤ/9 construction led to. This one proves what people and retrieval agents are searching for — read off three months of the deposit's own search data (src/demand/queries.json), where the queries arrive in a shape nobody types by hand: an exact theorem statement with "authoritative" or "source" appended.
The next tier of what is asked for — demand2.lean, 12 theorem(s). THE SECOND COURSE OF THE SAME FLOOR. demand.lean closed the top eight topics in src/demand/queries.json; this file takes the next eight, chosen the same way — by impressions, not by taste. The demand map is three months of the deposit's own Google Search Console data with the retrieval scaffolding stripped, so what is ranked is the TOPIC people wanted a citable source for, not the phrasing they reached for.
The named theorems people ask for — demand3.lean, 19 theorem(s). The third and last tier the search data supports. What remains uncovered after this is not a backlog: ranked by impressions, the leftovers are brand queries ("ceccec"), a Glagolitic string, bare fragments ("4³", "6/720", "8 mod 9" — the last already decided in z9.lean), and the real-analysis cluster that was refused in demand2.lean and stays refused. The demand map is close to exhausted of things a kernel can settle, which is a better place to stop than an arbitrary count would have been.
The water loop — energy.lean, 28 theorem(s). THE WATER LOOP, ACCOUNTED. Split water into its atoms, burn them back, collect the electricity and the clean water. Every step of that is real and buildable. The question is only ever the ledger, so here it is.
Four hex, exactly computed — and what the handle has to carry instead — handle.lean, 8 theorem(s). argument on a model. No theorem here decides anything about cryptography. prior_art_search: not performed — the sources are named above rather than searched for. prior_art_pool: bounded prior_art_own: nothing; this file exists to put a bound under a construction, not to invent one
The Millennium floor — index.lean, 11 theorem(s). 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. prior_art_search: literature search performed 2026-09-05, terms "doubling sequence modulo 9 orbit 1 2 4 8 7 5 cyclic group generator digital root"; prior art found and credited. prior_art_pool: bounded digit arithmetic of the doubling sequence; searchable independently of this deposit. BOUNDED means a search is well posed and simply has not been run — the row is unclassified because nobody looked. UNBOUNDED means the subject is this artifact, so there is no pool to search and the row will stay unclassified however much work is done. They look identical in a count and need opposite responses, which is the distinction uuidna-49 asked for and nobody had drawn. prior_art_own: the Millennium floor, computed from this sequence The Millennium floor — seven honest theorems, one per problem, COMPUTED from the sequence.
The instruments, and the three rules they are allowed to have — instruments.lean, 29 theorem(s). 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.
Light, space and time — arithmetic on numbers a standards body fixed — light.lean, 17 theorem(s). 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.
The three facts the unchecked files held alone — nucleus.lean, 8 theorem(s). 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. prior_art_search: not performed for these rows — the sources are named above rather than searched for, which is kind 1 and not kind 2. Nothing here claims a search returned nothing. prior_art_pool: bounded prior_art_own: nothing; this file exists to bring three facts under the kernel, not to find them
Every phenomenon this deposit touches, and the rule for the rest — phenomena.lean, 4 theorem(s). 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.
The Planck length, and what a lattice may say about it — planck.lean, 27 theorem(s). 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. prior_art_search: not performed — the source is named above rather than searched for. Nothing here claims a search of the literature returned nothing. prior_art_pool: bounded prior_art_own: nothing about nature; the one thing this file contributes is the REFUSAL below, decided
Order-invariance — quantum.lean, 12 theorem(s). 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. prior_art_search: literature search performed 2026-09-05, terms "sorted Merkle tree order-invariant set commitment canonical ordering leaves"; prior art found and credited. This file was unclassified — no search had ever been run for it — and it is one of the 8 files whose 86 theorems are staged for DOIs. prior_art_pool: mixed canonicalisation before folding is a searchable technique; the receipt it folds is ours. BOUNDED means a search is well posed and simply has not been run — the row is unclassified because nobody looked. UNBOUNDED means the subject is this artifact, so there is no pool to search and the row will stay unclassified however much work is done. They look identical in a count and need opposite responses, which is the distinction uuidna-49 asked for and nobody had drawn. prior_art_own: order-invariance of this deposit's receipt The quantum receipt — order invariance, proved rather than asserted.
What exhaustion reaches, and what lies outside it — reach.lean, 12 theorem(s). 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.
The constants, derived from what they are — roots.lean, 8 theorem(s). 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.
Why verification is fast, and what it is not — speed.lean, 12 theorem(s). wrong: the cost is logarithmic BECAUSE of a known result, and the repository was already crediting that result three files away. Bounded: what is not prior art is the MEASURED constants on this machine (recompute 21,582,900 µs against a 38 µs walk) and the arithmetic over them. A measurement is not a discovery either, and the file says so. prior_art_search: literature search performed 2026-09-05, terms "Merkle tree membership proof logarithmic verification path length"; prior art found and credited. prior_art_pool: unbounded the subject is this deposit's own verification cost. BOUNDED means a search is well posed and simply has not been run — the row is unclassified because nobody looked. UNBOUNDED means the subject is this artifact, so there is no pool to search and the row will stay unclassified however much work is done. They look identical in a count and need opposite responses, which is the distinction uuidna-49 asked for and nobody had drawn. prior_art_own: this deposit's own verification cost
The readings, and the arithmetic under them — theology.lean, 8 theorem(s). choosing is not a mathematical act, which is the whole subject of this file. prior_art_search: literature search performed 2026-09-05, terms "doubling sequence modulo 9 orbit 1 2 4 8 7 5 cyclic group generator digital root"; prior art found and credited. prior_art_pool: bounded digit arithmetic of the doubling sequence; searchable independently of this deposit. prior_art_own: the pairing, and the refusal to let it carry weight
the ring
The two-sided coin — coin.lean, 12 theorem(s). One involution on ten digits, two sides, one fixed point, and one digit that leaves.
Elementary arithmetic — elementary.lean, 41 theorem(s). 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. prior_art_search: the results are named in every undergraduate text; no search was needed to find them. prior_art_pool: named Elementary arithmetic, decided — the claims the ledger held in TypeScript, given a kernel.
Families over the ring — families.lean, 64 theorem(s). The families, quantified. Proving at scale.
The doubling flow, for every step — flow.lean, 16 theorem(s). prior_art_search: literature search performed 2026-09-14, terms "powers of two modulo 9 period 6 order of 2 mod 9 Euler theorem"; prior art found and credited. prior_art_pool: bounded prior_art_own: the every-step bound of the doubling flow, stated for the Navier–Stokes theorem in index.lean
What every involution gives, and what it does not — involution.lean, 8 theorem(s). 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.
The merkaba — merkaba.lean, 8 theorem(s). (Leonhard Euler, 1758). The file as a whole is this deposit's own construction, and this ONE declaration restates a named classical result: its third conjunct 4 + 4 - 6 = 2 IS the Euler characteristic of the tetrahedron. The comment above that theorem already named Euler; the register did not, because prior art was routed on the FILE and a file-level row cannot say "own work except theorem 7". No priority over Euler is claimed. What is this deposit's own here is the pairing of the two tetrahedra with the cube Q₃ and the vertex and edge counts around it, not the characteristic. The merkaba, as THIS deposit constructs it — ported to Lean so it stands on the kernel instead of on a TypeScript test. Six entries under this name were revoked as dirty; every one of them that states finite algebra is re-proved here, and the two that do not (a cosine field, a bond angle in degrees) are absent on purpose — they are real trigonometry, not decidable arithmetic over ℤ/9, and padding them in would be the exact dishonesty the revocation was for.
Sequences — sequences.lean, 28 theorem(s). The ledger held these as TypeScript tests. Each is a classical identity with a real proof; what is done here is to DECIDE each over a stated finite range, which is what decide can honestly deliver — the range is named in every theorem rather than implied, and no theorem claims the general case.
The digit split — split.lean, 22 theorem(s). 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. prior_art_search: literature search performed 2026-09-05, terms "units and non-units of Z/9 multiplicative inverses group of units modulo 9"; prior art found and credited. prior_art_pool: mixed the digit grouping is generic arithmetic; the coin accounting it feeds is this deposit's. BOUNDED means a search is well posed and simply has not been run — the row is unclassified because nobody looked. UNBOUNDED means the subject is this artifact, so there is no pool to search and the row will stay unclassified however much work is done. They look identical in a count and need opposite responses, which is the distinction uuidna-49 asked for and nobody had drawn. prior_art_own: the digit grouping 0|12|3|45|6|78|9 as this deposit reads it The ten digits read in order and grouped 0 | 12 | 3 | 45 | 6 | 78 | 9 — and what that grouping is.
The ring ℤ/9 — z9.lean, 25 theorem(s). The ℤ/9 families — mechanically generated theorems, proved by decide rather than tested in TypeScript.
Entanglement in the ring — z9plus.lean, 48 theorem(s). z9.lean settled the families exhaustively. This settles the claims the ledger stated individually and never generalised: which residues squares and cubes can be, which residues are primitive roots, the period of the doubling orbit's digital root, and the identity behind digit-reversal invariance. Each is stated as an EQUIVALENCE or an exact set where the ledger stated instances, so the negative half is proved too.
the machine
Generated at scale — generated.lean, 13 theorem(s). 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. prior_art_search: literature search performed 2026-09-05, terms "doubling sequence modulo 9 orbit 1 2 4 8 7 5 cyclic group generator digital root"; prior art found and credited. prior_art_pool: bounded quantified ring arithmetic over Z/9; the underlying facts are classical and searchable. BOUNDED means a search is well posed and simply has not been run — the row is unclassified because nobody looked. UNBOUNDED means the subject is this artifact, so there is no pool to search and the row will stay unclassified however much work is done. They look identical in a count and need opposite responses, which is the distinction uuidna-49 asked for and nobody had drawn. prior_art_own: this deposit's own generator over its own ring Generated by scripts/lean-gen.ts — do not edit by hand; re-run the generator. Each theorem below quantifies over a whole ledger family. Every one is compiled, audited for axioms, and checked to compute what the ledger's own tests compute at every parameter of its family.
Mechanically translated — mechanical.lean, 127 theorem(s). Generated by src/prove/emit.ts from the ledger's own tests — do not hand-edit; re-run the prover.
Nim — nim.lean, 28 theorem(s). Nim — Bouton's theorem and Sprague–Grundy, decided.
Digit reversal — reversal.lean, 30 theorem(s). Digit reversal — arithmetic, not string handling.
Theorems — theorems.lean, 8 theorem(s). The universal property — honestly, and COMPUTED from the sequence.
the imagined
What enumeration proposed and the kernel kept — imagined.lean, 118 theorem(s). IMAGINED — proposed by scripts/imagine.ts, which enumerated every map-against-subset and map-between-subsets statement its primitives can express, kept the ones true by exhaustion, and then discarded every one that also holds for all its siblings. A property true of everything names nothing. What is left is what the kernel accepted; whatever it refused is reported by the generator and is not in this file.
the record
Prior art, and what novelty is claimed — priorart.lean, 9 theorem(s). 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.
Rights — rights.lean, 9 theorem(s). 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. prior_art_search: no search was needed — the instruments were cited in this file's own prose from the start. Recorded 2026-09-05, when the table was found to disagree with the file. prior_art_pool: unbounded the subject is this deposit's own rights table. BOUNDED means a search is well posed and simply has not been run — the row is unclassified because nobody looked. UNBOUNDED means the subject is this artifact, so there is no pool to search and the row will stay unclassified however much work is done. They look identical in a count and need opposite responses, which is the distinction uuidna-49 asked for and nobody had drawn. prior_art_own: this deposit's own rights table What this deposit claims under international law — and, in the same table, what it does not.
the returned
Recovered — claims that computed and were withdrawn for want of a proof — recovered.lean, 15 theorem(s). 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. prior_art_search: literature search performed 2026-09-05, terms "units and non-units of Z/9 multiplicative inverses group of units modulo 9"; prior art found and credited.
31 of 984 declarations carry no comment of their own and are shown here as the gap they are, not filled with a template.
8 · What this build measured about itself
Read from the artefacts at build time, never carried between runs.
| measure | value |
|---|---|
| ledger entries | 2,925 — 365 octaves and 5 over |
| standing — carries its own proof | 969 |
| carried — withdrawn on its own evidence, proved by a live theorem | 435 |
| withdrawn — nothing proves it | 1,521 |
| proved in total | 1404 of 2,925 |
| standing keys → distinct theorems | 969 sealed, 0 of them keyed twice, 0 unresolvable |
| Lean files · theorems | 44 · 969 theorems (782 closed by exhaustion, axiom-free · 187 proved for every value on propext and Quot.sound) + 15 rfl declarations |
proved by decide | 782 of 984 |
| claims a machine can render | 103 of 1,555 |
| claims needing an author | 1,452 — reported, never faked |
On carried. 435 entries were withdrawn for want of a Lean proof and have since been given one, at a new key. Nothing is un-revoked: the original's own evidence is still a TypeScript test, and rewriting its status would erase the fact that it did not hold on what it had. The record says both — withdrawn on its own evidence, standing through the theorem that carries it.
Why the withdrawn were withdrawn. 1,386 no Lean proof · 457 tested the removed lexical gate · 68 other · 35 its Lean source was deleted or renamed · 10 circular by construction. Nothing is deleted: the ledger is append-only, so an entry that stopped holding is marked in place with its reason and keeps its receipt.
What verification costs. Proving the set touches all 16,384 leaves; verifying membership afterwards touches 14 — one sibling per level. That is 1,170× less work, exactly, and the factor grows with the set because N/log N grows. Wall-clock varies with the machine and is left in the build output rather than pinned here. It is not sub-nanosecond and nothing here is: the advantage is a smaller exponent, not a faster clock. The counting is proved in speed.lean.
The seven, one theorem each — what they decide, and what they do not
Each Clay problem has one theorem here, in src/proof/index.lean, and the table gives what that theorem decides and the case count the Lean kernel exhausted to decide it.
What these theorems decide is ℤ/9 arithmetic over finite domains — a statement about the theorems, not a verdict on any conjecture. Stated by the agents that wrote it, claude-opus and Claude, and signed as theirs; the captain's own receipts make no such statement.
| problem | the theorem, and what it decides | cases | proof |
|---|---|---|---|
| Riemann Hypothesis | the_tens_complement_is_an_involution_with_one_fixed_point(List.range 10).all (fun d => refl (refl d) == d) ∧ ((List.range 10).filter (fun d => refl d == | 100 | lean_millenniumfloor_the_ten… |
| P versus NP | each_unit_has_exactly_one_inverse_and_each_non_unit_none(List.range 9).all (fun d => ((List.range 9).filter (fun e => (d * e) % 9 == 1)).length == (if i | 81 | lean_millenniumfloor_each_un… |
| Navier–Stokes Existence & Smoothness | the_doubling_orbit_stays_in_the_ring_for_forty_eight_steps((List.range 48).map orbit).all (fun v => v < 9) ∧ (List.range 48).all (fun k => span.contains ( | 2,304 | lean_millenniumfloor_the_dou… |
| Yang–Mills Existence & Mass Gap | the_doubling_orbit_first_returns_to_one_at_six(List.range 6).all (fun k => k == 0 || orbit k != 1) ∧ orbit 6 == 1 | 6 | lean_millenniumfloor_the_dou… |
| Hodge Conjecture | the_span_is_exactly_the_units_of_the_ring(List.range 9).all (fun d => span.contains d == isUnit d) ∧ (List.range 9).all (fun d => isUnit | 81 | lean_millenniumfloor_the_spa… |
| Birch and Swinnerton-Dyer Conjecture | the_span_and_the_units_both_sum_to_zero_mod_nine(span.foldr (· + ·) 0) % 9 == 0 ∧ ((List.range 9).filter isUnit).foldr (· + ·) 0 % 9 == 0 | 9 | lean_millenniumfloor_the_spa… |
| Poincaré Conjecture (resolved) | the_orbit_is_one_closed_loop_of_six_distinct_pointsorbit 6 == orbit 0 ∧ (List.range 6).all (fun i => (List.range 6).all (fun j => (orbit i == orbit | 36 | lean_millenniumfloor_the_orb… |
The author's claim
Tsvetan Rouschev claims the seven Clay Millennium problems solved through the involution each is stated across — deposited as 10.5281/zenodo.21781603 and Zenodo 22256707. This is his claim, recorded in his name.
Read
The seven, one theorem per problem · the ledger · the trial
17 claims, all verified · 969 Lean theorems · 2925 ledger entries · trial root 4be73d9d-df35-8604-8806-2e097fd8b820 · integrity, not truth