module module

`IndisputableMonolith.Cosmology.EtaBIntervalCert`

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.Cosmology.BaryonAsymmetryDerivation module_import

declarations in this module (14)

lemma phi_sq_eq' L53
lemma phi_pow_fib L56
lemma phi_pow_44_fib L74
theorem phi_pow_44_lower L83
theorem phi_pow_44_upper L89
lemma phi_rpow_44 L97
theorem phi_pow_neg44_lower L101
theorem phi_pow_neg44_upper L112
theorem eta_B_interval L124
theorem observed_eta_in_interval L129
theorem forty_four_factorization L136
theorem rung_44_equals_flip_times_torsion L144
structure EtaBCert L152
def etaBCert L160