horizon_lt_two_pow_five
plain-language theorem explainer
The recognition event horizon $8\varphi^2$ lies strictly below the fifth dyadic rung $2^5=32$. Cosmologists citing Phase-9 freeze-out or dyadic scale selection use this bound to mark scale 32 as super-horizon. The proof rewrites the horizon definition and closes by nonlinear arithmetic from $\varphi^2=\varphi+1$ and nonnegativity of $(\varphi-2)^2$.
Claim. The de Sitter recognition event horizon satisfies $8\varphi^{2}<2^{5}$, i.e. $8\varphi^{2}<32$. Equivalently $\varphi^{2}<4$ (and in fact $\varphi\le 5/3$).
background
In Recognition Science cosmology, a recognition signal covers eight comoving cells per epoch (T-7 eight-tick cadence) while self-similar dilation expands scales by $\varphi$ each epoch (T-6). Per-epoch comoving reach is therefore $8/\varphi^{m}$, and the infinite cumulative reach converges to the geometric sum $8\varphi^{2}\approx 20.944$ cells: the recognition event horizon.
This finite horizon is the forced de Sitter cutoff with no fitted Hubble rate. Structure at or beyond the horizon never enters causal contact and freezes at primordial amplitude; structure below eventually homogenizes. That is the RS $\Omega_{\Lambda}$ freeze-out formalized in this module.
The golden-ratio identity $\varphi^{2}=\varphi+1$ (from $x^{2}-x-1=0$) is the algebraic engine behind the closed form of the sum, and is the sole upstream identity needed here.
proof idea
Compute $2^{5}=32$ by norm_num. Rewrite the goal via the horizon definition as $8\varphi^{2}<32$. Finish with nlinarith, feeding $\varphi^{2}=\varphi+1$ and the nonnegativity of $(\varphi-2)^{2}$. The squared residual supplies the quadratic comparison that forces $\varphi^{2}<4$, hence $8\varphi^{2}<32$.
why it matters
This inequality is one half of the sandwich that pins the freeze break to the fifth dyadic rung. Downstream, recognitionEventHorizon_between_dyadic_rungs pairs it with the companion lower bound $2^{4}<$ horizon to place $8\varphi^{2}$ strictly between 16 and 32. dyadicFreezeRung_is_least then uses it as the witness that the freeze rung equals 5: the least power-of-two exponent strictly above the horizon.
Framework landmarks T-6 ($\varphi$ forced) and T-7 (eight-tick octave) fix the horizon as $8\varphi^{2}$ with no free parameter. The result is the arithmetic anchor of Phase-16 freeze-out scale selection: self-similar structure freezes at and above scale 32 and homogenizes at and below 16, with no fitted scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.