AlphaGScoreCardCert
plain-language theorem explainer
AlphaGScoreCardCert packages two numerical checks on the Recognition Science native prediction for the gravitational fine-structure constant. Researchers auditing the P0-AG scorecard row would cite it to record that the computed value lies inside the stated bracket and exceeds the CODATA target. The structure is introduced by direct definition of its two fields with no lemmas or computation required.
Claim. The structure asserts that the RS-native gravitational coupling satisfies $4.5times10^9 < G m_e^2/(hbar c) < 4.85times10^9$ and $1.7518times10^{-45} < G m_e^2/(hbar c)$, where $G$, $hbar$, $c$ and $m_e$ are the Recognition Science constants and structural electron mass.
background
In Recognition Science the gravitational coupling is written in native units as $alpha_G^{RS} := G m_e^2/(hbar c)$ using the constants $G=phi^5/pi$, $hbar=phi^{-5}$, $c=1$ and the structural electron mass from Physics.ElectronMass. The module contrasts this with the CODATA target stored as alphaG_codata. The upstream definition row_alphaG_pred supplies the explicit expression $Gcdot electron_structural_mass^2/(hbar c)$ while alphaG_codata holds the measured value 1.7518e-45. This row is tagged as a hypothesis bridge because the native result is order 10^9 while the SI dimensionless number is order 10^{-45}; the missing conversion is the dimensional bridge map.
proof idea
The declaration is a pure structure definition whose two fields are the bracket inequality and the ordering against codata. No lemmas are invoked; the fields are later instantiated by alphaG_pred_bracket and native_very_not_codata in the downstream cert definition.
why it matters
The structure supplies the concrete witness required by the cert definition, which immediately yields the inhabitedness theorem cert_inhabited. It documents the Phase 0 P0-AG row of the physical derivation plan and flags the open dimensional calibration between coherence-mass units and SI kilograms. The construction closes the local scorecard without reference to the forcing chain, RCL or phi-ladder steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.