theorem
proved
darkEnergyModel_count
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Cosmology.DarkEnergyEquationOfStateDepth on GitHub at line 28.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
25 | phantom
26 deriving DecidableEq, Repr, BEq, Fintype
27
28theorem darkEnergyModel_count : Fintype.card DarkEnergyModel = 5 := by decide
29
30/-- δ bound = 1/φ⁵. Using φ⁵ = 5φ + 3. -/
31noncomputable def deltaBound : ℝ := 1 / phi ^ 5
32
33theorem phi5_eq : phi ^ 5 = 5 * phi + 3 := by
34 have h2 := phi_sq_eq
35 have h3 : phi ^ 3 = 2 * phi + 1 := by nlinarith
36 have h4 : phi ^ 4 = 3 * phi + 2 := by nlinarith
37 nlinarith
38
39theorem deltaBound_pos : 0 < deltaBound := by
40 unfold deltaBound
41 exact div_pos one_pos (pow_pos phi_pos 5)
42
43theorem deltaBound_small : deltaBound < 0.1 := by
44 unfold deltaBound
45 have h5 : phi ^ 5 = 5 * phi + 3 := phi5_eq
46 rw [h5]
47 have h_phi_gt : (1.61 : ℝ) < phi := phi_gt_onePointSixOne
48 have h_denom : (11.05 : ℝ) < 5 * phi + 3 := by linarith
49 have h_denom_pos : (0 : ℝ) < 5 * phi + 3 := by linarith
50 rw [div_lt_iff₀ h_denom_pos]
51 nlinarith
52
53structure DarkEnergyEoSDepthCert where
54 five_models : Fintype.card DarkEnergyModel = 5
55 phi5_fibonacci : phi ^ 5 = 5 * phi + 3
56 delta_pos : 0 < deltaBound
57 delta_bounded : deltaBound < 0.1
58