alphaG_pred_lower
plain-language theorem explainer
The theorem establishes a strict lower bound of 4.5 billion on the RS-native prediction for the dimensionless gravitational coupling alpha_G^RS. Researchers working on the Recognition Science mass ladder and dimensionless constants cite it when bracketing the predicted value for the alpha_G score card. The proof chains numeric bounds on phi above 1.618 and pi below 3.142, then applies nlinarith after algebraic rearrangement of the closed phi-form expression.
Claim. $4.5times10^9<alpha_G^{rm RS}$ where $alpha_G^{rm RS}:=G m_e^2/(hbar c)$ denotes the RS-native prediction in coherence-mass units.
background
In the Recognition Science framework the dimensionless gravitational coupling is defined as alpha_G^RS := G m_e^2 / (hbar c) using the in-framework constants Constants.G, Constants.hbar, Constants.c and the electron structural mass from Physics.ElectronMass. The module treats this as Phase 0 row P0-AG, noting that the raw RS-native value lies near 10^9 while the SI CODATA value is near 10^{-45}; the gap is closed only by the dimensional bridge in DimensionalBridgeStructural. Upstream results include the phi-forcing structure from PhiForcingDerived.of and the ledger factorization from DAlembert.LedgerFactorization.of that supply the closed phi-form used here.
proof idea
The tactic proof first obtains hφ : phi > 1.618 via phi_gt_1618 and hpiUB : pi < 3.142 via Real.pi_lt_d6. It then shows 2^{-44} * 1.618^{112} < 2^{-44} * phi^{112} by Real.rpow_lt_rpow, feeds the comparison into nlinarith to bound 4.5e9 * pi below 2^{-44} * phi^{112}, and finally rewrites the division to reach the target inequality. The last step simplifies directly with alphaG_pred_closed.
why it matters
The result supplies the lower half of alphaG_pred_bracket and is invoked by native_very_not_codata to separate the native prediction from the CODATA number. It fills the Phase 0 row P0-AG of the physical derivation plan and underscores the open dimensional-calibration question that must be resolved before any direct numerical match with experiment. The bound is consistent with the phi-ladder mass formula and T5 J-uniqueness but remains a conservative numeric verification rather than a derivation from the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.