pith. sign in
module module high

IndisputableMonolith.RecogSpec.RSLedger

show as:
view Lean formalization →

RSLedger encodes the three generations of fermions through torsion differences and sector base rungs on the phi-ladder. Derivations of lepton mass ratios and geometric mixing angles cite it directly. The module supplies the required ledger definitions and supporting lemmas for downstream tier calculations.

claimThe module defines $RSLedger$ together with $Generation$, $FermionSector$, $sectorBaseRung$, and the three torsion differences $torsionDiff_{21}$, $torsionDiff_{31}$, $torsionDiff_{32}$ that label the muon, tau, and their ratios on the recognition ladder.

background

Recognition Science places fermions on the cubic ledger whose geometry is supplied by the imported Constants and AlphaDerivation modules; the former fixes the base time quantum while the latter extracts $4π$ from vertex deficits. RecogSpec.Core supplies the underlying recognition composition law. The present module introduces the concrete objects Generation (three families), generationTorsion, and FermionSector with its base rung, all expressed in the native phi-ladder units.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

RSLedger supplies the tier structure consumed by MassLawFromLedger, which extracts the canonical ratios $mu/e = φ^{11}$, $tau/e = φ^{17}$, $tau/mu = φ^6$, and by RSBridge, which obtains CKM angles from the same geometric couplings. It therefore closes the fermion-generation step required for both the mass-law and mixing-angle derivations in the Recognition framework.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (22)