Appendix C — The mechanization
Appendix B is prose, and prose proofs can hide a step. This appendix reports the machine check: a self-contained Lean 4 development in the book’s repository under proofs/, using no mathematics library, so every ingredient of the argument appears explicitly. One command re-checks everything, on a pinned toolchain. No proof contains a placeholder, and the checker reports each theorem’s axioms.
Checked — every result on the formalizable list:
| result | Lean theorem |
|---|---|
| B.1 representation, finite and full (the union law) | representation_finite, representation_full |
| B.2 arity core (Prop. 5.2) | arity_minimal_is_three |
| B.2’s trap: the pairing reduction, located | gadget_escape_closed |
| B.3 uniqueness, assembled and exact (Thm. 5.4) | uniqueness, uniqueness_iso |
| B.4 independence, four of the five conditions | atomistic_independent, order_freedom_independent, idempotence_independent, accumulation_independent |
| B.5 analysis theorem, the shape half (Prop. 4.4) | analysis_shape, minimal_window_exists |
| B.6 independent evolution (Prop. 4.5) | present_substitution, timelines_independent |
| B.7 homomorphism, against a model of §18 (Prop. 8.1) | homomorphism, seval_monotone |
| B.8 genericity core: the free theorem (Thm. 8.2) | transposition, treats_no_name_specially, not_generic_of_treatsSpecially, canon_renaming_commutes |
| Prop. 7.1 delta normal form | delta_normal_form |
| B.9 federation closure | federation_closure |
| B.5 ↔︎ B.7, the halves meeting | halves_meet |
Prop. 6.1 canon exists, ground states |
canon_exists |
| Props. 7.2–7.4 forms, one algebra, five moves | submit, find_then_denote, five_moves |
| Prop. 9.1 the bill for anonymity, algebraic core | bill_for_anonymity |
| Prop. 9.2 erasure, and the quad repair | attribution_erased, attrOf_merge, attribution_closes |
| Prop. 20.1 nothing else to vary | nothing_else_to_vary |
The embedding half of B.1 and the arity core depend on no axioms at all; the rest use only Lean’s three standard ones.
One result in the development checks nothing above: coordination-free convergence — parties that received the same updates agree, in any order, with any duplication — follows from the merge laws alone, which turns Chapter 5’s corroboration from the replication literature into a theorem about this model.
The check sharpened two things the prose states only in passing. B-2d splits into two named hypotheses: one half of the atom-map homomorphism is derivable from the merge laws alone, and only the “no emergence” half is genuinely axiomatic. And that axiom is necessary: the model (ℕ, max) satisfies every merge law yet violates atomicity, so B.1 must assume what it assumes. The formalization answers “did you assume what you needed?” with: yes, necessarily, and here is the witness.
The ceiling is a category boundary, not a shortfall. Lean checks the conditional skeleton: given the requirements as axioms, everything downstream follows. What it can never do is discharge the axioms, because their justification is the Transposition Thesis, and that is unprovable the way the Church–Turing thesis is unprovable: it equates an informal subject (what the web enforces) with a formal object (the merge laws). No formalism can certify its own adequacy to an informal subject. The thesis is corroborated and consequence-tested, never proved.
Nothing formalizable remains. Four results are checked to a stated scope: B.7’s correspondence is to a model of the query algebra’s specification, never to an engine; B.8’s is the free-theorem core; canon is checked on named entities; and the bill for anonymity is checked as algebra. What those four defer — the transformation language’s completeness, the canonical labeling of unnamed entities, the cost of redundancy elimination — stays cited, because each is someone else’s theorem. The fifth independence condition, totality, is enforced by the formalization’s own typing, so dropping it leaves nothing to state. Parts I, IV, and VI are not on the list, because scores and history are not mathematics.