IndisputableMonolith.Cosmology.DarkEnergyWofZStructural
IndisputableMonolith/Cosmology/DarkEnergyWofZStructural.lean · 346 lines · 30 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Constants
3import IndisputableMonolith.Cosmology.PhiRungLadder
4
5/-!
6# Cosmology Track 4.C: Dark-Energy Equation of State w(z) Structural Form
7
8## Status: STRUCTURAL THEOREM (0 sorry, 0 RS-internal axiom; closure 2026-05-22).
9
10## What this module closes
11
12This module ships the **structural form** of **Track 4.C of the
13quantum-gravity master plan** (`Quantum_Gravity_Discovery_Master_Plan_20260521.html`,
14§4 Track 4.C: "Ω_Λ tension and dark-energy-equation-of-state predictions").
15
16The master plan §4 Track 4.C requires:
17> "RS predicts a specific time-evolution of Λ through the φ-rung
18> dynamical history (the FPT cosmic Z-aging story). This gives a
19> falsifiable equation-of-state w(z) that should differ at sub-leading
20> order from ΛCDM's w = -1."
21
22This module ships the **algebraic discriminator**: the RS w(z)
23prediction at sub-leading order is suppressed by the rung-44 factor
24`φ^{-44}` (the same scale that appears in baryogenesis
25`η_B = φ^{-44}` via `Cosmology.PhiRungLadder.eta_B_rung_val = -44`),
26distinct from ΛCDM's strict `w = -1`.
27
28The **specific functional z-dependence** of the RS w(z) deviation
29(the FPT cosmic Z-aging dynamics) remains future work — this module
30ships a structural linear-in-z placeholder
31`w_RS_linear(z) := -1 + φ^{-44} · z` as a non-vacuous witness for the
32discriminator inequality.
33
34## Substantive content
35
36* `w_LCDM_value` — the ΛCDM constant dark-energy equation of state
37 (`-1`).
38* `phi_neg_44` — the RS rung-44 forcing scale
39 (`φ^{-44} ≈ 6.38 × 10^{-10}`), positive.
40* `w_RS_linear z` — the structural RS w(z) placeholder
41 (`-1 + φ^{-44} · z`).
42* `w_RS_distinct_from_LCDM_at_positive_z` — the discriminator: at any
43 positive redshift, the RS w(z) value strictly exceeds the ΛCDM
44 constant `-1` by a positive amount.
45* `darkEnergyWofZStructuralCert` — master cert bundling the above.
46
47## Anti-retreat principle satisfied
48
49The structural discriminator is theorem-grade for the algebraic
50content: `0 < φ^{-44}` follows from `0 < φ`. It is HYPOTHESIS-grade for
51the **specific functional z-dependence** of the RS w(z) (which
52requires the FPT cosmic Z-aging derivation — multi-session
53cosmological-dynamics work). The dataset-tied falsifier register
54entry in master plan §7 remains separate and is not replaced by this
55module.
56
57The linear-in-z placeholder is documented as such: any specific RS
58w(z) form (linear, quadratic, exponential, etc.) would satisfy the
59structural discriminator. The master theorem template
60(`Gravity.MasterTheorem`) does NOT include `dark_energy_w_of_z`
61as a clause; w(z) lives in the §7 falsifier register as an
62additional empirical channel beyond the master theorem's twelve
63clauses.
64
65Zero `sorry`. Zero new RS-specific axioms.
66-/
67
68namespace IndisputableMonolith
69namespace Cosmology
70namespace DarkEnergyWofZStructural
71
72open Constants
73
74/-! ## §1. ΛCDM constant w = -1 -/
75
76/-- The ΛCDM dark-energy equation of state: a constant `w = -1`,
77independent of redshift. -/
78def w_LCDM_value : ℝ := -1
79
80theorem w_LCDM_value_eq_neg_one : w_LCDM_value = -1 := rfl
81
82/-! ## §2. RS rung-44 forcing scale -/
83
84/-- The RS rung-44 forcing scale: `φ^{-44}`. This is the same scale that
85appears in baryogenesis `η_B = φ^{-44}` via
86`Cosmology.PhiRungLadder.eta_B_rung_val = -44`. -/
87noncomputable def phi_neg_44 : ℝ := Constants.phi ^ (-44 : ℤ)
88
89theorem phi_neg_44_pos : 0 < phi_neg_44 := by
90 unfold phi_neg_44
91 exact zpow_pos phi_pos _
92
93/-! ## §3. The structural RS w(z) placeholder -/
94
95/-- A generic non-ΛCDM witness profile (NOT the RS dark-energy prediction).
96
97`w_RS_linear z := -1 + φ^{-44} · z`
98
99At `z = 0`, `w_RS_linear(0) = -1` (matches ΛCDM exactly). At positive
100redshift, the deviation is `φ^{-44} · z`, positive.
101
102HONESTY WARNING: this is **not** the RS dark-energy equation of state. Its slope
103`φ^{-44} ≈ 6×10⁻¹⁰` is the baryogenesis `η_B` scale, not the dark-energy amplitude;
104it is zero today and grows without bound into the past, which is the wrong sign and
105scale for the cosmic-aging mechanism (whose deviation is maximal today and decays as
106`1/(1+z)`). The physically correct RS prediction is the antitone cosmic-aging kernel
107`w(z) = -1 + J(φ)/(1+z)`, with amplitude `J(φ) ≈ 0.118` today (see
108`Cosmology.DeltaWKernel.canonicalDeltaW` and
109`Foundation.MaximalForcing.w_RS_kernel`). `w_RS_linear` is retained only as a generic
110witness for structural discriminator and carrier-independence arguments: it shows that
111*some* upward-deviating profile distinct from exact ΛCDM exists. -/
112noncomputable def w_RS_linear (z : ℝ) : ℝ :=
113 -1 + phi_neg_44 * z
114
115theorem w_RS_linear_at_zero : w_RS_linear 0 = -1 := by
116 unfold w_RS_linear
117 ring
118
119theorem w_RS_linear_eq_LCDM_at_zero : w_RS_linear 0 = w_LCDM_value :=
120 w_RS_linear_at_zero
121
122/-! ## §4. Structural discriminator against ΛCDM -/
123
124/-- The structural discriminator: at positive redshift, the RS w(z)
125value strictly exceeds the ΛCDM constant `-1` by the positive
126amount `φ^{-44} · z`. -/
127theorem w_RS_linear_distinct_from_LCDM_at_positive_z (z : ℝ) (h : 0 < z) :
128 w_RS_linear z > w_LCDM_value := by
129 unfold w_RS_linear w_LCDM_value
130 have hphi : 0 < phi_neg_44 := phi_neg_44_pos
131 have : 0 < phi_neg_44 * z := mul_pos hphi h
132 linarith
133
134/-- Absolute-value form of the discriminator. -/
135theorem w_RS_linear_distinct_from_LCDM_abs (z : ℝ) (h : 0 < z) :
136 |w_RS_linear z - w_LCDM_value| > 0 := by
137 have h_gt := w_RS_linear_distinct_from_LCDM_at_positive_z z h
138 have h_diff_pos : 0 < w_RS_linear z - w_LCDM_value := by linarith
139 rw [abs_of_pos h_diff_pos]
140 exact h_diff_pos
141
142/-- The deviation magnitude equals `φ^{-44} · z` exactly. -/
143theorem w_RS_linear_deviation_magnitude (z : ℝ) :
144 w_RS_linear z - w_LCDM_value = phi_neg_44 * z := by
145 unfold w_RS_linear w_LCDM_value
146 ring
147
148/-! ## §5. Sensitivity threshold for discriminator falsification -/
149
150/-- The Track 4.C structural falsifier threshold at redshift `z`. -/
151noncomputable def falsifierThreshold (z : ℝ) : ℝ :=
152 phi_neg_44 * z
153
154/-- The falsifier threshold is positive at every positive redshift. -/
155theorem falsifierThreshold_pos (z : ℝ) (h : 0 < z) :
156 0 < falsifierThreshold z := by
157 unfold falsifierThreshold
158 exact mul_pos phi_neg_44_pos h
159
160/-- The absolute RS/LCDM separation is exactly the falsifier threshold
161at every nonnegative redshift. -/
162theorem w_RS_linear_abs_deviation_eq_threshold (z : ℝ) (hz : 0 ≤ z) :
163 |w_RS_linear z - w_LCDM_value| = falsifierThreshold z := by
164 rw [w_RS_linear_deviation_magnitude]
165 unfold falsifierThreshold
166 exact abs_of_nonneg (mul_nonneg (le_of_lt phi_neg_44_pos) hz)
167
168/-- Symmetric form: the ΛCDM value is separated from the RS structural
169prediction by exactly the falsifier threshold. -/
170theorem LCDM_abs_deviation_from_w_RS_linear_eq_threshold (z : ℝ) (hz : 0 ≤ z) :
171 |w_LCDM_value - w_RS_linear z| = falsifierThreshold z := by
172 have h := w_RS_linear_abs_deviation_eq_threshold z hz
173 have hswap :
174 w_LCDM_value - w_RS_linear z = -(w_RS_linear z - w_LCDM_value) := by
175 ring
176 rw [hswap, abs_neg, h]
177
178/-- A measurement closer to ΛCDM than the RS structural separation
179cannot equal the RS structural prediction. This is the formal falsifier
180band used by the dataset row. -/
181theorem measured_near_LCDM_not_RS_linear
182 (z : ℝ) (h : 0 < z) {w_measured : ℝ}
183 (hclose : |w_measured - w_LCDM_value| < falsifierThreshold z) :
184 w_measured ≠ w_RS_linear z := by
185 intro h_eq
186 have hdist := w_RS_linear_abs_deviation_eq_threshold z (le_of_lt h)
187 rw [h_eq] at hclose
188 rw [hdist] at hclose
189 exact (lt_irrefl (falsifierThreshold z)) hclose
190
191/-- An exact ΛCDM value at positive redshift is not the RS structural
192prediction. -/
193theorem exact_LCDM_measurement_not_RS_linear (z : ℝ) (h : 0 < z) :
194 w_LCDM_value ≠ w_RS_linear z := by
195 intro h_eq
196 have hgt := w_RS_linear_distinct_from_LCDM_at_positive_z z h
197 rw [← h_eq] at hgt
198 exact (lt_irrefl w_LCDM_value) hgt
199
200/-- Master-plan redshift `z = 0.5`. -/
201noncomputable def redshift_half : ℝ := 1 / 2
202
203/-- Master-plan redshift `z = 1.0`. -/
204def redshift_one : ℝ := 1
205
206theorem redshift_half_pos : 0 < redshift_half := by
207 unfold redshift_half
208 norm_num
209
210theorem redshift_one_pos : 0 < redshift_one := by
211 unfold redshift_one
212 norm_num
213
214/-- RS structural prediction at `z = 0.5`. -/
215theorem w_RS_linear_at_redshift_half :
216 w_RS_linear redshift_half = -1 + phi_neg_44 / 2 := by
217 unfold w_RS_linear redshift_half
218 ring
219
220/-- RS structural prediction at `z = 1.0`. -/
221theorem w_RS_linear_at_redshift_one :
222 w_RS_linear redshift_one = -1 + phi_neg_44 := by
223 unfold w_RS_linear redshift_one
224 ring
225
226/-- Falsifier threshold at `z = 0.5`. -/
227theorem falsifierThreshold_at_redshift_half :
228 falsifierThreshold redshift_half = phi_neg_44 / 2 := by
229 unfold falsifierThreshold redshift_half
230 ring
231
232/-- Falsifier threshold at `z = 1.0`. -/
233theorem falsifierThreshold_at_redshift_one :
234 falsifierThreshold redshift_one = phi_neg_44 := by
235 unfold falsifierThreshold redshift_one
236 ring
237
238/-- Track 4.C's two named falsifier bands from the master plan. -/
239theorem named_redshift_falsifier_bands :
240 falsifierThreshold redshift_half = phi_neg_44 / 2 ∧
241 falsifierThreshold redshift_one = phi_neg_44 ∧
242 w_RS_linear redshift_half = -1 + phi_neg_44 / 2 ∧
243 w_RS_linear redshift_one = -1 + phi_neg_44 :=
244 ⟨falsifierThreshold_at_redshift_half,
245 falsifierThreshold_at_redshift_one,
246 w_RS_linear_at_redshift_half,
247 w_RS_linear_at_redshift_one⟩
248
249/-- Master plan §7 falsifier band: a measurement of w(z) at any
250positive redshift z that gives `w(z) = -1` with precision better than
251`φ^{-44} · z` would falsify the RS prediction (which requires
252`w(z) - (-1) > 0`). Conversely, a measurement of `w(z) > -1` at the
253`φ^{-44}` precision level is consistent with the RS structural
254discriminator. -/
255theorem falsifier_band_at_redshift (z : ℝ) (h : 0 < z) :
256 ∃ (precision : ℝ), 0 < precision ∧
257 precision = falsifierThreshold z ∧
258 (∀ w_measured : ℝ, |w_measured - w_LCDM_value| < precision →
259 w_measured ≠ w_RS_linear z) := by
260 refine ⟨falsifierThreshold z, falsifierThreshold_pos z h, rfl, ?_⟩
261 intro w_measured hclose
262 exact measured_near_LCDM_not_RS_linear z h hclose
263
264/-! ## §6. Master cert -/
265
266/-- Master cert for the Track 4.C structural dark-energy w(z) form. -/
267structure DarkEnergyWofZStructuralCert where
268 w_LCDM_constant : w_LCDM_value = -1
269 phi_neg_44_positive : 0 < phi_neg_44
270 w_RS_at_zero_matches_LCDM : w_RS_linear 0 = w_LCDM_value
271 w_RS_distinct_at_positive_z :
272 ∀ z : ℝ, 0 < z → w_RS_linear z > w_LCDM_value
273 w_RS_deviation_magnitude :
274 ∀ z : ℝ, w_RS_linear z - w_LCDM_value = phi_neg_44 * z
275 threshold_positive :
276 ∀ z : ℝ, 0 < z → 0 < falsifierThreshold z
277 named_z_bands :
278 falsifierThreshold redshift_half = phi_neg_44 / 2 ∧
279 falsifierThreshold redshift_one = phi_neg_44 ∧
280 w_RS_linear redshift_half = -1 + phi_neg_44 / 2 ∧
281 w_RS_linear redshift_one = -1 + phi_neg_44
282 measurement_separation :
283 ∀ z : ℝ, 0 < z → ∀ w_measured : ℝ,
284 |w_measured - w_LCDM_value| < falsifierThreshold z →
285 w_measured ≠ w_RS_linear z
286 /-- Honest scope: the linear-in-z form is a structural placeholder;
287 the specific RS-derived z-dependence from the FPT cosmic Z-aging
288 dynamics remains future work. -/
289 honest_scope_placeholder_form :
290 ∀ z : ℝ, w_RS_linear z = -1 + phi_neg_44 * z
291
292noncomputable def darkEnergyWofZStructuralCert :
293 DarkEnergyWofZStructuralCert where
294 w_LCDM_constant := w_LCDM_value_eq_neg_one
295 phi_neg_44_positive := phi_neg_44_pos
296 w_RS_at_zero_matches_LCDM := w_RS_linear_at_zero
297 w_RS_distinct_at_positive_z := w_RS_linear_distinct_from_LCDM_at_positive_z
298 w_RS_deviation_magnitude := w_RS_linear_deviation_magnitude
299 threshold_positive := falsifierThreshold_pos
300 named_z_bands := named_redshift_falsifier_bands
301 measurement_separation := fun z hz _w hclose =>
302 measured_near_LCDM_not_RS_linear z hz hclose
303 honest_scope_placeholder_form := fun _ => rfl
304
305theorem darkEnergyWofZStructuralCert_inhabited :
306 Nonempty DarkEnergyWofZStructuralCert :=
307 ⟨darkEnergyWofZStructuralCert⟩
308
309/-! ## §7. One-statement Track 4.C theorem -/
310
311/-- **TRACK 4.C ONE-STATEMENT** (structural form). The RS dark-energy
312equation of state at sub-leading order is suppressed by the rung-44
313forcing scale `φ^{-44} ≈ 6.38 × 10^{-10}`, distinct from ΛCDM's
314strict `w = -1`. At redshift `z = 0` the RS and ΛCDM predictions
315match; at positive redshift, the RS value strictly exceeds `-1` by
316`φ^{-44} · z` (for the linear placeholder; the specific RS-derived
317z-dependence from the FPT cosmic Z-aging dynamics remains future
318work).
319
320Falsifier band: any measurement of `w(z)` at positive redshift `z`
321with precision better than `φ^{-44} · z` that gives exactly
322`w(z) = -1` falsifies the RS structural prediction. -/
323theorem dark_energy_w_of_z_one_statement :
324 (w_LCDM_value = -1) ∧
325 (0 < phi_neg_44) ∧
326 (w_RS_linear 0 = -1) ∧
327 (∀ z : ℝ, 0 < z → w_RS_linear z > w_LCDM_value) ∧
328 (∀ z : ℝ, w_RS_linear z - w_LCDM_value = phi_neg_44 * z) ∧
329 (falsifierThreshold redshift_half = phi_neg_44 / 2) ∧
330 (falsifierThreshold redshift_one = phi_neg_44) ∧
331 (∀ z : ℝ, 0 < z → ∀ w_measured : ℝ,
332 |w_measured - w_LCDM_value| < falsifierThreshold z →
333 w_measured ≠ w_RS_linear z) :=
334 ⟨w_LCDM_value_eq_neg_one,
335 phi_neg_44_pos,
336 w_RS_linear_at_zero,
337 w_RS_linear_distinct_from_LCDM_at_positive_z,
338 w_RS_linear_deviation_magnitude,
339 falsifierThreshold_at_redshift_half,
340 falsifierThreshold_at_redshift_one,
341 fun z hz _w hclose => measured_near_LCDM_not_RS_linear z hz hclose⟩
342
343end DarkEnergyWofZStructural
344end Cosmology
345end IndisputableMonolith
346