alphaG_pred_eq
plain-language theorem explainer
The equality reduces the RS-native gravitational coupling α_G^RS := G m_e² / (ℏ c) to the closed form m_e² φ^{10} / π under the unit convention c = 1. Workers closing the P0-AG row of the physical derivation plan cite this result when they need the exact φ-ladder expression for the electron-scale prediction. The tactic proof substitutes the relation ħ c = ħ, factors the quotient via field_simp on ħ ≠ 0, inserts the pre-derived ratio G / ħ, and finishes with ring.
Claim. In RS-native units the predicted gravitational fine-structure constant satisfies α_G^RS := G m_e² / (ℏ c) = m_e² φ^{10} / π, where m_e denotes the structural electron mass.
background
The module supplies a dimensionless score card for gravitational coupling at the electron scale (Phase 0 row P0-AG). In RS-native units the constants are defined by G = λ_rec² c³ / (π ħ) and ħ = φ^{-5}, with c fixed to 1; the structural electron mass is taken from Physics.ElectronMass.electron_structural_mass. The theorem therefore converts the defining expression α_G^RS := G m_e² / (ℏ c) into an explicit power of φ divided by π.
proof idea
The proof first rewrites with the lemma hbar_c_eq_hbar that enforces ħ c = ħ. It then rewrites the quotient G * m_e² / ħ as (G / ħ) * m_e² by field_simp on the nonzero ħ supplied by hbar_pos. Substitution of the precomputed ratio G_div_hbar followed by ring closes the equality.
why it matters
This supplies the closed φ-form required for the P0-AG row in the physical derivation plan and feeds the subsequent bounds alphaG_pred_closed, alphaG_pred_lower and alphaG_pred_upper. The derivation rests on the Recognition Science forcing chain that fixes φ as the self-similar fixed point and sets D = 3. The open question it touches is the explicit dimensional bridge that would map the native O(10^9) value onto the CODATA O(10^{-45}) number.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.