exponentialLoad_lt_0086705
plain-language theorem explainer
The gap-weight to geometric-seed ratio satisfies f_gap/α_seed < 0.0086705. Measurement-verdict arguments cite this as the certified exponential-load ceiling before comparing first-order α⁻¹_Genesis to CODATA. The proof multiplies interval upper bounds on the eight-tick weight and log φ, then clears the division by a lower bound on the seed 4π·11.
Claim. Let $f_{\mathrm{gap}} = w_8\log\varphi$ be the eight-tick gap weight and $\alpha_{\mathrm{seed}} = 4\pi\cdot 11$ the geometric seed. Then $f_{\mathrm{gap}}/\alpha_{\mathrm{seed}} < 0.0086705$.
background
This lives in the Alpha Genesis M7 quarantine module, which formalizes Anil Thapa's measurement-side objection against the first-order inverse-fine-structure prediction. The module imports CODATA anchors and is deliberately not imported by the forward construction.
The gap weight is $f_{\mathrm{gap}} = w_8\log\varphi$, with $w_8$ the DFT-8 eight-tick projection weight and $\varphi=(1+\sqrt{5})/2$ the golden ratio forced at T6. The geometric seed $\alpha_{\mathrm{seed}}=4\pi\cdot 11$ is the baseline spherical closure cost over 11-edge interaction paths. Their ratio is the natural exponential load entering the first-order curvature correction to $\alpha^{-1}$.
Upstream, log_phi_lt_048122 supplies $\log\varphi<0.48122$, and interval numerics give a strict upper bound on $w_8$ together with $\alpha_{\mathrm{seed}}>138.230048$. The lemma one_lt_phi guarantees $\log\varphi>0$, so all factors stay positive under multiplication.
proof idea
Two intermediate inequalities, then a cleared division.
First bound $f_{\mathrm{gap}}$ from above: unfold it as $w_8\log\varphi$, apply w8_computed_lt and log_phi_lt_048122, and use positivity of $w_8$ and of $\log\varphi$ (from one_lt_phi) to get
$w_8\log\varphi < w_8\cdot 0.48122 < 2.490572090\cdot 0.48122 < 1.198514$.
Second, take the certified seed floor $\alpha_{\mathrm{seed}}>138.230048$ from alpha_seed_gt, hence positivity. Rewrite the target as $f_{\mathrm{gap}} < 0.0086705\cdot\alpha_{\mathrm{seed}}$ via div_lt_iff₀, then chain $f_{\mathrm{gap}}<1.198514$ into $1.198514 < 0.0086705\cdot\alpha_{\mathrm{seed}}$ by nlinarith on the seed lower bound.
why it matters
Sole consumer is alphaInvGenesis_exceeds_CODATA_by_0007, the formal statement of Anil's measurement objection: first-order $\alpha^{-1}_{\mathrm{Genesis}}$ sits at least $0.0007$ above the CODATA anchor. Because CODATA's $1\sigma$ uncertainty is $\sim 2.1\times 10^{-8}$, that margin is $>30000\sigma$; the exact residual is about $7.67\times 10^{-4}$, and this load bound is the certified piece that makes the coarse comparison honest.
In the RS constants pipeline the load $f_{\mathrm{gap}}/\alpha_{\mathrm{seed}}$ is the exponential factor in the first-order curvature correction built from the eight-tick weight (T7) and $\varphi$ (T6). The quarantine design keeps CODATA out of the forward Alpha Genesis derivation while still answering the measurement challenge before any seam correction is derived. The RS-native $\alpha^{-1}$ band $(137.030,137.039)$ is the longer-term target; this lemma only polices the present first-order overshoot.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.