cert
plain-language theorem explainer
The cert definition assembles the AlphaGScoreCardCert structure for the RS-native gravitational coupling. It packages the interval 4.5e9 < row_alphaG_pred < 4.85e9 with the strict separation from the CODATA value. Researchers auditing dimensionless constants in Recognition Science cite this to record the native prediction scale before any external calibration. The construction is a direct structure instantiation that applies the bracket theorem and the separation lemma.
Claim. Let $a_G^{RS}$ denote the RS-native prediction of $G m_e^2/ (hbar c)$. The certificate cert satisfies $4.5 times 10^9 < a_G^{RS} < 4.85 times 10^9$ and $a_G^{CODATA} < a_G^{RS}$.
background
The module records the gravitational coupling score card for phase 0 row P0-AG. It defines the RS-native value as $alpha_G^{RS} := G m_e^2 / (hbar c)$ using Constants.G, Constants.hbar, Constants.c and the electron structural mass. The module notes that this row is a hypothesis bridge alert: the raw RS-native value is O(10^9) while the SI dimensionless number is O(10^{-45}), so any comparison requires the dimensional bridge map from coherence mass to kilograms. Upstream, alphaG_pred_bracket supplies the closed interval theorem and native_very_not_codata supplies the separation alphaG_codata < row_alphaG_pred via lower bound and norm_num comparison.
proof idea
The definition is a direct structure instantiation of AlphaGScoreCardCert. It assigns the native_bracket field to the result of alphaG_pred_bracket and the not_codata field to native_very_not_codata.
why it matters
This definition completes the score card certificate for the gravitational coupling row. It supports the hypothesis bridge alert stated in the module documentation and records the phi-ladder prediction scale before the ExternalCalibration mass map is applied. In the Recognition framework it sits inside the Masses domain and precedes any claim that would identify the native value with the measured alpha_G without the dimensional conversion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.