GenerationTorsionCert
plain-language theorem explainer
Empty certificate carrier whose verification predicate packs the claim that fermion-generation torsion offsets are exactly {0, 11, 17}, with differences {11, 17, 6}, and that any RS ledger carrying those torsions has matching lepton rung-difference exponents. Anyone checking that mass-ratio exponents are structure-derived (not free φ-parameters) cites this pack. Content is definitional conjunction plus a one-shot refine proof of the predicate.
Claim. A unit certificate type whose verification predicate asserts: generation torsion offsets equal $0$, $11$, $17$ on the three generations; pairwise torsion differences equal $11$, $17$, $6$; the canonical RS ledger carries exactly that torsion map; and every RS ledger with the same torsion map has lepton rung differences equal to those torsion differences (so mass ratios are forced as $\varphi^{\Delta\tau}$).
background
In the Recognition ledger, each fermion generation carries an integer torsion offset $\tau$. The module fixes the canonical values from eight-tick geometry: first generation $\tau=0$ (ground), second $\tau=11$ (passive cube edges), third $\tau=17$ (faces times wallpaper groups over 6). Mass ratios are then not free $\varphi$-formulas but consequences: $m_{g_i}/m_{g_j}=\varphi^{\tau_i-\tau_j}$, so the exponents are exactly the torsion differences $11$, $17$, and $6$.
An RSLedger is a ledger object with a torsion map and rung-difference data (here restricted to leptons). The canonical ledger is the distinguished RS-compliant instance whose torsion is required to equal the generation-torsion function. The certificate is an empty structure; all mathematical content lives in the Boolean-style verification predicate attached to it.
Upstream forcing material (self-similar dressings, canonical arithmetic, circle-winding injectivity, cost-projector structure) supplies the ambient RS geometry that makes those integer offsets meaningful, but this module only unfolds the torsion function and does elementary arithmetic.
proof idea
The structure itself is empty (deriving Repr only). The verification predicate is a flat conjunction of eight atomic claims: three torsion values, three torsion differences, equality of canonical-ledger torsion with the generation-torsion map, and a universal implication from matching torsion to lepton rung differences.
The companion theorem that every certificate verifies is a single refine into eight goals. Six goals are discharged by named arithmetic lemmas (torsion_first/second/third, torsion_diff_21/31/32). One goal is canonicalRSLedger_torsion. The last introduces an arbitrary ledger with matching torsion and applies massRatios_from_torsion_structure. No induction, no analysis: definitional unfolding plus $11-0=11$, $17-0=17$, $17-11=6$.
why it matters
Closes a slice of the parameter-derivation gap: mass-ratio exponents for the three generations are read off ledger torsion rather than inserted by hand as $\varphi$-powers. That is the module's stated key result and a concrete step toward non-circular mass formulas on the $\varphi$-ladder (yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$).
The integers themselves are tied to eight-tick geometry (primer T7: period $2^3$), so the certificate sits downstream of the octave forcing chain even though this file only records the arithmetic consequences. No downstream consumers are wired yet (used_by empty); the pack is a verification endpoint meant for audit and for later mass-spectrum assembly.
Non-circularity is explicit: no measurement constants, no axioms, no sorry. What remains open is the geometric derivation that $\tau\in{0,11,17}$ must be those values from first principles; this certificate assumes the torsion function and certifies its mass-ratio fallout.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.