IndisputableMonolith.Cosmology.RecognitionEventHorizon

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Cosmology: the recognition event horizon `8 φ²` (Phase 9 freeze-out)
   6
   7## Status: THEOREM (0 sorry, 0 RS-internal axiom).
   8
   9This module formalizes the finite recognition horizon that drives the Phase-9
  10accelerated-expansion freeze-out in
  11`scripts/cosmogenesis/freeze_out_dynamics.py`.
  12
  13## The forced setup (no tuned Hubble rate, no coupling)
  14
  15A recognition signal travels one comoving cell per tick at unit scale. The
  16cadence is eight ticks per recognition epoch (T-7), so a signal covers eight
  17comoving cells per epoch at unit scale. The forced self-similar dilation
  18expands the comoving scale by `φ` per epoch (T-6), so the comoving distance a
  19signal covers in epoch `m` is divided by `φ^m`:
  20
  21  `perEpochReach m = 8 / φ^m = 8 (1/φ)^m`.
  22
  23The cumulative comoving reach after infinitely many epochs is the geometric
  24series `∑ 8 (1/φ)^m`. Because the dilation ratio `1/φ` is strictly below one,
  25this series converges to a finite limit, the de Sitter recognition event
  26horizon:
  27
  28  `∑_{m ≥ 0} 8 (1/φ)^m = 8 φ² = 8 (φ + 1) ≈ 20.944` comoving cells.
  29
  30The two ingredients are the cadence `8` (T-7) and the dilation sum `φ²`
  31(T-6, via `φ² = φ + 1`). There is no fitted constant.
  32
  33## What this forces physically
  34
  35The partial reach after any finite number of epochs is strictly below `8 φ²`
  36and increases monotonically toward it. So a comoving separation at or beyond
  37`8 φ²` is never crossed by a recognition signal. Structure on those scales can
  38never be brought into causal contact, so it can never be homogenized: it
  39freezes at its primordial amplitude. Structure below the horizon is eventually
  40crossed and homogenizes. That is the RS `Ω_Λ` freeze-out.
  41
  42## Relation to `VacuumHorizonForcing`
  43
  44`VacuumHorizonForcing` selects the *past-directed particle horizon* for the
  45*vacuum-energy ledger cost*, and there the de Sitter event horizon is excluded
  46because that calculation must not depend on future expansion. This module is a
  47different object: the *future-directed* reach of a signal launched now, which
  48is exactly a de Sitter event horizon. The two are consistent, not in tension:
  49the ledger ground-state cost uses the past cone, the forward freeze-out of
  50structure uses the future cone.
  51-/
  52
  53namespace IndisputableMonolith
  54namespace Cosmology
  55namespace RecognitionEventHorizon
  56
  57open scoped BigOperators
  58
  59/-- Local alias for the golden ratio, following the per-module convention. -/
  60noncomputable abbrev φ : ℝ := Constants.phi
  61
  62lemma phi_pos : 0 < φ := Constants.phi_pos
  63lemma one_lt_phi : 1 < φ := Constants.one_lt_phi
  64lemma phi_sq_eq : φ ^ 2 = φ + 1 := Constants.phi_sq_eq
  65
  66/-! ## §1. The dilation ratio `1/φ` -/
  67
  68lemma phi_inv_pos : 0 < 1 / φ := one_div_pos.mpr phi_pos
  69
  70lemma phi_inv_nonneg : (0 : ℝ) ≤ 1 / φ := le_of_lt phi_inv_pos
  71
  72lemma phi_inv_lt_one : 1 / φ < 1 := by
  73  rw [div_lt_one phi_pos]; exact one_lt_phi
  74
  75/-! ## §2. Per-epoch reach, cumulative reach, the horizon -/
  76
  77/-- The comoving distance a recognition signal covers in epoch `m`: the cadence
  78`8` (T-7) divided by the forced dilation `φ^m` (T-6). -/
  79noncomputable def perEpochReach (m : ℕ) : ℝ := 8 * (1 / φ) ^ m
  80
  81/-- The de Sitter recognition event horizon forced by φ-dilation: `8 φ²`. -/
  82noncomputable def recognitionEventHorizon : ℝ := 8 * φ ^ 2
  83
  84/-- The cumulative comoving reach after `n` epochs: the partial sum of
  85per-epoch reaches. -/
  86noncomputable def cumulativeReach (n : ℕ) : ℝ :=
  87  ∑ m ∈ Finset.range n, perEpochReach m
  88
  89lemma perEpochReach_pos (k : ℕ) : 0 < perEpochReach k := by
  90  unfold perEpochReach
  91  exact mul_pos (by norm_num) (pow_pos phi_inv_pos k)
  92
  93lemma perEpochReach_summable : Summable perEpochReach :=
  94  (summable_geometric_of_lt_one phi_inv_nonneg phi_inv_lt_one).mul_left 8
  95
  96/-! ## §3. The geometric sum: `∑ (1/φ)^m = φ²` -/
  97
  98/-- The closed-form geometric sum of the dilation ratio. With ratio `1/φ < 1`,
  99`∑_{m ≥ 0} (1/φ)^m = (1 - 1/φ)⁻¹`, and `(1 - 1/φ)⁻¹ = φ²` follows from the
 100self-similar identity `φ² = φ + 1`. -/
 101theorem tsum_phi_inv_pow : ∑' m : ℕ, (1 / φ) ^ m = φ ^ 2 := by
 102  rw [tsum_geometric_of_lt_one phi_inv_nonneg phi_inv_lt_one]
 103  -- Goal: (1 - 1/φ)⁻¹ = φ ^ 2
 104  have hφ : φ ≠ 0 := ne_of_gt phi_pos
 105  have hkey : (1 - 1 / φ) * φ ^ 2 = 1 := by
 106    have e1 : (1 - 1 / φ) * φ ^ 2 = φ ^ 2 - φ := by
 107      field_simp
 108    rw [e1, phi_sq_eq]; ring
 109  exact inv_eq_of_mul_eq_one_right hkey
 110
 111/-! ## §4. The total reach equals the horizon -/
 112
 113/-- **THEOREM.** The total cumulative reach over all epochs equals the forced
 114event horizon `8 φ²`. A recognition signal can only ever traverse a finite
 115comoving distance, even given infinitely many epochs. -/
 116theorem tsum_perEpochReach :
 117    ∑' m : ℕ, perEpochReach m = recognitionEventHorizon := by
 118  unfold perEpochReach recognitionEventHorizon
 119  rw [tsum_mul_left, tsum_phi_inv_pow]
 120
 121/-- The horizon in closed form, purely from `φ² = φ + 1`. Numerically
 122`8 (φ + 1) ≈ 20.944` comoving cells, matching the numeric simulation. -/
 123theorem recognitionEventHorizon_eq : recognitionEventHorizon = 8 * (φ + 1) := by
 124  unfold recognitionEventHorizon; rw [phi_sq_eq]
 125
 126/-! ## §5. The partial reach never reaches the horizon -/
 127
 128/-- **THEOREM.** After any finite number of epochs the cumulative reach is
 129strictly below the horizon. A comoving separation at or beyond `8 φ²` is
 130therefore never crossed by a recognition signal, so super-horizon structure can
 131never be homogenized: it freezes at its primordial amplitude. -/
 132theorem cumulativeReach_lt_horizon (n : ℕ) :
 133    cumulativeReach n < recognitionEventHorizon := by
 134  have hsum := perEpochReach_summable
 135  have hsplit := Summable.sum_add_tsum_nat_add n hsum
 136  have htail_summable : Summable (fun i => perEpochReach (i + n)) :=
 137    (summable_nat_add_iff n).2 hsum
 138  have htail_pos : 0 < ∑' i, perEpochReach (i + n) :=
 139    htail_summable.tsum_pos (fun i => le_of_lt (perEpochReach_pos _)) 0
 140      (perEpochReach_pos _)
 141  have key :
 142      cumulativeReach n + ∑' i, perEpochReach (i + n) = recognitionEventHorizon := by
 143    have h := hsplit
 144    rw [tsum_perEpochReach] at h
 145    simpa [cumulativeReach] using h
 146  linarith [htail_pos, key]
 147
 148/-- **THEOREM.** The cumulative reach increases strictly with each epoch:
 149each epoch adds a strictly positive per-epoch reach, so the reach climbs
 150monotonically toward (but never attains) the horizon. -/
 151theorem cumulativeReach_strictMono : StrictMono cumulativeReach := by
 152  apply strictMono_nat_of_lt_succ
 153  intro n
 154  have hstep : cumulativeReach (n + 1) = cumulativeReach n + perEpochReach n := by
 155    simp [cumulativeReach, Finset.sum_range_succ]
 156  rw [hstep]; linarith [perEpochReach_pos n]
 157
 158/-! ## §6. The dyadic freeze rung: the horizon sits between `2^4` and `2^5` -/
 159
 160/-- The horizon strictly exceeds the dyadic rung `2^4 = 16`: `16 < 8 φ²`, equivalently
 161`2 < φ²`, equivalently `1 < φ`. So a self-similar (dyadic) structure at scale `2^4 = 16` is
 162sub-horizon and is homogenized. -/
 163theorem two_pow_four_lt_horizon : (2 : ℝ) ^ 4 < recognitionEventHorizon := by
 164  have h16 : (2 : ℝ) ^ 4 = 16 := by norm_num
 165  rw [recognitionEventHorizon_eq, h16]
 166  linarith [one_lt_phi]
 167
 168/-- The horizon is strictly below the dyadic rung `2^5 = 32`: `8 φ² < 32`, equivalently
 169`φ² < 4`, equivalently `φ < 3` (in fact `φ ≤ 5/3`). So a self-similar (dyadic) structure at
 170scale `2^5 = 32` is super-horizon and freezes at its primordial amplitude. -/
 171theorem horizon_lt_two_pow_five : recognitionEventHorizon < (2 : ℝ) ^ 5 := by
 172  have h32 : (2 : ℝ) ^ 5 = 32 := by norm_num
 173  rw [recognitionEventHorizon_eq, h32]
 174  nlinarith [phi_sq_eq, sq_nonneg (φ - 2)]
 175
 176/-- **THEOREM.** The recognition event horizon `8 φ²` sits strictly between the dyadic rungs
 177`2^4 = 16` and `2^5 = 32`. So a self-similar (dyadic) structure freezes exactly at and above
 178the scale `2^5 = 32` and homogenizes at and below `2^4 = 16`: the freeze break is forced to
 179the fifth dyadic rung, with no fitted scale. This is the arithmetic anchor of the Phase-16
 180freeze-out scale selection (`scripts/cosmogenesis/foam_freeze_out.py`). -/
 181theorem recognitionEventHorizon_between_dyadic_rungs :
 182    (2 : ℝ) ^ 4 < recognitionEventHorizon ∧ recognitionEventHorizon < (2 : ℝ) ^ 5 :=
 183  ⟨two_pow_four_lt_horizon, horizon_lt_two_pow_five⟩
 184
 185/-- The forced dyadic freeze rung: the least exponent `k` with `2^k` above the horizon. -/
 186def dyadicFreezeRung : ℕ := 5
 187
 188/-- **THEOREM.** `dyadicFreezeRung = 5` is the least power-of-two rung strictly above the
 189recognition horizon: `2^5 > 8 φ²`, while every smaller rung `2^k` (`k < 5`) is strictly below
 190it. So the freeze-out selects exactly the dyadic scales at or above `2^5 = 32`. -/
 191theorem dyadicFreezeRung_is_least :
 192    recognitionEventHorizon < (2 : ℝ) ^ dyadicFreezeRung ∧
 193    ∀ k : ℕ, k < dyadicFreezeRung → (2 : ℝ) ^ k < recognitionEventHorizon := by
 194  refine ⟨horizon_lt_two_pow_five, ?_⟩
 195  intro k hk
 196  simp only [dyadicFreezeRung] at hk
 197  have hk4 : k ≤ 4 := by omega
 198  have hnat : (2 : ℕ) ^ k ≤ 2 ^ 4 := Nat.pow_le_pow_right (by norm_num) hk4
 199  have hmono : (2 : ℝ) ^ k ≤ (2 : ℝ) ^ 4 := by exact_mod_cast hnat
 200  exact lt_of_le_of_lt hmono two_pow_four_lt_horizon
 201
 202/-! ## §7. One-statement master theorem -/
 203
 204/-- **RECOGNITION EVENT HORIZON, ONE STATEMENT.** The forced φ-dilation (one
 205φ-rung per eight-tick epoch, T-6 and T-7) gives a finite de Sitter recognition
 206horizon equal to `8 φ² = 8 (φ + 1)`; the cumulative reach converges to it from
 207strictly below and increases monotonically, so any comoving separation at or
 208beyond `8 φ²` is never crossed. This is the law-derived freeze-out mechanism:
 209no tuned Hubble rate and no fitted coupling enter. -/
 210theorem recognition_event_horizon_one_statement :
 211    (∑' m : ℕ, perEpochReach m = recognitionEventHorizon) ∧
 212    recognitionEventHorizon = 8 * (φ + 1) ∧
 213    (∀ n : ℕ, cumulativeReach n < recognitionEventHorizon) ∧
 214    StrictMono cumulativeReach :=
 215  ⟨tsum_perEpochReach, recognitionEventHorizon_eq, cumulativeReach_lt_horizon,
 216    cumulativeReach_strictMono⟩
 217
 218/-! ## §8. Real-space reachability dichotomy (Phase 17) -/
 219
 220/-- **THEOREM.** The real-space freeze-out dichotomy. A comoving separation `r` is eventually
 221crossed by a recognition signal launched at the σ = 0 seed iff it lies strictly below the
 222horizon: for every `r < 8 φ²` there is a finite epoch whose cumulative reach exceeds `r` (so
 223structure at radius `r` is eventually homogenized), while for every `r ≥ 8 φ²` no finite epoch
 224ever reaches `r` (so structure at radius `r` freezes at its primordial amplitude). This is the
 225real-space form of the Phase-9 horizon and the law-derived statement behind the inner
 226homogenized ball / outer frozen foam split in
 227`scripts/cosmogenesis/foam_real_space_freeze_out.py`: the freeze surface is the comoving sphere
 228of radius `8 φ²`, which by §6 sits strictly between the dyadic shells `2^4 = 16` and
 229`2^5 = 32`. -/
 230theorem reach_dichotomy :
 231    (∀ r : ℝ, r < recognitionEventHorizon → ∃ n : ℕ, r < cumulativeReach n) ∧
 232    (∀ r : ℝ, recognitionEventHorizon ≤ r → ∀ n : ℕ, cumulativeReach n < r) := by
 233  refine ⟨?_, ?_⟩
 234  · intro r hr
 235    have hsum : HasSum perEpochReach recognitionEventHorizon := by
 236      have h := perEpochReach_summable.hasSum
 237      rwa [tsum_perEpochReach] at h
 238    have hT : Filter.Tendsto cumulativeReach Filter.atTop (nhds recognitionEventHorizon) := by
 239      simpa [cumulativeReach] using hsum.tendsto_sum_nat
 240    have hev : ∀ᶠ n in Filter.atTop, r < cumulativeReach n :=
 241      hT.eventually (eventually_gt_nhds hr)
 242    exact hev.exists
 243  · intro r hr n
 244    exact lt_of_lt_of_le (cumulativeReach_lt_horizon n) hr
 245
 246end RecognitionEventHorizon
 247end Cosmology
 248end IndisputableMonolith
 249