alphaG_codata
plain-language theorem explainer
The declaration supplies the CODATA numerical target for the dimensionless gravitational coupling constant at the electron mass scale. Researchers auditing Recognition Science mass predictions against experiment cite this value when certifying scorecards that contrast native predictions against measured data. It enters as a direct numerical definition with no computation or proof obligations.
Claim. The CODATA target value for the dimensionless gravitational coupling is defined by the constant assignment $1.7518times10^{-45}$.
background
The module defines the predicted RS-native quantity as $alpha_G^{RS} := G m_e^2 / (hbar c)$ using the framework constants G, hbar, c and the structural electron mass. The present definition records the corresponding CODATA measurement target in SI units at the electron scale. The module doc flags this row as a hypothesis bridge alert because the RS-native prediction lies near $4.5times10^9$ while the SI number is $O(10^{-45})$, with the gap closed only by an explicit dimensional calibration map.
proof idea
Direct definition that assigns the literal floating-point constant 1.7518e-45 to the identifier.
why it matters
This constant supplies the experimental benchmark inside the AlphaGScoreCardCert structure and the two comparison theorems codata_very_small and native_very_not_codata. It implements the measurement side of phase-0 row P0-AG in the physical derivation plan, underscoring the open requirement for the dimensional bridge that converts coherence-mass reports to kilograms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.