module module

`IndisputableMonolith.Cosmology.BaryonHigherOrder`

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

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cosmology.BaryonAsymmetryExact module_import

declarations in this module (22)

theorem eta_B_leading L71
theorem eta_B_leading_pos L74
def N_sph L80
theorem N_sph_pos L83
theorem N_sph_gt_one L86
def delta_washout L91
theorem delta_pos L94
theorem delta_lt_one L97
def correction_factor L105
theorem correction_factor_pos L108
theorem correction_factor_lt_one L113
theorem correction_factor_in_interval L118
def eta_B_corrected L125
theorem eta_B_corrected_pos L129
theorem corrected_lt_leading L134
theorem corrected_in_range L144
theorem correction_moves_toward_cmb L151
theorem correction_is_8tick_rung L158
theorem corrected_decomposition L162
theorem correction_term_rung L168
structure BaryonCorrectionCert L182
theorem baryon_correction_cert L204