What is machine-checked, and how to reproduce it

The evidence layer — with the counts disputed in public

The real question on this page is not how many theorems there are. It is which statements carry a machine-checked proof, and which do not. A count is a marketing number; a boundary between proved and unproved is a scientific one. So the page is organised around that boundary — and it ends by disclosing, rather than hiding, a disagreement about the counts themselves.

What is machine-checked

Two corpora of Lean 4 carry proofs. They are different bodies with different scopes, and they are not interchangeable.

Corpus	What it proves
The categorical layer (CausModel)	The intervention category and its universal property; cohesion as an idempotent monad; the boundary as its fixed point; the defect as a decidable obstruction class. The layer has zero $sorry$ , zero $axiom$ .
The value layer (frozen)	The 33 frozen declarations — 27 theorems and 6 lemmas over 7 definitions — formalising the logistic coordinate instance: the two-term potential, the exact derivative identity, the sign trichotomy, both limits in $ε$ – $δ$ form.
The bridge	Transfers the categorical layer's "the form is forced" theorem and its non-categoricity negative result onto the value layer's central object.

What is not machine-checked — and cannot be

Item	Why it cannot be
The variable identification ( $κ \leftrightarrow$ stiffness, and its companions)	It is an assumption about the world. No formalisation removes it. Mapping hypothesis
The interpretive residue	Reading the conserved charge as self-continuity is interpretation, and is tagged as such. Interpretation
The numerical tables	They are deterministic computation, not machine proof. Running the numbers is not proving a theorem. Computation

Machine-checked exactness and empirical confirmation are different achievements. This work holds only the first, and says so.

Reproduce it

cd lean && bash build_lean_all.sh

Source snapshot and reproduction scripts: see Papers & code; after publication also available from limisys.github.io/boundary-axiom/.

A full reproduction requires Lean 4.33.0 and Mathlib of the matching version. The script compiles every module, then the single importable entry point, then runs the zero- $sorry$ check. Two auxiliary scripts verify the frozen manifest and the declaration counts.

Two known defects in the bundled verification scripts, disclosed as-is. (i)

check_no_sorry.py

globs

*.lean

relative to the current directory, so running it from one level up scans zero files and still prints "pass" — a false green. (ii) The frozen manifest

MANIFEST.tsv

is stale, so its verification currently fails on two files. An independent recount tool is provided precisely because the bundled scripts can report success while checking nothing.

The 33-declaration dependency graph

The machine-extracted dependency graph of the A-module BoundaryTheory: 7 definitions and 33 load-bearing declarations (40 nodes / 72 edges / 5 layers), from the boundary potential to C_H = π²/3.

Read it in 60 seconds: definitions → the potential/force cluster and the entropy/integral cluster → C_H. The two clusters share almost no intermediate result; the graph exposes that structural seam. Note: the B-line seam and no-go are not in this graph.

The 33-declaration dependency graph (English) — The 33-declaration dependency graph (English; click for the full-size SVG)

Current external statement (2026-10-19 unified audit): unified body 56 files / 467 theorems+lemmas / 90 definitions; Paper B slice 53/417/77; A module 1/33/7. The table below is the historical four sets plus one direct measurement, kept to show the divergence in counting standards.

The counts disagree, and that is disclosed here

The programme's own documents report four different sets of numbers for the same corpora. Measuring both corpora directly, on 2026-10-09, gives a fifth. Rather than pick the flattering one, all of them are listed.

Corpus	Source	Claimed
Categorical layer	the paper	124 declarations · 12 modules · cold build 3333 jobs
	the line's own audit notes	155 declarations · 14 modules · 3335 jobs
	direct measurement (2026-10-09)	107 theorems / 49 definitions / 15 files
Boundary programme body	the line's own summary	417 theorems · 77 definitions · 53 files
Boundary programme body	direct measurement (2026-10-09)	434 theorems / 84 definitions / 55 files
Value layer	the paper and the summary	33 declarations — the only figure on which everything agrees

Why this is on the page rather than in a footnote. A site whose stated purpose is that a competent critic can begin checking without believing anything must not present a disputed count as a fact. The counts are snapshots; the counts are also in dispute; the command is neither. Run the command.

Status of every claim on this page

Claim	Status
Both corpora compile with zero $sorry$ and zero $axiom$	Machine-Checked
The 33 frozen value-layer declarations	Machine-Checked
The bridge theorems	Machine-Checked
Any declaration count	Disputed — four published sets
Any statement about a real system	None exists

Found something to challenge? → How to challenge this work