module module

`IndisputableMonolith.Foundation.GapDerivation`

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.Cosmology.EtaBExactRungDerivation module_import
IndisputableMonolith.Cosmology.EtaBPrefactorDerivation module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Foundation.NineParities module_import

declarations in this module (23)

def D L41
def configDim L45
def parityCount L49
def dimensionGap L52
theorem configDim_at_D3 L56
theorem dual_routes L60
theorem parityCount_at_D3 L64
theorem three_D_eq_D_sq L67
theorem parityCount_matches_enumeration L70
theorem gap_at_D3 L76
theorem gap_factors L78
theorem gap_is_lcm L80
theorem coprimality_odd L86
theorem coprimality_even_fails L100
theorem coprime_at_D3 L110
def E_coh_gap L117
theorem E_coh_gap_eq L119
theorem Constants_E_coh_eq_configDim L135
theorem hbar_exponent_eq_configDim L146
def A L154
theorem gap_balance L157
structure Gap45Cert L168
def gap45_cert L179