IndisputableMonolith.Numerics.Interval.W8Bounds
The module supplies verified decimal bounds on √2, φ and the derived gap weight w₈. Researchers building the α pipeline or Fermi-constant scorecard cite these bounds to certify the numeric value of w₈. The argument consists of direct decimal-comparison lemmas that establish the input inequalities and propagate them to an interval for w₈.
claim$1.4142 < √2 < 1.4143$, $1.61803395 < φ < 1.6180340$, and the resulting closed interval for the gap weight $w_8$.
background
The upstream GapWeight module defines the 8-tick projection weight by the relation f_gap = w₈ · ln(φ) and requires that w₈ be obtained without free parameters. This module imports that definition and supplies the decimal certificates needed to make the claim rigorous. The local setting is therefore numeric interval arithmetic supporting the Recognition Science constants pipeline.
proof idea
This is a numerics module. It contains direct inequality lemmas for √2 and φ via decimal comparisons, followed by computed lower and upper bounds on w₈ and the definition of w8Interval.
why it matters in Recognition Science
The module feeds AlphaBounds (rigorous bounds on α⁻¹), GapWeightNumericsScaffold (numeric match certificate) and FermiConstantScoreCard (electroweak identity). It supplies the numeric certification step required by the T7 eight-tick octave and the gap term in the α pipeline.
scope and limits
- Does not derive a closed-form expression for w₈.
- Does not bound constants other than √2, φ and w₈.
- Does not address the symbolic derivation from the forcing chain.
- Limited to the listed decimal precisions.