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.