IndisputableMonolith.Cosmology.RecognitionEventHorizon
Defines the recognition event horizon in RS cosmology: per-epoch reach scaled by the golden-ratio dilation $1/\varphi$, plus the cumulative geometric sum that bounds causal contact. Cosmologists working in the RS ladder would cite the horizon radius and summability facts. The module is mostly definitions and elementary positivity lemmas imported from Constants.
claimWith $\varphi$ the golden ratio, the per-epoch recognition reach scales as a positive multiple of $\varphi^{-n}$. The cumulative reach is the sum of those terms, and the recognition event horizon is the limiting total reach under golden-ratio dilation (a convergent geometric series).
background
Recognition Science fixes the golden ratio $\varphi$ as the unique self-similar cost fixed point (forcing step T6). In RS-native units the fundamental tick is $\tau_0=1$, and successive recognition epochs dilate by the inverse ratio $1/\varphi<1$.
This module works in that discrete-epoch setting. It aliases $\varphi:=\mathrm{Constants.phi}$ and records the standard facts $0<\varphi$, $1<\varphi$, and $\varphi^2=\varphi+1$, then introduces the dilation ratio $1/\varphi$ as the geometric factor that shrinks reachable recognition volume each epoch.
The named objects are per-epoch reach, cumulative reach (the partial or infinite sum), and the recognition event horizon obtained as the limiting cumulative reach. Elementary lemmas assert positivity of the per-epoch term and summability of the series.
proof idea
Definition-and-lemma module, not a single deep theorem. Local $\varphi$ is a thin alias of Constants.phi; positivity and quadratic identities are one-line re-exports. Per-epoch reach is defined as a positive multiple of the geometric factor $\varphi^{-n}$; cumulative reach is the corresponding sum. Horizon existence is the standard geometric-series argument: $0<\varphi^{-1}<1$ implies absolute convergence, recorded as perEpochReach_pos and perEpochReach_summable.
why it matters in Recognition Science
Supplies the causal-horizon primitive for RS cosmology: once recognition is quantized into epochs dilated by $1/\varphi$, there is a finite total reach beyond which no further recognition events can couple. That bound is the natural place to hang discrete-horizon, causal-diamond, and large-scale structure arguments in the Cosmology domain.
No downstream consumers are wired in the current graph (used_by is empty), so the module is presently a leaf definition package. It sits next to the eight-tick octave (T7) and the $\varphi$-ladder mass formula: the same geometric ratio that grades particle rungs here grades cosmological reach. Closing the leaf would mean citing the horizon inside a proved bound on observable epochs or CMB-scale causal contact.
scope and limits
- Does not derive $\varphi$ or the dilation law; both are imported from Constants and the forcing chain.
- Does not model continuous FLRW metrics, redshift, or standard GR event horizons.
- Does not fix units or the overall yardstick prefactor of per-epoch reach.
- Does not prove observational bounds (CMB, Hubble radius) from the horizon definition.
- Does not yet feed a parent theorem in the dependency graph.
depends on (1)
declarations in this module (25)
-
structure
uses -
lemma
phi_pos -
lemma
one_lt_phi -
lemma
phi_sq_eq -
lemma
phi_inv_pos -
lemma
phi_inv_nonneg -
lemma
phi_inv_lt_one -
def
perEpochReach -
def
recognitionEventHorizon -
def
cumulativeReach -
lemma
perEpochReach_pos -
lemma
perEpochReach_summable -
theorem
tsum_phi_inv_pow -
theorem
tsum_perEpochReach -
theorem
recognitionEventHorizon_eq -
theorem
cumulativeReach_lt_horizon -
theorem
cumulativeReach_strictMono -
theorem
two_pow_four_lt_horizon -
theorem
horizon_lt_two_pow_five -
theorem
recognitionEventHorizon_between_dyadic_rungs -
def
dyadicFreezeRung -
theorem
dyadicFreezeRung_is_least -
theorem
recognition_event_horizon_one_statement -
structure
at -
theorem
reach_dichotomy