IndisputableMonolith.Constants.GapWeightNumericsScaffold
Scaffold module certifying that the closed-form eight-tick gap weight w₈ agrees with its certified numeric value inside a fixed tolerance. Alpha-pipeline and constants authors cite it when wiring the gap term f_gap = w₈ ln φ into numeric α checks. The argument is a direct match of the DFT-8 closed form against interval bounds from W8Bounds.
claimThe eight-tick gap weight $w_8 = (348 + 210\sqrt{2} - (204 + 130\sqrt{2})\varphi)/7$ matches its certified numeric value (approximately $2.490569$) within the stated tolerance, so the gap term $f_{\mathrm{gap}} = w_8 \ln\varphi$ is numerically grounded.
background
In the Recognition Science α pipeline a single gap correction appears: $f_{\mathrm{gap}} = w_8 \cdot \ln\varphi$. Historically $w_8$ lived only as a numeric certificate; the GapWeight module replaces that with a parameter-free closed form obtained from the eight-tick (DFT-8) projection,
$w_8 = (348 + 210\sqrt{2} - (204 + 130\sqrt{2})\varphi)/7$.
W8Bounds records that this expression evaluates to about $2.490569$ and supplies interval certificates. The present module sits between those two layers: it imports the closed form and the interval bounds, then exposes the match lemmas (w8_matches_certified, w8_value) that downstream numeric scaffolds need. The eight-tick structure itself is the T7 landmark (period $2^3$) of the forcing chain.
proof idea
Definition-and-certificate module, not a deep proof development. It evaluates the closed-form $w_8$ from GapWeight, compares the result to the certified interval from W8Bounds, and packages the agreement as w8_matches_certified together with an explicit numeric w8_value. No new analytic identities are proved here; the work is interval arithmetic and tolerance checking against the upstream bounds.
why it matters in Recognition Science
Feeds AlphaNumericsScaffold, which runs match-to-CODATA checks on the symbolic α construction. Without a certified numeric $w_8$, the gap term in that construction cannot be evaluated inside Lean. The module therefore closes the last numeric hinge between the parameter-free DFT-8 formula and the α band checks, while leaving exact $\alpha^{-1}(0)$ open (as AlphaNumericsScaffold itself notes). It supports the broader "no free parameters" claim for constants by replacing an ad-hoc float with a proved match to the closed form.
scope and limits
- Does not derive the closed form of $w_8$; that lives in GapWeight.
- Does not prove exact equality to any CODATA constant; only a tolerance match.
- Does not derive $\alpha$ or close the exact $\alpha^{-1}(0)$ question.
- Does not supply analytic error bounds beyond the imported W8Bounds intervals.