Cosmology Recognition Event Horizon Horizon Lt Two Pow Five

The finite horizon

In cosmology, an event horizon is the boundary beyond which events can never be seen or influenced from a given location, because the universe's expansion carries them away faster than any signal can travel. In the Recognition Science framework, the same idea takes a precise, countable form. The framework models the universe as a discrete grid of cells, where a recognition signal, a unit of information transfer, moves one cell per tick, the framework's basic time step. The tick cadence is fixed at eight ticks per epoch, and each epoch expands the grid by the golden ratio φ ≈ 1.618. So a signal launched now covers 8 cells in the first epoch, then 8/φ in the next, then 8/φ², and so on. Adding these shrinking contributions gives a finite total: 8φ² = 8(φ+1) ≈ 20.944 cells. This number is the framework's recognition event horizon.

The theorem horizon_lt_two_pow_five proves that this horizon is less than 2⁵ = 32 cells. The proof is short and purely algebraic: it uses the identity φ² = φ + 1 and the fact that (φ − 2)² ≥ 0 to show 8(φ+1) < 32. A companion theorem places the horizon between 16 and 32, and another identifies 5 as the least integer rung for which 2^r exceeds the horizon. These are not approximations; they are exact inequalities in the real numbers, checked by the framework's machine-checked library of formal theorems. The library also proves that the sum of the reach over all epochs converges exactly to 8φ², and that any finite partial sum stays strictly below it. The horizon is a genuine limit, approached but never reached.

The physical consequence, within the framework, is a freeze-out. Any two grid cells separated by 20.944 cells or more can never exchange a recognition signal, so they can never be brought into causal contact or homogenized. Their differences freeze at their primordial amplitude. Structure below the horizon is eventually crossed and smoothed. This is the framework's account of accelerated-expansion freeze-out, with no fitted Hubble rate or coupling constant; the number 8φ² comes entirely from the fixed cadence and the golden-ratio dilation.

In Recognition Science, this horizon is the future-directed reach of a signal launched now. It is deliberately distinct from the past-directed particle horizon used in the vacuum-energy ledger cost, which must not depend on future expansion. The two objects are consistent, not in tension: one governs ground-state cost, the other governs forward freeze-out. The theorem itself establishes only the inequality and its algebraic consequences; the translation from those inequalities to the physical freeze-out story is a modeling step, not part of the formal proof.

/-- 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 total cumulative reach over all epochs equals the forced
event horizon `8 φ²`. A recognition signal can only ever traverse a finite
comoving distance, even given infinitely many epochs. -/
theorem tsum_perEpochReach :
    ∑' m : ℕ, perEpochReach m = recognitionEventHorizon := by
  unfold perEpochReach recognitionEventHorizon
  rw [tsum_mul_left, tsum_phi_inv_pow]

/-- The horizon is strictly below the dyadic rung `2^5 = 32`: `8 φ² < 32`, equivalently
`φ² < 4`, equivalently `φ < 3` (in fact `φ ≤ 5/3`). So a self-similar (dyadic) structure at
scale `2^5 = 32` is super-horizon and freezes at its primordial amplitude. -/
theorem horizon_lt_two_pow_five : recognitionEventHorizon < (2 : ℝ) ^ 5 := by
  have h32 : (2 : ℝ) ^ 5 = 32 := by norm_num
  rw [recognitionEventHorizon_eq, h32]
  nlinarith [phi_sq_eq, sq_nonneg (φ - 2)]

/-- **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 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

What this page does not claim

The theorem does not prove that the physical universe has a discrete grid or that recognition signals are real; that is a modeling assumption. The theorem does not derive the value of the cosmological constant or any Hubble rate. The freeze-out story is a framework interpretation, not part of the formal inequality.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cosmology/RecognitionEventHorizon.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: