structure
definition
ReionizationCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Cosmology.ReionizationHistoryFromRS on GitHub at line 42.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
39theorem redshift_pos (k : ℕ) : 0 < boundaryRedshift k :=
40 pow_pos phi_pos k
41
42structure ReionizationCert where
43 five_epochs : Fintype.card ReionizationEpoch = 5
44 phi_ratio : ∀ k, boundaryRedshift (k + 1) / boundaryRedshift k = phi
45 boundary_always_pos : ∀ k, 0 < boundaryRedshift k
46
47noncomputable def reionizationCert : ReionizationCert where
48 five_epochs := reionizationEpoch_count
49 phi_ratio := redshift_ratio
50 boundary_always_pos := redshift_pos
51
52end IndisputableMonolith.Cosmology.ReionizationHistoryFromRS