massRatios_from_torsion_structure
plain-language theorem explainer
The theorem proves that a rich ledger equipped with the canonical torsion offsets 0, 11 and 17 from D=3 cube geometry produces lepton rung differences of exactly 11, 17 and 6. Mass modelers in Recognition Science cite this to confirm that inter-generation ratios emerge directly from torsion structure on the phi-ladder rather than being postulated. The term-mode proof splits the conjunction and discharges each conjunct by rewriting via the canonical rung difference under the torsion hypothesis, then reflexivity.
Claim. Let $L$ be a rich ledger whose torsion map equals the canonical generation torsion. Then the rung differences for leptons satisfy $L.rungDiff(leptons, second, first) = 11$, $L.rungDiff(leptons, third, first) = 17$, and $L.rungDiff(leptons, third, second) = 6$.
background
The RSLedger augments a basic ledger with a torsion function from generations to integers and base rungs per fermion sector. The rung for any sector and generation is the sector base plus the generation torsion; mass ratios are then phi to the power of the rung difference. The canonical generationTorsion is defined by cube combinatorics in D=3: 0 for first generation, 11 for second (passive field edges), and 17 for third (adding cube faces). Upstream result generationTorsion states: 'Canonical generation torsion from Q₃ cube geometry. - Gen 1 (ground state): τ = 0 - Gen 2 (passive-edge mode): τ = passive_field_edges(D) = 11 - Gen 3 (passive-edge + face mode): τ = passive_field_edges(D) + cube_faces(D) = 17'. This module derives mass ratios from that torsion rather than defining them as formulas.
proof idea
The term proof refines the goal into a three-way conjunction. Each conjunct is solved by rewriting the rung difference using the canonical form under the hypothesis that the ledger torsion equals generationTorsion, then closing by reflexivity. The rewrite invokes the rungDiff_canonical property of the RSLedger structure.
why it matters
This result is central because it shows masses are derived from torsion structure, as stated in the doc comment. It supports the phi-ladder mass formula with the specific rung differences 11, 17, 6 and connects to the T8 forcing of D=3 dimensions together with the geometric origin of torsion from cube combinatorics. No downstream uses appear yet, but the declaration closes the gap between geometric torsion and observable mass hierarchies in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.