NeutronGFactorResidual
plain-language theorem explainer
Names the residual proposition that a Recognition-derived neutron g-factor exists within relative error 10^{-6} of the CODATA value g_n ≈ -3.82608545. Score-card and planning consumers cite it as the open spin/strong-sector numerical bridge (P1-C08). The body is a pure existential definition over the CODATA target constant, not a derivation.
Claim. There exists a real prediction $g_{\mathrm{pred}}$ such that $\frac{|g_{\mathrm{pred}} - g_n^{\mathrm{CODATA}}|}{|g_n^{\mathrm{CODATA}}|} < 10^{-6}$, where $g_n^{\mathrm{CODATA}} = -3.82608545$ is the fixed CODATA/PDG neutron $g$-factor target.
background
This module is Phase 1 row P1-C08 of the physical derivation plan: a neutron $g$-factor score card. CODATA/PDG fix the measurement target $g_n \approx -3.82608545$ (equivalently $\mu_n \approx -1.91304273,\mu_N$). The codebase already carries structural J-cost-on-ratio facts for the neutron magnetic moment row, but no derived numerical $g_n$ from the spin/strong sector.
The upstream constant row_neutron_g_codata is exactly that CODATA target as a real. The residual packages the missing numerical claim as a named proposition: existence of some real prediction inside a $10^{-6}$ relative window of that target. Module status is zero sorry and zero axiom; only structure is proved so far.
proof idea
Definition, not a theorem. The body is the existential proposition $\exists g_{\mathrm{pred}}:\mathbb{R}$ with relative distance to the CODATA neutron $g$ target strictly below $10^{-6}$. No lemmas are applied; the right-hand side is the residual predicate itself.
why it matters
Holds the open numerical slot on the neutron $g$ score card. Downstream, NeutronGFactorScoreCardCert bundles only structural facts (negative CODATA $g$ and $\mu$ targets, matched and nonnegative domain cost, positive canonical threshold) and does not discharge this residual. The identity theorem row_neutron_g_residual_named merely pins the name for planning references.
In framework terms this sits after magnetic-moment J-cost structure and before a spin/strong-sector bridge that would produce $g_n$ on the $\phi$-ladder or related RS numerics. Until that bridge exists, claiming a derived neutron $g$ is false; the residual makes that gap explicit for P1-C08.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.