structure
definition
CosmicInflationCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Cosmology.CosmicInflationFromJCost on GitHub at line 32.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
29/-- Inflation ends when J-cost crosses the canonical threshold. -/
30theorem inflation_ends_at_threshold : J 1 = 0 := J_one
31
32structure CosmicInflationCert where
33 five_models : Fintype.card InflationModel = 5
34 reheating_condition : J 1 = 0
35 threshold : CanonicalCert
36
37noncomputable def cosmicInflationCert : CosmicInflationCert where
38 five_models := inflationModelCount
39 reheating_condition := inflation_ends_at_threshold
40 threshold := cert
41
42end IndisputableMonolith.Cosmology.CosmicInflationFromJCost