row_neutron_g_codata
plain-language theorem explainer
Records the CODATA/PDG neutron g-factor as the real constant -3.82608545. Anyone building or citing the neutron magnetic-moment score card uses this as the measurement anchor. It is a bare numerical definition with no proof obligations.
Claim. The CODATA/PDG neutron $g$-factor target is the real number $g_n^{\mathrm{CODATA}} = -3.82608545$ (dimensionless).
background
This module is the Phase-1 score card for the neutron $g$-factor (row P1-C08). Recognition Science already supplies structural J-cost certificates for magnetic-moment ratios, but does not yet derive a numerical neutron $g$ from the spin/strong sector. The measurement target is therefore frozen as an external CODATA/PDG constant.
Equivalently one may quote $\mu_n \approx -1.91304273,\mu_N$. The score card keeps both the $g$ and $\mu/\mu_N$ anchors, proves only sign and J-cost structural facts, and names the missing numerical bridge as a residual proposition. Lean status of the module is zero sorry and zero axiom.
proof idea
Pure definition: the real literal $-3.82608545$ is assigned with no tactics, lemmas, or computation. Downstream theorems that need the sign simply unfold this constant and discharge the inequality by norm_num.
why it matters
Anchors every quantitative claim in the neutron $g$-factor score card. The residual NeutronGFactorResidual demands a predicted $g_{\mathrm{pred}}$ within relative $10^{-6}$ of this target. The certificate structure NeutronGFactorScoreCardCert requires the target to be negative, and the theorem row_neutron_g_codata_negative discharges that field by unfolding the constant. Until a spin/strong-sector bridge produces a derived number, claiming that $g_n$ is forced by the Recognition chain (T0–T8, RCL, phi-ladder) would be false; this definition keeps the measurement side honest while structural J-cost facts are already certified.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.