generationTorsion
Canonical torsion offsets for the three generations are supplied by this definition, which evaluates to zero, eleven, and seventeen respectively from the D=3 cube edge and face counts. Derivations of mass ratios in the Recognition Science ledger invoke it to establish the precise phi-power relations. The implementation consists of a case split on the Generation type that directly substitutes the combinatorial functions without additional computation.
claimThe torsion offset function assigns to each generation $g$ an integer value given by cases: zero for the first generation, the passive-field edge count $E(D)$ for the second, and $E(D)$ plus the face count $F(D)$ for the third, where $D=3$ yields the concrete values 0, 11, and 17.
background
The RSLedger module equips the phi-ladder mass formula with generation-dependent torsion offsets so that rung differences produce mass ratios as exact powers of phi. Torsion for generation $g$ is added to the sector base rung, giving the full rung and the ratio $m_f/m_g = phi^{r_f - r_g}$. The module documentation states that the offsets arise from D=3 cube combinatorics and produce the inter-generation ratios phi to the 11, 17, and 6.
proof idea
The definition is realized by pattern matching on the three constructors of the Generation inductive type. The first case returns the constant zero. The second case returns the integer value of passive_field_edges applied to D. The third case returns the sum of passive_field_edges D and cube_faces D, cast to integers.
why it matters in Recognition Science
This definition supplies the torsion structure required by canonicalRSLedger and by the theorems massRatiosFromTiers_canonical and massRatio_21_canonical, which recover the phi-power triple for inter-generation ratios. It realizes the geometric derivation of torsion from Q3 cube combinatorics described in the module documentation, closing the link between cube geometry and the phi-ladder mass formula.
scope and limits
- Does not assign torsion values outside the three fermion generations.
- Does not derive the numerical values of passive_field_edges or cube_faces.
- Does not prove that these torsions yield the physical mass ratios.
- Does not extend to non-fermion sectors or higher-dimensional cubes.
Lean usage
rw [hL, generationTorsion]formal statement (Lean)
59def generationTorsion : Generation → ℤ
60 | .first => 0
61 | .second => (passive_field_edges D : ℤ)
62 | .third => (passive_field_edges D + cube_faces D : ℤ)
63