The foundational arithmetic library

This part of the book is the readable front end to a native first-order Peano arithmetic library. It begins with ordinary equality and semiring laws, builds division, relational gcd, balanced Bézout, Gauss cancellation and Euclid’s lemma, then constructs finite factor sequences and their products using Gödel-β codes. The endpoint is a checked, β-coded Fundamental Theorem of Arithmetic.

Two cumulative editions

The Stable library contains 432 closed native theorems, including factorization existence, extensional uniqueness, their combined FTA, and a constructive theorem producing a prime above every supplied bound. The newest Alpha quadratic-reciprocity campaign includes parity, constructive residue decision, finite folds, factorial and power algebra, modular units, sign and half-range bridges, β swap/reindex, finite pigeonhole, replacement balance, and exact swap-last product invariance. Twenty-five strict-HA entries now expose canonical remainder, congruence, bounded modular inverses, relational gcd/LCM compatibility, LCM existence and uniqueness, and the gcd–LCM product law. The exact 23-row generalized-CRT dependency closure is now Stable: it covers the all-modulus solvability criterion, classification modulo a relational LCM, the zero/nonzero canonical boundary, certified obstruction, and raw-input total decision. New reviewed layers enter Alpha first and move to Stable only after closure, compilation, dependency, resource, and release audits. Sealed Alpha v2 adds seventeen body-checked K3C rows for valid list codes, membership, unique in-range lookup, extensional code equality, and unique outer-cell decomposition. Sealed Alpha v3 adds the first twenty-one Bertrand rows, and sealed Alpha v4 adds forty-two Round-2 rows for exact valuation multiplication, integer envelopes, ceiling/floor-square arithmetic, and the quotient budget. Sealed Alpha v5 preserves that complete 965-row ledger and appends seven body-checked FactorialVal rows. Sealed Alpha v5 therefore has 972 rows, sealed Alpha v6 has 993, sealed Alpha v7 has 1,017, sealed Alpha v8 has 1,055, sealed Alpha v9 has 1,076, sealed Alpha v10 has 1,085, and sealed Alpha v11 has 1,123. Historical Alpha v12 preserves the entire v11 ledger and appends 180 body-checked Bertrand rows in nine exact twenty-row microbatches. Alpha v13 adds the four-square and Lucas campaigns; v14 adds Kummer’s carry theorem; v15 adds the supplementary laws and complete two-square classification. Current immutable Alpha v16 preserves all 1,673 v15 statements while promoting exactly 315 independently proved quadratic-reciprocity results, including the final theorem, to checked use. Stable remains the unchanged default. See Alpha and Stable library editions for the exact scopes and lifecycle.

432Stable theorems

1,673Alpha v16 theorems

885Alpha checked-use rows

1,241Alpha-only rows

The generated Stable snapshot has ordered root 4d02dc439d53533e8992a471b26ee34059fb6001f822041e42c56b2cc0a7a079. Every entry is reconstructed from its authored script and checked from the empty context. Names, summaries and hashes organize the library; none of them grant proof authority. Its graph has 1,185 direct dependency edges; the Book exposes 432 theorem cards, while the synchronized vault contains 531 notes and 5,377 resolved links.

The current Alpha v16 graph has 1,673 theorems, 5,615 direct edges, and 53 dependency layers. Its mixed evidence is intentional: 432 Stable-closed and 453 Alpha-closed rows have actual checked-use authority, while 788 body-only rows remain visible without being treated as empty-context facts. No pending row remains. The historical Alpha v12 graph has 1,303 theorems, 4,302 direct edges and its immutable evidence partition still includes 732 body_checked rows. Every Alpha v1–v15 parent remains sealed; Stable remains 432. The exact contract and opt-in API are on the edition page.

Historical Alpha v12 retains the Alpha-v11 B4 and B5-support tranches, then adds the dependency-closed B6 support and B5–BP02 completion chain. Its frozen partition was 432 stable_closed, 138 alpha_closed, 732 body_checked, and one pending_layered_closure; checked use was 570. The current v16 partition is 432 stable_closed, 453 alpha_closed, 788 body_checked, and zero pending rows. Only the completed quadratic-reciprocity closure was promoted; Bertrand, Lucas, four-square, Kummer, supplementary-law, and two-square body evidence has not acquired checked-use or Stable authority.

The mathematical metro map

The exact dependency graph has 432 vertices and 1,185 edges and is useful to machines, but a human first needs the stations. Each box below is a link into the guided tour.

The exact generated graph remains available as an immutable dependency-graph.mmd. The Stable theorem atlas gives a readable local neighborhood instead of attempting to draw all 1,185 edges at once. The Alpha QR proof explorer adds permanent theorem tags, numbered tactic-line targets, and the larger quadratic-reciprocity campaign slice. It is not the complete Alpha or Stable catalog. Its parallel definition-aware edition renders the same 557 specifications with a 40-entry conservative-definition registry (38 definitions occur) and exact native replay lines; it does not change the proof graph or admission status. Its interactive dependency graph draws short or critical premise chains, start-to-target corridors, and complete transitive cones. The complete Bertrand proof explorer applies the same interface to all 544 nodes in the final strict theorem’s closure.

