row_alphaG_pred_eq
The equality sets the RS-native gravitational coupling α_G^RS equal to G times the square of the electron structural mass divided by ħc. Researchers closing the Phase 0 P0-AG scorecard row in Recognition Science mass derivations cite this when confirming the native-unit expression. The proof is a one-line reflexivity that unfolds the definition of row_alphaG_pred.
claim$α_G^{RS} = G m_e^2 / (ℏ c)$ where $m_e$ is the electron structural mass and the constants G, ℏ, c are taken from the RS-native definitions.
background
The module defines the gravitational coupling scorecard row P0-AG as the dimensionless quantity α_G^RS := G m_e² / (ℏ c) in RS-native units. Here G is the gravitational constant expressed as λ_rec² c³ / (π ℏ), ℏ is the reduced Planck constant φ^{-5} in coherence units, and m_e is the electron structural mass imported from the electron mass module. The local setting treats this as a hypothesis bridge that records the native prediction before any external calibration map converts coherence masses to SI kilograms.
proof idea
The proof is a direct reflexivity after row_alphaG_pred expands to the explicit product G * electron_structural_mass ^ 2 / (hbar * c). No additional lemmas are applied; the term mode simply matches the unfolded definition.
why it matters in Recognition Science
This theorem supplies the closed native-unit form for the Phase 0 alpha_G scorecard entry. It feeds the subsequent results alphaG_pred_eq, alphaG_pred_closed, alphaG_pred_lower and alphaG_pred_upper in the same module. Within the Recognition framework it links the J-cost-derived G to the phi-ladder electron mass, underscoring the dimensional bridge required before any comparison with the CODATA value 1.7518 × 10^{-45}.
scope and limits
- Does not claim numerical equality between the RS-native value and the CODATA measurement.
- Does not derive the explicit forms of G or the electron structural mass.
- Does not incorporate the dimensional bridge map from coherence units to kilograms.
- Does not address multi-electron or higher-rung corrections to the mass formula.
formal statement (Lean)
51theorem row_alphaG_pred_eq : row_alphaG_pred = G * electron_structural_mass ^ 2 / (hbar * c) := rfl
proof body
Term-mode proof.
52
53/-! ## Helper algebra (native units) -/
54