dyadicFreezeRung
plain-language theorem explainer
Names the natural number 5 as the dyadic freeze rung: the least exponent k with 2^k strictly above the recognition event horizon 8φ². Cosmologists working the Phase-9 freeze-out cite it when selecting which power-of-two comoving scales freeze at primordial amplitude. The body is a one-line constant definition; the leastness claim is proved separately.
Claim. The dyadic freeze rung is the natural number $5$, intended as the least exponent $k$ such that $2^k$ lies strictly above the recognition event horizon $8\varphi^2\approx 20.944$ (so $2^5=32$ is the first dyadic scale at or beyond freeze-out).
background
The module treats the finite recognition event horizon that drives Phase-9 accelerated-expansion freeze-out. A recognition signal covers one comoving cell per tick; the eight-tick octave (T-7) gives eight cells per epoch at unit scale. Self-similar dilation by φ per epoch (T-6) shrinks the comoving reach of epoch m to $8/\varphi^m$.
The infinite cumulative reach is the geometric series $\sum_{m\ge 0} 8(1/\varphi)^m$. Since $1/\varphi<1$ and $\varphi^2=\varphi+1$, the sum equals the closed form $8\varphi^2\approx 20.944$ comoving cells. Separations at or beyond that horizon are never crossed by a recognition signal, so structure there freezes at primordial amplitude (the RS $\Omega_\Lambda$ freeze-out).
Among pure powers of two, one needs the least $k$ with $2^k>8\varphi^2$. Numerically $2^4=16$ sits below the horizon and $2^5=32$ sits above; this definition packages that exponent as a named constant.
proof idea
Pure definition: the body is the numeral 5. No tactics, no lemmas. Downstream theorems unfold the name and discharge the inequalities $8\varphi^2<2^5$ and $2^k<8\varphi^2$ for all $k<5$.
why it matters
Gives a stable name to the dyadic cutoff used by dyadicFreezeRung_is_least, which proves $8\varphi^2<2^5$ and that every smaller power of two lies strictly below the horizon, so freeze-out selects exactly the dyadic scales at or above $2^5=32$.
The constant is forced by the same two landmarks that fix the horizon itself: the eight-tick cadence (T-7) and the self-similar fixed point φ with $\varphi^2=\varphi+1$ (T-6). No fitted Hubble rate or coupling enters. It is the discrete rung at which the continuous geometric horizon is snapped onto the power-of-two ladder used elsewhere in the RS mass and spectrum constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.