row_alphaG_pred
plain-language theorem explainer
The declaration defines the RS-native gravitational fine-structure constant for the electron as G times the square of the structural electron mass divided by ħ c. Recognition Science workers on the mass ladder cite it as the P0-AG row that initiates the dimensionless coupling scorecard. The definition is a direct one-line abbreviation that composes the imported constants G, ħ, c with the electron mass expression.
Claim. $α_G^{RS} := G m_e^2 / (ℏ c)$, where $G$ is the RS-native gravitational constant, $ℏ$ the reduced Planck constant in RS units, $c$ the speed of light, and $m_e$ the structural electron mass.
background
The module sets up the predicted RS-native gravitational coupling α_G^RS in coherence-mass units as the Phase 0 row P0-AG. It uses the constants G = λ_rec² c³ / (π ℏ) and ℏ = φ^{-5} together with the structural electron mass from the phi-ladder. The local setting is the hypothesis bridge that records the raw RS-native value before any external calibration map converts coherence masses to SI kilograms.
proof idea
One-line definition that directly assembles the product G * (electron_structural_mass)^2 / (hbar * c) from the imported constants.
why it matters
It supplies the starting expression for the AlphaGScoreCard, feeding the closed phi-form theorem alphaG_pred_eq and the numerical bracket theorems alphaG_pred_lower and alphaG_pred_upper. The row marks the explicit hypothesis bridge between the RS-native O(10^9) value and the CODATA O(10^{-45}) target, highlighting the dimensional conversion that remains open in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.