Pith. sign in
module module high

IndisputableMonolith.RecogSpec.RSLedger

show as:
view Lean formalization →

The module encodes the three generations of fermions via ledger tiers, torsion differences, and sector base rungs. Mass-ratio and mixing-angle derivations cite its structure. It supplies a collection of definitions imported from Core and Constants, with no embedded proofs.

claimThe recognition ledger organizes the three generations of fermions through sector base rungs and torsion differences on the $\phi$-ladder.

background

The module resides in RecogSpec and imports Core together with Constants (where $\tau_0$ is the fundamental RS time quantum equal to one tick) and AlphaDerivation (which obtains $\alpha^{-1}$ from vertex deficits of the cubic ledger via Gauss-Bonnet). Its doc-comment states that the content concerns the three generations of fermions. Sibling definitions introduce Generation, FermionSector, sectorBaseRung, and RSLedger together with torsion quantities.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the ledger tiers required by MassLawFromLedger to obtain the canonical ratios $\mu/e=\phi^{11}$, $\tau/e=\phi^{17}$, $\tau/\mu=\phi^6$ and by RSBridge to derive CKM angles from geometric couplings. It therefore fills the organizational step for fermion generations inside 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)