alphaG_pred_bracket
plain-language theorem explainer
The theorem establishes that the RS-native gravitational coupling alphaG_pred, defined via G times electron structural mass squared over hbar c, lies strictly between 4.5e9 and 4.85e9. Researchers validating phi-ladder mass predictions in Recognition Science cite this interval when checking coherence-mass outputs. The proof is a direct term-mode pairing of the separately established lower and upper bounds.
Claim. Let $m_e$ denote the electron structural mass and define $a_G := G m_e^2/ (hbar c)$. Then $4.5 times 10^9 < a_G < 4.85 times 10^9$.
background
The module treats the dimensionless gravitational coupling in RS-native coherence-mass units. The definition row_alphaG_pred computes G * electron_structural_mass^2 / (hbar * c) using the framework constants and the electron mass from Physics.ElectronMass. Module documentation identifies this as Phase 0 row P0-AG, notes the raw value is O(10^9) while the SI CODATA target is O(10^{-45}), and flags the result as a hypothesis bridge pending the dimensional map in DimensionalBridgeStructural. The upstream theorems alphaG_pred_lower and alphaG_pred_upper supply the concrete numerical bounds by applying phi inequalities (phi > 1.618 and phi < 1.6185) together with pi bounds and power estimates.
proof idea
The proof is a one-line term-mode wrapper that constructs the conjunction by pairing the theorems alphaG_pred_lower and alphaG_pred_upper.
why it matters
This bracket populates the native_bracket field of the AlphaGScoreCardCert definition, which also carries the not_codata disclaimer. It completes the Phase 0 gravitational-coupling row in the physical derivation plan. The result underscores the framework distinction between RS-native phi-ladder outputs and SI values, consistent with the T5 J-uniqueness and T6 phi fixed-point steps that generate the underlying mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.