torsion_first
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the values of passive_field_edges or cube_faces.
- Does not address sector base rungs or explicit mass values.
- Does not treat mixing between generations or higher-order corrections.
formal statement (Lean)
64@[simp] lemma torsion_first : generationTorsion .first = 0 := rfl
proof body
65