native_very_not_codata
plain-language theorem explainer
Recognition Science native prediction for the dimensionless electron gravitational coupling exceeds the CODATA value. Researchers comparing RS constants to experiment cite this to flag the mismatch requiring a dimensional bridge. The short tactic proof combines a lower bound on the native prediction with a numerical upper bound on the CODATA figure and applies linear arithmetic to obtain the strict inequality.
Claim. The CODATA value of the dimensionless gravitational coupling satisfies $α_G^{CODATA} < α_G^{RS}$, where $α_G^{RS} = G m_e^2 / (ℏ c)$ is the Recognition Science prediction in coherence-mass units on the φ-ladder.
background
The AlphaGScoreCard module computes the RS-native dimensionless gravitational coupling as $α_G^{RS} := G m_e^2 / (ℏ c)$, where $G$ is the RS-native gravitational constant and $m_e$ is the electron structural mass on rung 2 of the φ-ladder. The row prediction is the closed φ-form value of this expression. The target is the CODATA experimental value approximately 1.7518 × 10^{-45}.
proof idea
The proof is a short tactic sequence. It obtains the lower bound on the RS prediction from the alphaG_pred_lower lemma. It then shows that the CODATA value is less than 10^9 by unfolding the codata definition and applying norm_num. Linear arithmetic on these two facts establishes the strict inequality.
why it matters
This theorem supplies the not_codata component of the AlphaGScoreCardCert in the same module. It implements the P0-AG row of the physical derivation plan by documenting the separation between the native RS prediction and the experimental CODATA target. In the Recognition framework it highlights the necessity of the structural mass bridge before any numerical comparison to experiment, consistent with the φ-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.