theorem
proved
efoldCount_eq
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Cosmology.InflatonPotentialStructural on GitHub at line 35.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
32
33/-- e-fold count N_e = 44 (gap-45 ladder). -/
34def efoldCount : ℕ := 44
35theorem efoldCount_eq : efoldCount = 44 := rfl
36
37/-- Slow-roll parameter ε = 1/(2φ⁵). -/
38noncomputable def slowRollEpsilon : ℝ := 1 / (2 * phi ^ 5)
39
40/-- Slow-roll parameter η = 1/φ⁵. -/
41noncomputable def slowRollEta : ℝ := 1 / phi ^ 5
42
43/-- φ⁵ = 5φ + 3 (Fibonacci identity). -/
44theorem phi5_eq : phi ^ 5 = 5 * phi + 3 := by
45 have h2 := phi_sq_eq
46 have h3 : phi ^ 3 = 2 * phi + 1 := by nlinarith
47 have h4 : phi ^ 4 = 3 * phi + 2 := by nlinarith
48 nlinarith
49
50theorem slowRollEpsilon_pos : 0 < slowRollEpsilon := by
51 unfold slowRollEpsilon
52 apply div_pos one_pos
53 exact mul_pos (by norm_num) (pow_pos phi_pos 5)
54
55theorem slowRollEta_pos : 0 < slowRollEta := by
56 unfold slowRollEta
57 exact div_pos one_pos (pow_pos phi_pos 5)
58
59/-- n_s - 1 = -2/45 gives n_s ∈ (0.955, 0.957). -/
60theorem spectralIndex_band :
61 ((0.955 : ℝ) < 1 - 2/45) ∧ (1 - 2/45 < (0.957 : ℝ)) := by
62 refine ⟨?_, ?_⟩ <;> norm_num
63
64structure InflatonCert where
65 five_regimes : Fintype.card InflatonRegime = 5