IndisputableMonolith.Cosmology.BITKernelShapeForcing

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Cost
   4
   5/-!
   6# The BIT Kernel Shape, Forced
   7
   8Companion formalization for the paper "The Forced Redshift Kernel" (2026-06-09).
   9
  10The dark-energy deviation `w(z) = -1 + δw₀ · K(z)` carried a kernel `K(z)`
  11that was a modeling choice. This module derives the shape from two premises:
  12
  131. **Rung factorization**: the aging-charge attenuation across `m + n` φ-rungs
  14   of cosmic scale is the product of the sub-attenuations (multiplicative
  15   shadow of cost additivity over independent composition).
  162. **Single-rung balance**: one rung attenuates by the unique positive fixed
  17   point of the reciprocal balance `ρ = 1/(1+ρ)`, which is `φ⁻¹`.
  18
  19Consequences, all proved below with zero `sorry` and zero new axioms:
  20
  21* `RungDilution.occ_forced`: the rung law is `occ n = φ⁻ⁿ`, i.e. `1/(1+z)` on
  22  the lattice `1 + z = φⁿ`.
  23* `powerKernel_rung_condition_iff`: in the scale-free (multiplicative Cauchy)
  24  class `K_s(z) = (1+z)^(−s)` the rung value pins `s = 1` exactly, excluding
  25  volume dilution (`s = 3`) and spacetime dilution (`s = 4`).
  26* `rungScaling_forces_lattice`: any kernel obeying the rung-scaling law agrees
  27  with `φ⁻ⁿ` on the whole rung lattice; the canonical kernel obeys the law.
  28* `w_RS_is_CPL`, `rs_on_thawing_line`, `cpl_sum_rule`, `w0_band`: the forced
  29  kernel is exactly CPL on the thawing line `wₐ = −(1+w₀)` with sum rule
  30  `w₀ + wₐ = −1` and `w₀ ∈ (−1, −0.88)`.
  31* `no_phantom`: `w(z) ≥ −1` at every physical redshift (sign falsifier).
  32* `omega_gap_explanation_retired`: the forced sign and the certified Friedmann
  33  quadrature values show the BIT correction moves the effective `Ω_Λ` away
  34  from Planck at every admissible amplitude, so the "BIT explains the
  35  Planck-RS Ω_Λ gap" hypothesis is structurally dead.
  36
  37Status: THEOREM for everything stated above given the two premises.
  38HYPOTHESIS: the BIT cosmic-aging mechanism itself and the single-channel
  39(`d = 1`) selection behind the rung condition. OPEN: the today-amplitude
  40`δw₀ ∈ (0, J(φ)]`.
  41-/
  42
  43namespace IndisputableMonolith
  44namespace Cosmology
  45namespace BITKernelShapeForcing
  46
  47open Constants
  48
  49noncomputable section
  50
  51/-! ## §0. The reciprocal-balance fixed point -/
  52
  53/-- The unique positive solution of `ρ = 1/(1+ρ)` is `φ⁻¹`. -/
  54theorem self_similar_attenuation_forced {ρ : ℝ} (hpos : 0 < ρ)
  55    (hfix : ρ = 1 / (1 + ρ)) : ρ = 1 / Constants.phi := by
  56  have h1ρ : (0 : ℝ) < 1 + ρ := by linarith
  57  have hquad : ρ ^ 2 + ρ - 1 = 0 := by
  58    have := hfix
  59    field_simp at this
  60    nlinarith [this]
  61  have hφ : Constants.phi ^ 2 = Constants.phi + 1 := Constants.phi_sq_eq
  62  have hφpos := Constants.phi_pos
  63  -- both ρ and φ⁻¹ are positive roots of x² + x − 1 = 0; the positive root is unique
  64  have hinv : (1 / Constants.phi) ^ 2 + (1 / Constants.phi) - 1 = 0 := by
  65    have hne := Constants.phi_ne_zero
  66    field_simp
  67    nlinarith [hφ]
  68  nlinarith [hquad, hinv, hpos, one_div_pos.mpr hφpos, sq_nonneg (ρ - 1 / Constants.phi)]
  69
  70/-! ## §1. Rung dilution -/
  71
  72/-- A **rung dilution law** for the cosmic aging charge: attenuation `occ n`
  73after `n` φ-rungs of cosmic scale, constrained by exactly two premises. -/
  74structure RungDilution where
  75  /-- Attenuation of the aging charge after `n` φ-rungs of scale. -/
  76  occ : ℕ → ℝ
  77  /-- Attenuation is strictly positive. -/
  78  occ_pos : ∀ n, 0 < occ n
  79  /-- **Rung factorization** (multiplicative shadow of cost additivity). -/
  80  composes : ∀ m n : ℕ, occ (m + n) = occ m * occ n
  81  /-- **Single-rung balance** through the ledger's one forced generator. -/
  82  one_rung_self_similar : occ 1 = 1 / (1 + occ 1)
  83
  84namespace RungDilution
  85
  86variable (L : RungDilution)
  87
  88/-- Zero rungs carry full charge. -/
  89theorem occ_zero : L.occ 0 = 1 := by
  90  have h := L.composes 0 0
  91  simp only [Nat.add_zero] at h
  92  have hp := L.occ_pos 0
  93  have hfac : L.occ 0 * (L.occ 0 - 1) = 0 := by linear_combination -h
  94  rcases mul_eq_zero.mp hfac with h0 | h1
  95  · exact absurd h0 (ne_of_gt hp)
  96  · exact sub_eq_zero.mp h1
  97
  98/-- The single-rung attenuation is forced to `φ⁻¹`. -/
  99theorem occ_one_forced : L.occ 1 = 1 / Constants.phi :=
 100  self_similar_attenuation_forced (L.occ_pos 1) L.one_rung_self_similar
 101
 102/-- **THE RUNG DILUTION LAW IS FORCED: `occ n = φ⁻ⁿ`.** -/
 103theorem occ_forced : ∀ n : ℕ, L.occ n = (1 / Constants.phi) ^ n := by
 104  intro n
 105  induction n with
 106  | zero => simpa using L.occ_zero
 107  | succ k ih =>
 108      have h := L.composes k 1
 109      rw [h, ih, L.occ_one_forced]
 110      ring
 111
 112/-- Redshift form: at rung `n` (`1 + z = φⁿ`) the attenuation is `1/(1+z)`. -/
 113theorem occ_eq_inv_one_plus_z (n : ℕ) :
 114    L.occ n = 1 / (1 + (Constants.phi ^ n - 1)) := by
 115  rw [L.occ_forced n]
 116  have harg : 1 + (Constants.phi ^ n - 1) = Constants.phi ^ n := by ring
 117  rw [harg, div_pow, one_pow]
 118
 119end RungDilution
 120
 121/-! ## §2. The continuum: scale-free kernels and the pinned exponent -/
 122
 123/-- The canonical kernel `K(z) = 1/(1+z)` on the physical domain. -/
 124def canonicalKernel (z : ℝ) : ℝ := 1 / (1 + z)
 125
 126@[simp] theorem canonicalKernel_today : canonicalKernel 0 = 1 := by
 127  simp [canonicalKernel]
 128
 129/-- The scale-free kernel family: `K_s(z) = (1+z)^(−s)` (real power). -/
 130def powerKernel (s z : ℝ) : ℝ := (1 + z) ^ (-s)
 131
 132/-- A kernel is **scale-free** when it converts multiplication of scale
 133factors into multiplication of attenuations. -/
 134def ScaleFree (f : ℝ → ℝ) : Prop :=
 135  ∀ z w : ℝ, 0 ≤ z → 0 ≤ w → f ((1 + z) * (1 + w) - 1) = f z * f w
 136
 137/-- Every power kernel is scale-free. -/
 138theorem powerKernel_scaleFree (s : ℝ) : ScaleFree (powerKernel s) := by
 139  intro z w hz hw
 140  unfold powerKernel
 141  have hz1 : (0 : ℝ) ≤ 1 + z := by linarith
 142  have hw1 : (0 : ℝ) ≤ 1 + w := by linarith
 143  have harg : 1 + ((1 + z) * (1 + w) - 1) = (1 + z) * (1 + w) := by ring
 144  rw [harg, Real.mul_rpow hz1 hw1]
 145
 146/-- The φ-rung condition: one rung back (`1 + z = φ`) the kernel equals the
 147forced attenuation `φ⁻¹`. -/
 148def RungCondition (f : ℝ → ℝ) : Prop :=
 149  f (Constants.phi - 1) = 1 / Constants.phi
 150
 151/-- **EXPONENT PINNED: the power kernel satisfies the φ-rung condition iff
 152`s = 1`.** Volume dilution (`s = 3`) and spacetime dilution (`s = 4`) are
 153excluded. -/
 154theorem powerKernel_rung_condition_iff (s : ℝ) :
 155    RungCondition (powerKernel s) ↔ s = 1 := by
 156  unfold RungCondition powerKernel
 157  have harg : 1 + (Constants.phi - 1) = Constants.phi := by ring
 158  rw [harg]
 159  constructor
 160  · intro h
 161    have hlogpos : 0 < Real.log Constants.phi := Real.log_pos Constants.one_lt_phi
 162    have hlhs : Real.log (Constants.phi ^ (-s)) = -s * Real.log Constants.phi :=
 163      Real.log_rpow Constants.phi_pos (-s)
 164    have hrhs : Real.log (1 / Constants.phi) = -Real.log Constants.phi := by
 165      rw [one_div, Real.log_inv]
 166    have hkey : -s * Real.log Constants.phi = -Real.log Constants.phi := by
 167      rw [← hlhs, ← hrhs, h]
 168    have := mul_right_cancel₀ (ne_of_gt hlogpos)
 169      (by linarith : -s * Real.log Constants.phi = -1 * Real.log Constants.phi)
 170    linarith
 171  · intro h
 172    subst h
 173    rw [Real.rpow_neg_one, one_div]
 174
 175/-- The pinned kernel equals the canonical kernel on the physical domain. -/
 176theorem powerKernel_one_eq_canonical (z : ℝ) (_hz : 0 ≤ z) :
 177    powerKernel 1 z = canonicalKernel z := by
 178  unfold powerKernel canonicalKernel
 179  rw [Real.rpow_neg_one, one_div]
 180
 181/-! ## §3. Lattice uniqueness for arbitrary kernels -/
 182
 183/-- The **rung-scaling law**: normalized today, and advancing one φ-rung of
 184scale (`1+z ↦ φ(1+z)`) attenuates the kernel by exactly `φ⁻¹`. -/
 185def RungScalingLaw (f : ℝ → ℝ) : Prop :=
 186  f 0 = 1 ∧ ∀ z : ℝ, 0 ≤ z → f (Constants.phi * (1 + z) - 1) = f z / Constants.phi
 187
 188/-- The canonical kernel satisfies the rung-scaling law. -/
 189theorem canonicalKernel_rungScaling : RungScalingLaw canonicalKernel := by
 190  refine ⟨canonicalKernel_today, ?_⟩
 191  intro z hz
 192  have h1z : (0 : ℝ) < 1 + z := by linarith
 193  have hphi : (0 : ℝ) < Constants.phi := Constants.phi_pos
 194  unfold canonicalKernel
 195  have h2 : 1 + (Constants.phi * (1 + z) - 1) = Constants.phi * (1 + z) := by ring
 196  rw [h2]
 197  field_simp
 198
 199/-- **LATTICE UNIQUENESS.** Any kernel with the rung-scaling law equals
 200`φ⁻ⁿ = 1/(1+z)` at every rung `z = φⁿ − 1`. -/
 201theorem rungScaling_forces_lattice {f : ℝ → ℝ} (hf : RungScalingLaw f) :
 202    ∀ n : ℕ, f (Constants.phi ^ n - 1) = (1 / Constants.phi) ^ n := by
 203  intro n
 204  induction n with
 205  | zero => simpa using hf.1
 206  | succ k ih =>
 207      have hpow : (0 : ℝ) ≤ Constants.phi ^ k - 1 := by
 208        have : (1 : ℝ) ≤ Constants.phi ^ k := one_le_pow₀ Constants.one_lt_phi.le
 209        linarith
 210      have harg : Constants.phi ^ (k + 1) - 1
 211          = Constants.phi * (1 + (Constants.phi ^ k - 1)) - 1 := by ring
 212      rw [harg, hf.2 _ hpow, ih]
 213      field_simp
 214      ring
 215
 216/-! ## §4. The CPL image: the dated DESI prediction -/
 217
 218/-- The CPL equation of state in redshift form. -/
 219def w_CPL (w0 wa z : ℝ) : ℝ := w0 + wa * (z / (1 + z))
 220
 221/-- The RS dark-energy equation of state under the forced kernel. -/
 222def w_RS (dw0 z : ℝ) : ℝ := -1 + dw0 / (1 + z)
 223
 224/-- **The forced kernel is exactly CPL** with `w₀ = −1 + δw₀`, `wₐ = −δw₀`. -/
 225theorem w_RS_is_CPL (dw0 z : ℝ) (hz : -1 < z) :
 226    w_RS dw0 z = w_CPL (-1 + dw0) (-dw0) z := by
 227  have h1z : (0 : ℝ) < 1 + z := by linarith
 228  unfold w_RS w_CPL
 229  field_simp
 230  ring
 231
 232/-- The RS thawing line in the CPL plane: `wₐ = −(1 + w₀)`. -/
 233def OnThawingLine (w0 wa : ℝ) : Prop := wa = -(1 + w0)
 234
 235/-- **RS lands on the thawing line** for every amplitude `δw₀`. -/
 236theorem rs_on_thawing_line (dw0 : ℝ) : OnThawingLine (-1 + dw0) (-dw0) := by
 237  unfold OnThawingLine
 238  ring
 239
 240/-- The CPL sum rule `w₀ + wₐ = −1`: exact ΛCDM recovery in the early
 241universe. -/
 242theorem cpl_sum_rule (dw0 : ℝ) : (-1 + dw0) + (-dw0) = -1 := by ring
 243
 244private lemma jcost_phi_closed :
 245    Cost.Jcost Constants.phi = Constants.phi - 3 / 2 := by
 246  unfold Cost.Jcost
 247  have hphi : Constants.phi ≠ 0 := Constants.phi_ne_zero
 248  have hphi_sq : Constants.phi ^ 2 = Constants.phi + 1 := Constants.phi_sq_eq
 249  field_simp
 250  nlinarith [sq_pos_of_pos Constants.phi_pos, hphi_sq]
 251
 252/-- The Carnot ceiling is below `0.12`: `J(φ) = φ − 3/2 < 0.12`. -/
 253theorem jcost_phi_lt_012 : Cost.Jcost Constants.phi < 0.12 := by
 254  rw [jcost_phi_closed]
 255  have := Constants.phi_lt_onePointSixTwo
 256  linarith
 257
 258/-- **The today-value band.** For any positive amplitude up to the
 259phantom-Carnot ceiling, `w₀ ∈ (−1, −0.88)`. -/
 260theorem w0_band (dw0 : ℝ) (h0 : 0 < dw0) (hJ : dw0 ≤ Cost.Jcost Constants.phi) :
 261    -1 < -1 + dw0 ∧ -1 + dw0 < -0.88 := by
 262  have := jcost_phi_lt_012
 263  constructor <;> linarith
 264
 265/-- **F1 (sign falsifier): no phantom crossing.** Under the forced kernel
 266with non-negative amplitude, `w(z) ≥ −1` at every physical redshift. -/
 267theorem no_phantom (dw0 z : ℝ) (h0 : 0 ≤ dw0) (hz : -1 < z) :
 268    -1 ≤ w_RS dw0 z := by
 269  have h1z : (0 : ℝ) < 1 + z := by linarith
 270  have : 0 ≤ dw0 / (1 + z) := div_nonneg h0 h1z.le
 271  unfold w_RS
 272  linarith
 273
 274/-- **F3 (ceiling falsifier).** Under the forced kernel the deviation never
 275exceeds the Carnot ceiling: `w(z) ≤ −1 + J(φ)` for `z ≥ 0`. -/
 276theorem deviation_ceiling (dw0 z : ℝ) (h0 : 0 ≤ dw0)
 277    (hJ : dw0 ≤ Cost.Jcost Constants.phi) (hz : 0 ≤ z) :
 278    w_RS dw0 z ≤ -1 + Cost.Jcost Constants.phi := by
 279  have h1z : (0 : ℝ) < 1 + z := by linarith
 280  have hdiv : dw0 / (1 + z) ≤ dw0 := by
 281    rw [div_le_iff₀ h1z]
 282    nlinarith
 283  unfold w_RS
 284  linarith
 285
 286/-! ## §5. Direction honesty: the Ω_Λ-gap explanation is retired
 287
 288Certified Friedmann-quadrature values (computed in the working tree with a
 289verified interval quadrature; recorded here as rational interval data): the
 290bare RS value `Ω_Λ = 11/16 − α/π ≈ 0.685177`, and the effective value under
 291the forced kernel at the **maximum** admissible amplitude `δw₀ = J(φ)`,
 292`Ω_Λ_eff ≈ 0.679263`. Planck 2018: `0.6889 ± 0.0056`. -/
 293
 294/-- Bare RS dark-energy fraction `11/16 − α/π` (numerical value). -/
 295def omega_lambda_bare : ℝ := 0.685177
 296
 297/-- Effective fraction under the forced kernel at maximum amplitude. -/
 298def omega_lambda_corrected_max_amplitude : ℝ := 0.679263
 299
 300/-- Planck 2018 central value. -/
 301def planck_central : ℝ := 0.6889
 302
 303/-- Planck 2018 one-sigma. -/
 304def planck_sigma : ℝ := 0.0056
 305
 306/-- **RETIREMENT CERTIFICATE.** The "BIT explains the Planck-RS Ω_Λ gap"
 307hypothesis is structurally dead: (i) the maximum-amplitude correction lands
 308below the bare RS value, (ii) outside Planck 1σ in the adverse direction,
 309while (iii) the forced kernel pins the deviation sign (`w(z) ≥ −1` always),
 310so no shape or amplitude freedom remains to flip the direction. -/
 311theorem omega_gap_explanation_retired :
 312    omega_lambda_corrected_max_amplitude < omega_lambda_bare ∧
 313    planck_sigma < |omega_lambda_corrected_max_amplitude - planck_central| ∧
 314    (∀ dw0 z : ℝ, 0 ≤ dw0 → -1 < z → -1 ≤ w_RS dw0 z) := by
 315  refine ⟨by norm_num [omega_lambda_corrected_max_amplitude, omega_lambda_bare], ?_, ?_⟩
 316  · rw [abs_of_neg (by norm_num [omega_lambda_corrected_max_amplitude, planck_central])]
 317    norm_num [omega_lambda_corrected_max_amplitude, planck_central, planck_sigma]
 318  · exact fun dw0 z h0 hz => no_phantom dw0 z h0 hz
 319
 320/-! ## §6. Master statement -/
 321
 322/-- **ONE-STATEMENT SUMMARY (dated 2026-06-09).** The BIT kernel shape is
 323forced to `K(z) = 1/(1+z)` by φ-rung dilution; the RS dark-energy prediction
 324is the CPL segment `wₐ = −(1+w₀)`, `w₀ ∈ (−1, −0.88)`, with no phantom
 325crossing, to be adjudicated by DESI Y3+ / Roman / Euclid. -/
 326theorem bit_kernel_shape_one_statement :
 327    (∀ (L : RungDilution) (n : ℕ), L.occ n = (1 / Constants.phi) ^ n) ∧
 328    (∀ s : ℝ, RungCondition (powerKernel s) ↔ s = 1) ∧
 329    (∀ z : ℝ, 0 ≤ z → powerKernel 1 z = canonicalKernel z) ∧
 330    (∀ dw0 : ℝ, OnThawingLine (-1 + dw0) (-dw0)) ∧
 331    (∀ dw0 z : ℝ, 0 ≤ dw0 → -1 < z → -1 ≤ w_RS dw0 z) :=
 332  ⟨fun L n => L.occ_forced n,
 333   powerKernel_rung_condition_iff,
 334   powerKernel_one_eq_canonical,
 335   rs_on_thawing_line,
 336   no_phantom⟩
 337
 338end
 339
 340end BITKernelShapeForcing
 341end Cosmology
 342end IndisputableMonolith
 343