canonicalRSLedger
plain-language theorem explainer
The canonicalRSLedger definition assembles the standard ledger for Recognition Science mass derivations by wiring the generation torsion offsets from cube geometry to the base rungs of each fermion sector. Physicists deriving inter-generation mass ratios cite it as the single source of truth for the {0,11,17} torsion values. The construction is a direct record update that references the precomputed generationTorsion and sectorBaseRung functions.
Claim. The canonical ledger $L$ is the structure whose underlying carrier is the unit type, whose torsion map sends the first generation to 0, the second generation to the number of passive field edges in $D=3$, and the third generation to that quantity plus the number of cube faces, and whose base-rung map assigns 2 to leptons and 4 to both up-quark and down-quark sectors.
background
Recognition Science places particle masses on discrete rungs of the phi-ladder. The RSLedger structure augments a minimal Ledger with a torsion function Generation → ℤ and a base-rung function FermionSector → ℤ; the full rung for any fermion is then baseRung(sector) + torsion(gen). Mass ratios between particles follow directly as m_f / m_g = φ^(r_f - r_g).
proof idea
The definition is a direct structure literal that populates the three fields of RSLedger by referencing the sibling definitions generationTorsion and sectorBaseRung together with a unit carrier. No lemmas or tactics are invoked; the construction is purely by record update.
why it matters
This definition supplies the fixed torsion and rung data consumed by the downstream theorems canonical_massRatiosFromTiers, canonical_massRatio_21, canonical_massRatio_31, and canonical_massRatio_32. It realizes the geometric torsion values {0,11,17} derived from D=3 cube combinatorics that appear in the module documentation and thereby anchors the phi-ladder mass formula with the exponents 11, 17, and 6.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.