pith. machine review for the scientific record. sign in
theorem

etaBExactRungCert

proved
show as:
view math explainer →

Baryon asymmetry η_B sits at φ-rung 44.

module
IndisputableMonolith.Cosmology.EtaBExactRungDerivation
domain
Cosmology
line
159 · github
papers citing
1 paper (below)

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Cosmology.EtaBExactRungDerivation on GitHub at line 159.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 156  fermionic_gap_bridge :
 157    ((fermionicDOF / 2 : ℕ) : ℤ) = (integrationGap D : ℤ)
 158
 159theorem etaBExactRungCert : EtaBExactRungCert where
 160  witness_A := eta_B_rung_from_dimension_at_D3
 161  witness_B := eta_B_rung_from_chirality_eq
 162  witness_C := eta_B_rung_from_fermionic_eq
 163  AB_agree := witnesses_AB_agree
 164  AC_agree := witnesses_AC_agree
 165  BC_agree := witnesses_BC_agree
 166  chirality_gap_bridge := chirality_product_equals_gap_minus_one
 167  fermionic_gap_bridge := fermionic_half_equals_gap
 168
 169end EtaBExactRungDerivation
 170end Cosmology
 171end IndisputableMonolith

papers checked against this theorem (showing 1 of 1)