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.