alphaInv_predicted_range_check
The definition encodes a proposition that the Recognition Science-derived inverse fine-structure constant lies strictly between 137.030 and 137.039. Researchers checking numerical consistency of fundamental constants against CODATA would cite this as a direct match-to-data verification. It is realized as a one-line conjunction of inequalities on the alphaInv expression imported from the Alpha module.
claim$137.030 < {a}^{-1} < 137.039$, where ${a}^{-1}$ denotes the dimensionless inverse fine-structure constant obtained via exponential resummation of the structural seed and gap weight.
background
This module supplies numeric evaluation checks that match the symbolic alpha derivation in Constants.Alpha to experimental ranges. The central quantity alphaInv is defined as alpha_seed * exp(-(f_gap / alpha_seed)) and evaluates near 137.036. The fundamental tick is the RS-native time quantum fixed at 1, with one octave equal to eight ticks. Upstream results include the tick definition as the base time unit and the alphaInv formula itself, which carries no adjustable parameters.
proof idea
The declaration is a direct definition of the Prop consisting of the two-sided inequality on alphaInv. It applies the imported alphaInv expression without further lemmas or tactics.
why it matters in Recognition Science
This supplies the concrete numerical anchor confirming that the derived alpha inverse falls inside the predicted band (137.030, 137.039) required by the Recognition Science framework. It closes the verification step for the alpha derivation in Constants.Alpha and aligns with the eight-tick octave structure. No downstream theorems are listed, so the declaration functions as a standalone consistency check rather than an input to further proofs.
scope and limits
- Does not derive the exact numerical value of alphaInv from axioms.
- Does not incorporate experimental uncertainties or CODATA error bars.
- Does not relate alphaInv to other RS constants such as G or hbar.
formal statement (Lean)
18def alphaInv_predicted_range_check : Prop :=
proof body
Definition body.
19 137.030 < alphaInv ∧ alphaInv < 137.039
20
21/-- Check: the 8-tick gap weight is approximately 2.49057. -/