theorem
proved
delta_w0_max_pos
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Cosmology.BITKernelFamilies on GitHub at line 76.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
73/-- The maximum BIT amplitude is `J(φ) = φ - 3/2 ≈ 0.118`. -/
74def delta_w0_max : ℝ := phi - 3 / 2
75
76theorem delta_w0_max_pos : 0 < delta_w0_max := by
77 unfold delta_w0_max
78 have := phi_gt_onePointFive
79 linarith
80
81theorem delta_w0_max_lt_one : delta_w0_max < 1 := by
82 unfold delta_w0_max
83 have := phi_lt_two
84 linarith
85
86/-- The effective equation of state under BIT. -/
87def w_eff (k : KernelFamily) (z delta_w0 : ℝ) (z0 : ℝ := 1) : ℝ :=
88 -1 + delta_w0 * kernel k z z0
89
90/-- At `z = 0`, `w_eff = -1 + δw_0` for any kernel. -/
91theorem w_eff_at_zero (k : KernelFamily) (delta_w0 z0 : ℝ) :
92 w_eff k 0 delta_w0 z0 = -1 + delta_w0 := by
93 unfold w_eff
94 rw [kernel_at_zero]
95 ring
96
97/-! ## Master certificate -/
98
99/-- **BIT KERNEL FAMILIES MASTER CERTIFICATE.** -/
100structure BITKernelFamiliesCert where
101 kernel_at_zero_one :
102 ∀ k : KernelFamily, ∀ z0 : ℝ, kernel k 0 z0 = 1
103 delta_w0_max_pos :
104 0 < delta_w0_max
105 delta_w0_max_lt_one :
106 delta_w0_max < 1