The main theorem states the continuum limit, and clause (iii) is formalized at every member

Clause (iii) closes at every member, and the main theorem now states the continuum limit

Development snapshot 5ba0ca30d6e0113b9cd526b150f50c26e6227b3f (2026-09-08).

thm:main changed since v0.3.0, in two ways. Clause (ii) now states, at every window and coupling whose cut names an edge, that the edge is a located root of the window pencil's symbol attained at a word image, and it reads the contact pair $(3, H_r)$ through the walk's own divisor data at the head's compression to the tower labels. Clause (iii) now locates the chain's height at every scale between the ray's floor and its two caps, reads the lattice spacing as that height under the unit map, and asserts that at two directions or beyond the spacing falls under every floor beyond the floor's key, the lattice form of the continuum limit. The revision was forced by the Lean transcription, which is what it exists to do; it strengthened the proof and corrected deviations from Monte Carlo results that traced to errors in the TeX.

Newly formalized since v0.3.0:

Clause (iii)'s member layer: main.clauseIII_all holds the corner cell's floor datum at every member of the classification through the one disconjugacy certificate transported across the residues.
Clause (ii)'s window half at the TeX's own quantifier: attained.attained_at with the root read divisorid.rootIff.
The remainder of lem:cornerpivot, lem:corner's cell floor with the corner-output clauses of thm:decomp and thm:twoaction, lem:cone, thm:continuum, thm:reconstruct, the depth chain of a window, the probe cap lem:attained(iv) and the gradient read of thm:momentform.
The tail read's floor-line certificate and cap block (Cornercert).
Clause (i)'s window-level interface: the pencil interface and transport field of thm:pairpencil, the member generating tables of con:memtable with their dual pairs and closure reads (Memtable), the vertex lists beyond two ends, and the cell list with the ray tier of thm:gappos.
Verification: 35,389 constants across both libraries, none depending on any axiom; the full build's largest single process peaks at 8.45 GiB at one thread (Cornerstore), under the hosted runner's budget.

Open: clause (i) at every region, cutoff and interior ray; the tail read's key, the scale under which a window's height sits below a stated floor, and its join at main; clause (iii)'s composite statement at main; and the reverse correspondence walk. The README's status section is now an overview, with the module docstrings carrying the per-label detail.

The tree now verifies on the hosted CI again

The heaviest single obligation drops from ~57 GB of memory to under 9 GB, which is what lets the standard GitHub-hosted runner build the full tree and run the axiom sweep. Nothing about the verified statements changed.

Newly formalized since v0.2.0 (development snapshot 7e91dceb532f13d0df40deaca9a1a38203df29c5, 2026-08-30):

• lem:cornerpivot (vii)'s certificate tiers
• lem:spectator's derivation tier
• The entry-read tier

Full closure on thm:main (i) and (ii) in Lean

Both counting clauses of thm:main are now closed at every member of the classification, and two of clause (iii)'s largest support theorems are formalized whole. Snapshot at development commit fe29955ce87a276a0e5aa729006514bedd15d4f0.

Clause (i) at every member. main.clauseI_all holds gap positivity at the whole classification: the tie with the two committed chain reads as parametric theorems over the rank at the diagonal windows, E8's coupled window its own case.

Clause (ii) at every member. main.clauseII_all holds the contact value (3, H_r) at the whole classification: the channel's order count, the base collection, the excess–harmonic value, and the occupancy families as theorems over every residue and rank of the four series, the five fixed members decided by the kernel.

thm:groundreads complete. Clause (vii), the scale sandwich, lands with two corner scales compared at the grounds' own electric weights, the electric-square shell pricing, the scale counts, and the width telescope. All seven clauses (with (v′)) are now formalized.

lem:momentfold complete (new module Momentfold): the two moment streams with their fold identities, the graded square linear system for the truncated moment vector, the truncation cap, the scale comparison, and the datum assembly. The single-region datum read as a stream read at banded weights, with its scale closure at the elimination's cofactor reads.

lem:cornerpivot's certificate store (new module Cornerstore): the corner disconjugacy certificate's pre-tier data committed as Lean-side stores with kernel-decided validity reads.

