codata_very_small
plain-language theorem explainer
The declaration establishes that the CODATA value for the gravitational coupling alpha_G equals 1.7518 times 10 to the minus 45 and therefore lies below 10 to the minus 40. Researchers comparing Recognition Science native predictions to experimental scales cite this bound to document the numerical separation at the electron mass. The proof is a one-line wrapper that unfolds the constant definition and applies numerical normalization.
Claim. Let $alpha_G^{CODATA} := 1.7518 times 10^{-45}$. Then $alpha_G^{CODATA} < 10^{-40}$.
background
The module records the dimensionless gravitational coupling in the Masses domain as phase 0 row P0-AG. It defines the RS-native form alpha_G^{RS} := G m_e^2 / (hbar c) using Constants.G, Constants.hbar, Constants.c and the electron structural mass, then contrasts this with the experimental CODATA target of order 10^{-45}. The upstream definition alphaG_codata supplies the concrete numerical constant 1.7518e-45 used for the comparison. The module notes that any direct numerical match remains a hypothesis pending the dimensional bridge in DimensionalBridgeStructural.lean.
proof idea
The proof is a one-line wrapper that unfolds alphaG_codata to expose the literal value 1.7518e-45 and invokes norm_num to discharge the inequality against 1e-40.
why it matters
The bound anchors the alphaG scorecard by recording the extreme smallness of the measured coupling at electron scale. It fills the P0-AG row in the physical derivation plan and highlights the open dimensional mismatch between RS-native O(10^9) predictions and the SI O(10^{-45}) datum. No downstream theorems depend on it, so the result functions as a reference fact rather than an active lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.