IndisputableMonolith.Masses.AlphaGScoreCard
The AlphaGScoreCard module assembles predictions and closed interval bounds for the RS-derived product alpha G. Researchers verifying fundamental constants against the phi-ladder and observed alpha band would cite its rows. The module organizes its content as a sequence of row definitions, equality lemmas, and bracketed codata that close the prediction using imported phi bounds and electron mass residue.
claimThe module defines the predicted product $alpha_G^{pred}$ together with its closed interval bounds $alpha_G^{pred} in [alpha_G^{lower}, alpha_G^{upper}]$ and associated equality statements, all expressed in RS-native units where $G = phi^5 / pi$.
background
Recognition Science derives constants from the T0-T8 forcing chain with phi as self-similar fixed point and D=3. The Constants module supplies the base time quantum tau_0 = 1 tick. PhiBounds supplies algebraic inequalities that pin phi = (1 + sqrt(5))/2. ElectronMass formalizes the T9 electron mass via the ledger fraction hypothesis with residue delta.
proof idea
This is a definition module, no proofs. It collects row definitions for alphaG predictions, equality lemmas that equate closed forms, and bracketed interval statements that apply the imported phi bounds and electron mass ledger fraction.
why it matters in Recognition Science
The module supplies the alphaG scorecard that supports numerical checks against the predicted alpha^{-1} interval (137.030, 137.039) and G = phi^5 / pi. It prepares data for downstream mass ladder applications in the Recognition framework.
scope and limits
- Does not derive alpha from the forcing chain T0-T8.
- Does not extend beyond the electron mass residue delta.
- Does not compute explicit numerical values outside the supplied phi bounds.
- Does not connect to higher rungs of the mass ladder.
depends on (3)
declarations in this module (16)
-
def
row_alphaG_pred -
theorem
row_alphaG_pred_eq -
theorem
c_eq_one' -
theorem
hbar_c_eq_hbar -
theorem
G_div_hbar -
theorem
alphaG_pred_eq -
theorem
alphaG_pred_closed -
theorem
alphaG_pred_lower -
theorem
alphaG_pred_upper -
theorem
alphaG_pred_bracket -
def
alphaG_codata -
theorem
codata_very_small -
theorem
native_very_not_codata -
structure
AlphaGScoreCardCert -
def
cert -
theorem
cert_inhabited