G_div_hbar
plain-language theorem explainer
Researchers computing the RS-native gravitational fine structure constant cite the identity that G over hbar equals phi to the tenth over pi. It supplies the exact algebraic factor needed to close the expression for alpha_G^RS in terms of phi-powers alone. The tactic proof unfolds the definitions of G and hbar, substitutes the relation hbar equals phi to the minus five, and clears the denominator via the exponent sum to zero.
Claim. In Recognition Science native units, $G / hbar = phi^{10} / pi$, where $G$ is the gravitational constant derived from the recognition length and $hbar$ is the reduced Planck constant fixed at $phi^{-5}$.
background
The module AlphaGScoreCard computes the dimensionless gravitational coupling alpha_G^RS defined as G m_e^2 / (hbar c) in coherence-mass units, with c set to one. The constant G is defined via lambda_rec^2 c^3 / (pi hbar) where lambda_rec is the recognition length; after unfolding with ell0 equal to one this reduces to G = 1/(pi hbar). The upstream lemma hbar_eq_phi_inv_fifth states that hbar equals phi to the minus five, the fundamental identity hbar = E_coh tau_0 = phi^{-5}.
proof idea
The proof first unfolds G, lambda_rec, ell0 and c to obtain G = 1/(pi hbar). It rewrites the target ratio as 1/(pi hbar^2) and substitutes hbar^2 = phi^{-10} from two applications of hbar_eq_phi_inv_fifth. The final algebraic step multiplies numerator and denominator by phi^{10} using the ring identity for exponents summing to zero, then applies field_simp to reach phi^{10}/pi.
why it matters
This identity is invoked directly in the proofs of alphaG_pred_eq and alphaG_pred_closed to replace G/hbar by phi^{10}/pi inside the expression for row_alphaG_pred. It closes the algebraic reduction of the RS-native alpha_G to a pure phi-power form, consistent with the forced value of G = phi^5 / pi in the Recognition Science constants. The module doc flags that numerical comparison to CODATA alpha_G still requires the external dimensional bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.