module module

`IndisputableMonolith.RecogSpec.RSLedger`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (2)

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

IndisputableMonolith.RecogSpec.MassLawFromLedger module_import
IndisputableMonolith.RecogSpec.RSBridge module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Constants.AlphaDerivation module_import
IndisputableMonolith.RecogSpec.Core module_import

declarations in this module (22)

inductive Generation L47
def generationTorsion L59
lemma torsion_first L64
lemma torsion_second L66
lemma torsion_third L69
def torsionDiff L73
lemma torsion_diff_21 L76
lemma torsion_diff_31 L79
lemma torsion_diff_32 L82
inductive FermionSector L88
def sectorBaseRung L99
structure RSLedger L113
def massRatioFromRungs L150
theorem massRatio_21_canonical L155
theorem massRatio_31_canonical L163
theorem massRatio_32_canonical L171
def canonicalRSLedger L181
theorem canonicalRSLedger_torsion L187
theorem canonical_massRatio_21 L191
theorem canonical_massRatio_31 L195
theorem canonical_massRatio_32 L199
theorem massRatios_from_torsion_structure L209