recognitionEventHorizon_between_dyadic_rungs
plain-language theorem explainer
The recognition event horizon $8\varphi^2$ lies strictly between the dyadic scales $2^4=16$ and $2^5=32$. Anyone citing the Phase-16 freeze-out scale selection (no fitted Hubble rate) needs this sandwich. The proof is a one-line pairing of the two one-sided inequalities already proved in-module.
Claim. The de Sitter recognition event horizon satisfies $2^{4} < 8\varphi^{2} < 2^{5}$, equivalently $16 < 8\varphi^{2} < 32$. Thus a self-similar dyadic structure freezes at and above scale $32$ and homogenizes at and below scale $16$.
background
This module fixes the finite recognition horizon that drives Phase-9 accelerated-expansion freeze-out. A recognition signal covers one comoving cell per tick; the eight-tick octave (T-7) therefore yields eight cells per epoch at unit scale. Forced self-similar dilation expands the comoving scale by $\varphi$ each epoch (T-6), so the reach in epoch $m$ is $8/\varphi^{m}$. The infinite cumulative reach is the geometric series $\sum_{m\ge 0} 8(1/\varphi)^{m}=8\varphi^{2}\approx 20.944$ comoving cells, using $\varphi^{2}=\varphi+1$.
That limit is the definition recognitionEventHorizon := 8 * φ^2. Separations at or beyond it are never crossed by a recognition signal and freeze at primordial amplitude; separations below it are eventually homogenized. The two one-sided comparisons to powers of two are already theorems: $2^{4}<8\varphi^{2}$ from $1<\varphi$, and $8\varphi^{2}<2^{5}$ from $\varphi^{2}<4$ (via $\varphi\le 5/3$).
proof idea
Term-mode constructor pairing. The left conjunct is exactly two_pow_four_lt_horizon ($2^4 < 8\varphi^2$, reduced by rewriting the horizon definition and applying $1<\varphi$). The right conjunct is exactly horizon_lt_two_pow_five ($8\varphi^2 < 2^5$, reduced via $\varphi^2=\varphi+1$ and a nonnegativity bound on $(\varphi-2)^2$). No further arithmetic is done here.
why it matters
This is the arithmetic anchor of Phase-16 freeze-out scale selection (foam_freeze_out.py): the freeze break is forced to the fifth dyadic rung with no fitted scale. It packages the two horizon-vs-dyadic comparisons into the single sandwich cosmologists quote when arguing that structure at $2^5=32$ is super-horizon (freezes) while structure at $2^4=16$ is sub-horizon (homogenizes).
Framework landmarks used are exactly T-6 ($\varphi$ as self-similar fixed point, $\varphi^2=\varphi+1$) and T-7 (eight-tick octave supplying the factor 8). The horizon value $8\varphi^2$ itself is the closed form of the geometric series of per-epoch reaches; the sandwich shows that value sits cleanly between consecutive powers of two. No downstream Lean consumers are recorded yet; the declaration is the citation form of the already-proved bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.