pith. sign in
module module high

IndisputableMonolith.Constants.GapWeightNumericsScaffold

show as:
view Lean formalization →

This module certifies that the closed-form gap weight w₈ from the eight-tick projection matches its expected value within tolerance. Researchers deriving the fine-structure constant α cite it to confirm the parameter-free coefficient in f_gap = w₈ ln(φ). The module imports GapWeight and W8Bounds then defines w8_value together with the match predicate w8_matches_certified.

claimThe gap weight satisfies $w_8 = (348 + 210√2 - (204 + 130√2)φ)/7$ and matches the DFT-8 expected value within tolerance.

background

In the constants domain the gap weight w₈ supplies the single coefficient in the α pipeline term f_gap = w₈ · ln(φ). The upstream GapWeight module requires that w₈ be a parameter-free closed form to preserve the no-free-parameters claim. The W8Bounds module supplies the explicit expression w8 = (348 + 210√2 - (204 + 130√2)φ)/7, which evaluates numerically to approximately 2.490569.

proof idea

This is a definition module, no proofs. It consists of two sibling declarations: w8_value extracts the closed-form expression imported from W8Bounds, while w8_matches_certified applies the tolerance check to certify agreement with the DFT-8 value.

why it matters in Recognition Science

The module supplies the numeric certification required by the downstream AlphaNumericsScaffold for match-to-CODATA checks on the symbolic alpha derivation. It thereby supports the T7 eight-tick octave step by confirming a closed-form w₈ without free parameters. The parent module uses these checks to validate the overall α pipeline.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (2)