alphaG_pred_closed
plain-language theorem explainer
The theorem proves the RS-native electron gravitational coupling equals (2^{-44} φ^{112}) / π. Researchers deriving dimensionless constants from the Recognition Science mass ladder cite it to confirm the closed φ-form. The tactic proof substitutes the forced structural mass, squares it via zpow and rpow identities, reduces G/hbar, adds ten to the exponent, and clears the π denominator.
Claim. The RS-native gravitational coupling for the electron, defined as G m_e² / (ℏ c) with m_e the structural mass, equals (2^{-44} φ^{112}) / π.
background
The AlphaGScoreCard module computes the dimensionless gravitational coupling α_G^{RS} := G m_e² / (ℏ c) in RS-native units (c = 1). The structural electron mass is supplied by the upstream forced formula 2^{-22} φ^{51}. Constants.G gives G = λ_rec² c³ / (π ℏ) while Constants.hbar supplies ℏ = φ^{-5}; the sibling G_div_hbar lemma reduces the ratio directly.
proof idea
The proof recalls electron_structural_mass_forced, squares the mass with pow_two and zpow_add₀ to obtain 2^{-44} φ^{102}, rewrites row_alphaG_pred using hbar_c_eq_hbar, factors G/hbar, applies G_div_hbar, adds ten to the exponent via Real.rpow_add, and finishes with field_simp plus the merge identity for φ^{112}.
why it matters
This supplies the exact closed form required by the downstream bounds alphaG_pred_lower and alphaG_pred_upper. It realizes the predicted value for phase-0 row P0-AG in the physical derivation plan, connecting the phi-ladder mass formula (T6 fixed point) to the gravitational constant. The remaining open question is the dimensional bridge to SI units for CODATA comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.