theory.tex gains the forcing sentences its transcription surfaced, including lem:greenprod clause (iv) (the scalar chain's form read). The PDF is rebuilt.

.zenodo.json and CITATION.cff corrected: the manuscript is a completed proof of the Yang-Mills mass gap; the Lean tree is its transcription in progress.

Still open on the Lean side (README Status has the ledger): lem:cornerpivot's remainder, lem:corner's cell floor with the corner-output clauses of thm:decomp and thm:twoaction, lem:cone, thm:continuum, thm:reconstruct, the clause (iii) composite at main, and the reverse correspondence walk.

v0.1.0: first release of the Lean formalization

This release archives theory.tex with its compiled PDF, the companion manuscript the_physical_state.tex, and the first public snapshot of the Lean 4 formalization of theory.tex, under lean/. The snapshot is taken from the development tree at commit 9b0e7ce85e5e38914e7b3887a5d7a0c7680bd348 of 2026-08-25.

What the Lean tree holds. Two libraries, MassGap (117 content modules) and MassGapChecks (117 check modules, one per content module), transcribing the manuscript statement for statement: every top-level declaration sits in a namespace named after one \label of theory.tex, and each module's head docstring states which clauses of its label the module holds as theorems, which as decidable reads pinned by the batteries, and which arrive at other labels. Of the manuscript's 133 labels, 119 carry a Lean namespace.

Read off MassGap/Main.lean: main.Member is the classification's stated domain (the A-series at every residue, B/C/D at their index floors, and the five exceptional members); clause (ii) of thm:main, the contact pair (3, H_r), is the decidable read main.clauseII, decided by the kernel at every committed member. Clause (i), positivity of the cut at every interior coupling, is not yet stated at main — its derivation tier is landed (the count certificates, the chain, and thm:gappos's sandwich, transport, cell chain, cutoff price and window cut), and its wiring into one statement over main.Member is the open item. Clause (iii), the continuum reads, is not yet stated at main; lem:corner's coordinate, scaling, drift, grade-key, cap and count tiers and thm:restoration's first tier are landed, and lem:cornerpivot, thm:groundreads, lem:momentfold, lem:cone, lem:fourpoint, thm:continuum, thm:decomp and thm:reconstruct have no Lean yet. rem:dictionary, the correspondence to the conventional formulation, is prose by design and is not formalized.

Status: work in progress. The manuscripts have not undergone peer review, and this release is not an announcement of a completed formal proof of the Yang-Mills mass gap. Later releases may correct, reorganize, or extend the manuscripts and the tree.

The disciplines. Every declaration of both libraries depends on the empty axiom set: no propext, Quot.sound, Classical.choice, sorryAx, no native reflection; the kernel checks everything. The package is Lean core alone (lean-toolchain: leanprover/lean4:v4.32.2; no packages, no imports outside the two libraries), with no noncomputable, partial, unsafe, opaque or axiom declaration, every object computing by kernel reduction. The 8,413 battery examples decide the reads at committed data by kernel decide, with committed refusals isolating every load-bearing hypothesis. lakefile.toml sets warningAsError, so a sorry anywhere in either library is a build error.

Verifying. cd lean && lake build (239 jobs, no network dependency past the toolchain), then lake env lean AxiomCheck.lean, which walks every constant of both libraries with Lean.collectAxioms and prints constants read: 24174 / constants depending on axioms: 0, ending in an error otherwise; #print axioms main.clauseII in any file importing MassGap answers does not depend on any axioms.

Licensed under the Apache License 2.0.

Work in Progress: Mass Gap and Linear Theory of Physics Documents

This release archives the current working versions of theory.tex and the_physical_state.tex.

These manuscripts are intentionally maintained as compact technical specifications rather than publication-formatted papers. They are released here exactly as used in the ongoing research process.

Status: work in progress. The manuscripts have not undergone peer review, and the Lean formalization of theory.tex remains in progress. In particular, this release is not an announcement of a completed formal proof of the Yang-Mills mass gap.

Later releases may correct, reorganize, or extend the manuscripts. This release provides a public, citable record of their contents as of this version.