RSLedger
plain-language theorem explainer
The RSLedger structure augments a base ledger with a torsion map from the three generations to integers and base rungs for leptons, up quarks, and down quarks. Mass hierarchy researchers in Recognition Science cite it to obtain rung assignments whose differences yield phi-powered mass ratios. The definition is a direct packaging of these three fields with no separate proof.
Claim. A structure consisting of a base ledger, a map sending each generation to an integer torsion offset, and a map sending each fermion sector to an integer base rung. The full rung for a given sector and generation equals the sector base rung plus the generation torsion.
background
Recognition Science places fermion masses on a phi-ladder where mass scales as phi to the rung power. The module supplies the rich ledger to encode rung differences that arise from geometry rather than being inserted by hand. Torsion offsets come from D=3 cube combinatorics: zero for the ground generation, eleven for the edge-dressed generation, and seventeen for the face-plus-edge generation. Base rungs are fixed at two for leptons and four for each quark sector. The upstream rung constant supplies the integer step size used in the mass formula.
proof idea
The declaration is a structure definition that directly assembles the ledger, torsion function, and base-rung function. Later definitions inside the same file compute the composite rung as base plus torsion and prove that rung differences reduce exactly to torsion differences by ring simplification.
why it matters
This structure supplies the data layer required for deriving inter-generation mass ratios from cube geometry in the Recognition framework. It implements the rung assignment step that precedes the phi-ladder mass formula and the T7 eight-tick octave. The module doc states that torsion values {0, 11, 17} produce the ratios phi^11, phi^17, and phi^6. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.