hbar_c_eq_hbar
plain-language theorem explainer
The declaration proves that the reduced Planck constant times the speed of light equals the reduced Planck constant itself in Recognition Science native units. Researchers working on the dimensionless gravitational coupling alpha_G would cite this identity when simplifying expressions for the predicted value. The proof is a one-line rewrite that substitutes the unit choice c equals one and applies the multiplicative identity.
Claim. $hbar c = hbar$ in RS-native units, where $c = 1$ by definition and $hbar$ is the reduced Planck constant given by $phi^{-5}$.
background
The AlphaGScoreCard module computes the RS-native gravitational coupling $alpha_G^{RS} := G m_e^2 / (hbar c)$ using the in-framework constants from Constants and the electron structural mass. The reduced Planck constant is defined as $hbar = phi^{-5}$ in these units (Constants.hbar doc: Reduced Planck constant ħ in RS-native units: ħ = E_coh · τ₀ = φ⁻⁵ · 1). The speed of light satisfies the auxiliary result c_eq_one' : c = 1. Upstream arithmetic support comes from mul_one, which encodes the identity x * 1 = x.
proof idea
This is a one-line wrapper proof. It applies the rewrite tactic to substitute c = 1 from c_eq_one' and then invokes mul_one to reduce the product to the right-hand side.
why it matters
The result is invoked in alphaG_pred_eq and alphaG_pred_closed to simplify row_alphaG_pred to a closed phi-form. It fills the algebraic reduction step inside the gravitational coupling scorecard, consistent with the RS-native constants c = 1 and hbar = phi^{-5}. The module treats the comparison to CODATA alpha_G as a hypothesis bridge requiring an external dimensional map.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.