torsion_third
The lemma establishes that the third generation carries a torsion offset of 17 in the Recognition Science rich ledger. Researchers deriving fermion mass hierarchies from discrete φ-ladder rungs would cite this offset when scaling third-generation particles relative to the ground state. The proof reduces directly by simplification that unfolds generationTorsion into the sum of passive field edges and cube faces for D=3.
claimIn the Recognition Science ledger the torsion offset assigned to the third generation satisfies $τ_3 = 17$.
background
The RSLedger module encodes a rich ledger in which particle masses occupy discrete rungs on the φ-ladder. Each generation receives a torsion offset τ_g obtained from the combinatorics of the three-dimensional cube Q₃. The third-generation offset is defined as the sum of passive field edges and cube faces, replacing ad-hoc mass formulas with a geometric count.
proof idea
The proof is a one-line simplification that expands generationTorsion .third using the definitions of passive_field_edges, cube_edges, active_edges_per_tick, cube_faces, and D.
why it matters in Recognition Science
This lemma supplies the concrete value 17 that completes the torsion triple {0, 11, 17} for the three generations. The module documentation uses these offsets to obtain the inter-generation mass ratios φ^{11}, φ^{17}, and φ^6 via the rung formula rung = baseRung + τ_g. The result therefore anchors the discrete rung assignments that follow from T8 (D=3) and the cube geometry of the Recognition Science framework.
scope and limits
- Does not derive the cube edge or face formulas from first principles.
- Does not compute explicit mass values or ratios.
- Does not extend the torsion assignment to higher dimensions or additional generations.
- Does not invoke the J-function or Recognition Composition Law.
formal statement (Lean)
69@[simp] lemma torsion_third : generationTorsion .third = 17 := by
proof body
Term-mode proof.
70 simp [generationTorsion, passive_field_edges, cube_edges, active_edges_per_tick, cube_faces, D]
71
72/-- Torsion difference between generations -/