NeutronGFactorScoreCardCert
plain-language theorem explainer
Certificate bundle for the neutron g-factor score card (planning row P1-C08): CODATA g and mu/mu_N targets are negative, domain cost vanishes on equal nonzero ratios and is nonnegative on positives, the canonical threshold is positive, and the spin/strong residual is named. Anyone auditing structural readiness of the neutron magnetic row cites it. Pure structure definition; fields are Prop obligations discharged by a later Nonempty witness.
Claim. A neutron $g$-factor score-card certificate is a record of six facts: the CODATA neutron $g$ target satisfies $g_n<0$; the CODATA neutron magnetic moment in nuclear magnetons satisfies $\mu_n/\mu_N<0$; for every nonzero real $r$, the domain cost of the ratio $r$ against itself is zero; for all positive reals $m,e$, domain cost is nonnegative; the canonical threshold is strictly positive; and the named residual proposition (existence of a $g$ prediction within relative $10^{-6}$ of CODATA) is identical to itself.
background
This module is Phase 1 row P1-C08 of the physical derivation plan. It records CODATA/PDG targets $g_n\approx -3.82608545$ and $\mu_n\approx -1.91304273,\mu_N$, and packages only the structural J-cost facts already available. The codebase does not yet contain a derived numerical prediction for the neutron $g$ factor.
Domain cost is the recognition cost on a ratio of positive scales; matched equal arguments sit at the J-cost minimum (cost zero), and cost is nonnegative for positive inputs, matching the upstream ObserverForcing fact that every recognition event has nonnegative cost. The named residual is the open Prop that some predicted $g$ lies within relative $10^{-6}$ of the CODATA $g$ target: a spin/strong-sector bridge still to be derived.
The certificate is therefore a structural readiness object, not a numerical derivation.
proof idea
No proof body: the declaration is a structure whose fields are named Prop obligations. Downstream, neutronGFactorScoreCardCert_holds builds a term of this type by filling each field from sibling lemmas (negativity of the two CODATA rows, matched and nonnegative domain-cost facts, positivity of the canonical threshold, and rfl on the residual name).
why it matters
The structure is the typed interface for row P1-C08. Its sole consumer is neutronGFactorScoreCardCert_holds, which proves the certificate is inhabited and thereby marks the neutron magnetic score card as structurally closed under existing J-cost machinery.
Framework role is bookkeeping, not forcing: T5 J-uniqueness and the Recognition Composition Law underwrite the cost fields, but the numerical $g_n$ prediction remains the named residual. Module doc is explicit: claiming $g_n$ is derived is false until the spin/strong-sector bridge is stated; once stated, CODATA outside the declared interval falsifies the row. Lean status is zero sorry and zero axiom on the structural side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.