module module

`IndisputableMonolith.Cosmology.EtaBExactRungDerivation`

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 (1)

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

IndisputableMonolith module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Foundation.IntegrationGap module_import

declarations in this module (20)

def bitFlipCount0 L43
def torsionGap01 L47
def fermionicDOF L50
theorem fermionicDOF_eq L52
def eta_B_rung_from_dimension L59
theorem eta_B_rung_from_dimension_at_D3 L62
def eta_B_rung_from_chirality L69
theorem eta_B_rung_from_chirality_eq L72
def eta_B_rung_from_fermionic L77
theorem eta_B_rung_from_fermionic_eq L80
theorem witnesses_AB_agree L88
theorem witnesses_AC_agree L93
theorem witnesses_BC_agree L98
theorem chirality_product_equals_gap_minus_one L106
theorem fermionic_half_equals_gap L115
theorem D1_counterfactual_rung L124
theorem D2_counterfactual_rung L128
theorem D5_counterfactual_rung L132
structure EtaBExactRungCert L138
theorem etaBExactRungCert L159