torsion_first
plain-language theorem explainer
The lemma records that the first-generation torsion vanishes by definition in the rich ledger. Mass-ratio calculations in Recognition Science cite this zero base when deriving the φ^11 and φ^17 splittings between generations. The proof is immediate reflexivity on the generationTorsion case for .first.
Claim. The torsion offset for the ground-state generation satisfies τ₁ = 0.
background
In the RSLedger module, particle masses occupy discrete rungs on the φ-ladder. Each generation carries a torsion offset τ_g obtained from Q₃ cube combinatorics in D=3: the ground state receives zero, the second generation receives passive_field_edges(D), and the third receives that quantity plus cube_faces(D). The module documentation states that these offsets replace ad-hoc φ-formulas, yielding mass ratios m_f / m_g = φ^{r_f - r_g} once the rung is assembled as baseRung + τ_g.
proof idea
The proof is a one-line reflexivity that matches the .first case of the generationTorsion definition.
why it matters
This base case anchors the torsion ladder that supplies the zero offset for the inter-generation relations Gen 2 / Gen 1 = φ^{11} and Gen 3 / Gen 1 = φ^{17} listed in the module documentation. It closes the ground-state entry in the Q₃ cube combinatorics that feeds the eight-tick octave and D=3 structure of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.