Cosmology Recognition Event Horizon

/-- The horizon in closed form, purely from `φ² = φ + 1`. Numerically
`8 (φ + 1) ≈ 20.944` comoving cells, matching the numeric simulation. -/
theorem recognitionEventHorizon_eq : recognitionEventHorizon = 8 * (φ + 1) := by
  unfold recognitionEventHorizon; rw [phi_sq_eq]

/-- **THEOREM.** The real-space freeze-out dichotomy. A comoving separation `r` is eventually
crossed by a recognition signal launched at the σ = 0 seed iff it lies strictly below the
horizon: for every `r < 8 φ²` there is a finite epoch whose cumulative reach exceeds `r` (so
structure at radius `r` is eventually homogenized), while for every `r ≥ 8 φ²` no finite epoch
ever reaches `r` (so structure at radius `r` freezes at its primordial amplitude). This is the
real-space form of the Phase-9 horizon and the law-derived statement behind the inner
homogenized ball / outer frozen foam split in
`scripts/cosmogenesis/foam_real_space_freeze_out.py`: the freeze surface is the comoving sphere
of radius `8 φ²`, which by §6 sits strictly between the dyadic shells `2^4 = 16` and
`2^5 = 32`. -/
theorem reach_dichotomy :
    (∀ r : ℝ, r < recognitionEventHorizon → ∃ n : ℕ, r < cumulativeReach n) ∧
    (∀ r : ℝ, recognitionEventHorizon ≤ r → ∀ n : ℕ, cumulativeReach n < r) := by
  refine ⟨?_, ?_⟩
  · intro r hr
    have hsum : HasSum perEpochReach recognitionEventHorizon := by
      have h := perEpochReach_summable.hasSum
      rwa [tsum_perEpochReach] at h
    have hT : Filter.Tendsto cumulativeReach Filter.atTop (nhds recognitionEventHorizon) := by
      simpa [cumulativeReach] using hsum.tendsto_sum_nat
    have hev : ∀ᶠ n in Filter.atTop, r < cumulativeReach n :=
      hT.eventually (eventually_gt_nhds hr)
    exact hev.exists
  · intro r hr n
    exact lt_of_lt_of_le (cumulativeReach_lt_horizon n) hr

/-- **THEOREM.** After any finite number of epochs the cumulative reach is
strictly below the horizon. A comoving separation at or beyond `8 φ²` is
therefore never crossed by a recognition signal, so super-horizon structure can
never be homogenized: it freezes at its primordial amplitude. -/
theorem cumulativeReach_lt_horizon (n : ℕ) :
    cumulativeReach n < recognitionEventHorizon := by
  have hsum := perEpochReach_summable
  have hsplit := Summable.sum_add_tsum_nat_add n hsum
  have htail_summable : Summable (fun i => perEpochReach (i + n)) :=
    (summable_nat_add_iff n).2 hsum
  have htail_pos : 0 < ∑' i, perEpochReach (i + n) :=
    htail_summable.tsum_pos (fun i => le_of_lt (perEpochReach_pos _)) 0
      (perEpochReach_pos _)
  have key :
      cumulativeReach n + ∑' i, perEpochReach (i + n) = recognitionEventHorizon := by
    have h := hsplit
    rw [tsum_perEpochReach] at h
    simpa [cumulativeReach] using h
  linarith [htail_pos, key]

/-- **THEOREM.** The cumulative reach increases strictly with each epoch:
each epoch adds a strictly positive per-epoch reach, so the reach climbs
monotonically toward (but never attains) the horizon. -/
theorem cumulativeReach_strictMono : StrictMono cumulativeReach := by
  apply strictMono_nat_of_lt_succ
  intro n
  have hstep : cumulativeReach (n + 1) = cumulativeReach n + perEpochReach n := by
    simp [cumulativeReach, Finset.sum_range_succ]
  rw [hstep]; linarith [perEpochReach_pos n]

/-- **THEOREM.** The recognition event horizon `8 φ²` sits strictly between the dyadic rungs
`2^4 = 16` and `2^5 = 32`. So a self-similar (dyadic) structure freezes exactly at and above
the scale `2^5 = 32` and homogenizes at and below `2^4 = 16`: the freeze break is forced to
the fifth dyadic rung, with no fitted scale. This is the arithmetic anchor of the Phase-16
freeze-out scale selection (`scripts/cosmogenesis/foam_freeze_out.py`). -/
theorem recognitionEventHorizon_between_dyadic_rungs :
    (2 : ℝ) ^ 4 < recognitionEventHorizon ∧ recognitionEventHorizon < (2 : ℝ) ^ 5 :=
  ⟨two_pow_four_lt_horizon, horizon_lt_two_pow_five⟩

/-- **THEOREM.** `dyadicFreezeRung = 5` is the least power-of-two rung strictly above the
recognition horizon: `2^5 > 8 φ²`, while every smaller rung `2^k` (`k < 5`) is strictly below
it. So the freeze-out selects exactly the dyadic scales at or above `2^5 = 32`. -/
theorem dyadicFreezeRung_is_least :
    recognitionEventHorizon < (2 : ℝ) ^ dyadicFreezeRung ∧
    ∀ k : ℕ, k < dyadicFreezeRung → (2 : ℝ) ^ k < recognitionEventHorizon := by
  refine ⟨horizon_lt_two_pow_five, ?_⟩
  intro k hk
  simp only [dyadicFreezeRung] at hk
  have hk4 : k ≤ 4 := by omega
  have hnat : (2 : ℕ) ^ k ≤ 2 ^ 4 := Nat.pow_le_pow_right (by norm_num) hk4
  have hmono : (2 : ℝ) ^ k ≤ (2 : ℝ) ^ 4 := by exact_mod_cast hnat
  exact lt_of_le_of_lt hmono two_pow_four_lt_horizon

/-- **RECOGNITION EVENT HORIZON, ONE STATEMENT.** The forced φ-dilation (one
φ-rung per eight-tick epoch, T-6 and T-7) gives a finite de Sitter recognition
horizon equal to `8 φ² = 8 (φ + 1)`; the cumulative reach converges to it from
strictly below and increases monotonically, so any comoving separation at or
beyond `8 φ²` is never crossed. This is the law-derived freeze-out mechanism:
no tuned Hubble rate and no fitted coupling enter. -/
theorem recognition_event_horizon_one_statement :
    (∑' m : ℕ, perEpochReach m = recognitionEventHorizon) ∧
    recognitionEventHorizon = 8 * (φ + 1) ∧
    (∀ n : ℕ, cumulativeReach n < recognitionEventHorizon) ∧
    StrictMono cumulativeReach :=
  ⟨tsum_perEpochReach, recognitionEventHorizon_eq, cumulativeReach_lt_horizon,
    cumulativeReach_strictMono⟩