Choose your route

If you want to…	Begin here	Then move to…
understand the two release editions	Alpha and Stable library editions	canonical counts, checked-use boundary, promotion lifecycle, and graph legend
understand the mathematics	Guided route from zero to FTA	the focused theorem links inside each stage
inspect every Stable proof	Stable theorem atlas	exact statements, complete scripts, dependencies and dependents
follow the Alpha QR slice line by line	Alpha QR proof explorer	permanent tags, linked lemma references, informal outlines and source receipts
read expanded formulas through linked names	Definition-aware proof explorer	persistent PD expansions, exact native replay lines, and the unchanged theorem status
curate the next conservative edition	Curating the next conservative edition	P0/P1/P2 definitions, API completeness, and paired-source gates
see how theorems depend on one another	Interactive dependency graph	short and critical premise chains, route corridors and complete prerequisite cones
understand soundness	Language, notation, and trust	Self-contained proof sharing
study division and congruence	Divisibility and subtraction-free congruence	GCD and balanced Bézout
study encoded lists and lookup	K3B Alpha: cell histories and extensional lookup	the compact Alpha/Stable graph, exact proof sources, and WMI receipt
use list validity and membership	K3C Alpha: valid lists, membership, and semantic lookup	the seventeen-row interface, exact body receipts, and append/restriction gate
study primes and factorization	Primes and unique factorization	the FTA and prime_unbounded cards in the atlas
follow the reciprocity campaign	Quadratic reciprocity campaign	parity, residue-decision, and finite-fold cards in the atlas
follow the Bertrand campaign	Bertrand’s postulate campaign	constructive interval search, valuations, the central-binomial route, and exact risk gates
inspect the complete Bertrand proof	Complete Bertrand proof explorer	all 544 nodes, exact tactic bodies, and the interactive 1,917-edge dependency map
train a proof-producing model	Using and extending the library	the snapshot, corpus and vault links below
audit provenance	Sources and clean-room provenance	catalog source mappings and the separate Lean companion

What the native FTA says

At the readable level, the endpoint is

\[\begin{split} \begin{aligned} &\left(\forall n,\ n\ne0\Longrightarrow\exists F.\; \operatorname{CanonicalPF}(n,F)\right)\\ &\qquad\land \left(\forall n,F,G.\; \operatorname{CanonicalPF}(n,F)\land \operatorname{CanonicalPF}(n,G) \Longrightarrow F=_{\mathrm{ext}}G\right). \end{aligned} \end{split}\]

Here \(F\) and \(G\) are not primitive lists. BetaAt decodes a bounded entry from two natural-number codes, a second β code records prefix products, and equality is extensional on the selected finite prefix. The exact statement is ordinary first-order PA over 0, S, +, * and equality.

Native endpoint	Nodes	Depth	Cuts
prime_factorization_existence	43,973	98	1,328
prime_factorization_uniqueness	29,789	82	854
fundamental_theorem_of_arithmetic	73,767	99	2,184

The top-level authored proof is deliberately only three commands:

split
exact prime_factorization_existence
exact prime_factorization_uniqueness

That contrast is central. A short modular script is not a hidden axiom: its dependencies are embedded as self-contained Cut nodes, producing the 73,767-node closed certificate checked by the kernel. Read the complete card for fundamental_theorem_of_arithmetic.

Prime unboundedness is a separate constructive theorem

FTA is not used to prove that there is a prime above every bound. The native proof obtains a nonzero common multiple \(c\) of every positive number through \(n\), takes a prime divisor \(p\) of \(S(c)\), and excludes \(p\le n\): such a \(p\) would divide both \(c\) and \(S(c)\), hence one.

\[ c \longrightarrow S(c) \longleftarrow p, \qquad p\le n \Longrightarrow p\mid c \land p\mid S(c) \Longrightarrow p\mid1. \]

The theorem prime_unbounded has 4,595 nodes, depth 82 and 146 Cuts. Its full 84-command authored proof is embedded in the prime_unbounded atlas card.

The trust path

Authored scripts
readable tactic bodies

→

Nested Cuts
complete dependency proofs embedded

→

Empty-context kernel check
original closed formula

The checked FTA and prime_unbounded use only PA1–PA6 and ordinary induction; their audits find no double-negation elimination. The object language gained no primitive division, remainder, gcd, prime, list, product or factorization symbol.

Four synchronized views

One theorem name identifies the same object in four places:

1. the executable TheoremSpec and checked certificate;

2. the generated snapshot and dependency graph;

3. its card and narrative links in this Jupyter Book;

4. its atomic Obsidian vault note.

The current synchronized surfaces are:

• native theorem source;

• checked-theorem snapshot;

• research catalog;

• arithmetic vault map;

• deterministic training corpus.

There is exactly one deliberately unproved catalog boundary: the conventional integer-coefficient Bézout interface. Peano Lab quantifies only over naturals. The separately named balanced four-natural Bézout theorem is checked and is the interface used by Gauss cancellation and Euclid’s lemma.

Start reading

Continue with the guided route. It alternates intuition, exact formulas, proof anatomy and immutable proof links. When you want to move backward or forward through the dependency DAG, open the theorem atlas and focus the theorem you are reading.