pith. sign in
module module high

IndisputableMonolith.Constants.AlphaNumericsScaffold

show as:
view Lean formalization →

This module scaffolds numeric verification that the Recognition Science derivation of the inverse fine-structure constant yields a value near 137.036. Researchers deriving constants from the phi-ladder or J-function would cite it to confirm consistency with the observed alpha band. The module assembles range checks and gap-weight approximations imported from Alpha and GapWeightNumericsScaffold without performing new derivations.

claimThe scaffold asserts that the predicted value satisfies $137.030 < α^{-1} < 137.039$, with a central numeric check at approximately 137.036 derived from the phi-ladder and gap weights.

background

Recognition Science obtains α^{-1} from the J-cost function and the eight-tick octave structure, placing the value inside the narrow band (137.030, 137.039). The imported Alpha module supplies the predicted range while GapWeightNumericsScaffold supplies the numeric approximations for rung gaps that enter the mass formula. The present module simply wires these pieces into a single check that the derived α^{-1} sits near 137.036.

proof idea

This is a definition module, no proofs. It imports the range predicate from Alpha and the gap-weight approximant from GapWeightNumericsScaffold, then assembles them into the sibling declarations alphaInv_predicted_range_check and gap_weight_approx.

why it matters in Recognition Science

The module supplies the numeric match certificate required by the constant derivations that follow from T8 (D = 3) and the RCL. It feeds the parent constant-verification layer by confirming that the phi-ladder output for α^{-1} lands inside the experimental window, closing one link in the chain from J-uniqueness to observable constants.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (2)