gap_weight_approx
plain-language theorem explainer
The eight-tick gap weight w₈ satisfies 2.490 < w₈ < 2.491. Researchers deriving the fine-structure constant from Recognition Science constants cite this bound to confirm the closed-form expression falls inside the target interval. The proof splits the conjunction and chains pre-established numeric bounds on the expression in √2 and φ.
Claim. $2.490 < w_8 < 2.491$, where $w_8 = (348 + 210√2 - (204 + 130√2)φ)/7$ is the normalized projection weight of the gap onto the fundamental 8-tick basis and φ is the golden ratio.
background
The gap weight w₈ is the canonical, parameter-free quantity defined as the normalized projection weight of the gap onto the fundamental 8-tick basis. Its closed form is (348 + 210√2 - (204 + 130√2)φ)/7, with numerical value approximately 2.49056927545. This definition appears in the eight-tick octave step of the forcing chain and is packaged inside the Constants structure of LawOfExistence, which bundles Knet, Cproj, Ceng, Cdisp together with non-negativity of Knet. The present module supplies numeric match-to-CODATA checks for the symbolic alpha derivation.
proof idea
Constructor splits the conjunction into separate inequalities. The lower bound is discharged by a calc chain that steps from 2.490 through the pre-proved w8_computed_gt. The upper bound is discharged by a calc chain that steps from w8_computed_lt to 2.491. Both outer comparisons are closed by norm_num.
why it matters
This theorem supplies a tight numeric verification that the gap weight lies inside (2.490, 2.491), anchoring the alpha numerics scaffold. It directly supports the Constants bundle in LawOfExistence and the eight-tick octave (T7) of the forcing chain. No downstream lemmas are recorded, so the declaration functions as a verification checkpoint rather than an intermediate lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.