w8_matches_certified
plain-language theorem explainer
The gap weight w₈ from the eight-tick basis satisfies 2.490564399 < w₈ < 2.490572090. Recognition Science numerics work cites this to certify the closed-form expression against machine-checked interval bounds. The proof is a direct constructor that applies the two pre-established bounding theorems on the expression in √2 and φ.
Claim. $2.490564399 < w_8 < 2.490572090$, where $w_8$ is the normalized projection weight of the gap onto the fundamental 8-tick basis given by the closed-form expression $(348 + 210√2 - (204 + 130√2)φ)/7$.
background
The gap weight w₈ is the parameter-free closed-form quantity defined in GapWeight as the normalized projection weight of the gap onto the fundamental 8-tick basis, with numerical value approximately 2.49056927545. The present module supplies a numeric match certificate confirming that this quantity lies inside a narrow verified interval. Upstream results include the definition of w8_from_eight_tick together with the two bounding theorems w8_computed_gt and w8_computed_lt that establish the lower and upper ends of the interval by corner-case estimates on √2 and φ.
proof idea
The proof is a term-mode constructor that directly applies the two bounding theorems w8_computed_gt and w8_computed_lt from the W8Bounds module.
why it matters
This theorem supplies the certified interval used by the downstream w8_value theorem to obtain the approximate equality |w₈ - 2.490569275454| < 5e-6. It certifies the eight-tick gap weight inside the constants layer and aligns with the T7 eight-tick octave step of the forcing chain. No open questions remain; the bounds are fully discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.