alphaG_pred_upper
plain-language theorem explainer
The upper bound on the Recognition Science native-unit prediction for the electron gravitational coupling shows that this quantity lies strictly below 4.85 times 10 to the ninth. Researchers deriving mass ladders from the phi fixed point cite the result to complete the numerical bracket for the alpha_G scorecard entry. The proof substitutes the closed phi-form expression and chains strict inequalities on the golden ratio together with a lower bound on pi, reaching the target through linear arithmetic.
Claim. Let $alpha_G^{RS}$ denote the Recognition Science prediction $G m_e^2 / (hbar c)$ for the dimensionless gravitational coupling of the electron in native units, with $m_e$ the structural mass. Then $alpha_G^{RS} < 4.85 times 10^9$.
background
The AlphaGScoreCard module defines the predicted quantity as G multiplied by the square of the electron structural mass divided by hbar times c. This implements the RS-native formula for the gravitational fine-structure constant. The closed-form result rewrites the quantity as (2 to the power of negative 44 times phi to the 112) divided by pi, which follows from the forced electron mass 2 to the negative 22 times phi to the 51 together with algebraic power simplification. The bound phi less than 1.6185 is supplied by the PhiBounds module.
proof idea
The tactic proof first obtains phi less than 1.6185 by simplification from the golden-ratio bound theorem. It secures a lower bound on pi above 3.1415 via linarith on known pi facts. It then shows that the phi-powered term is strictly smaller than the 1.6185-powered term via the real-power strict inequality. These relations feed nlinarith to bound the closed expression below the target times pi; division by pi yields the inequality. The final substitution step transfers the bound to the predicted quantity.
why it matters
This declaration supplies the upper leg of the bracket theorem that sandwiches the native prediction between 4.5 times 10 to the 9 and 4.85 times 10 to the 9. It completes the numerical characterization of the phase-0 gravitational-coupling scorecard row. The bound is consistent with the phi self-similar fixed point and the mass-ladder construction. The result remains inside the hypothesis bridge; the scale mismatch with the CODATA measurement awaits the explicit dimensional-calibration map.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.