Pith. sign in
theorem

row_neutron_threshold_pos

proved
show as:
module
IndisputableMonolith.Physics.NeutronGFactorScoreCard
domain
Physics
line
68 · github
papers citing
none yet

plain-language theorem explainer

The canonical residual threshold used by the neutron g-factor score card is strictly positive. Anyone assembling or citing the Phase-1 neutron magnetic-moment certificate needs this inequality as a structural side condition. The proof is a one-line wrapper that reuses the shared positivity lemma for that threshold.

Claim. The canonical residual threshold $T_{\mathrm{can}}$ satisfies $0 < T_{\mathrm{can}}$.

background

This module is Phase-1 row P1-C08 of the physical-derivation plan: a neutron g-factor score card. It records the CODATA targets $g_n \approx -3.82608545$ and $\mu_n \approx -1.91304273,\mu_N$, and certifies only structural J-cost facts already present in the nuclear neutron-magnetic-moment development. No derived numerical prediction for $g_n$ is claimed yet; the spin/strong-sector bridge is left as a named residual.

Score-card rows share a fixed positive cutoff, the canonical residual threshold, against which matched costs and residuals are judged. Positivity of that cutoff is a bookkeeping invariant of the certificate type, not a physics derivation. The surrounding rows already fix CODATA sign facts and nonnegativity/matching of the magnetic J-cost on the moment ratio.

proof idea

One-line wrapper: the goal $0 < \texttt{canonicalThreshold}$ is discharged by applying the shared lemma that the canonical threshold is positive. No neutron-specific algebra is performed.

why it matters

Feeds the aggregate certificate theorem that the neutron g-factor score-card certificate is inhabited: each structural field (negative CODATA $g$ and $\mu$ targets, matched magnetic cost, nonnegative cost, and positive threshold) must hold before the row can be marked theorem-grade support.

In the Recognition plan this is scaffolding for P1-C08, not a mass or coupling derivation. Landmarks such as T5 J-uniqueness and the RCL enter only indirectly via the imported neutron magnetic-moment J-cost facts. The open item remains the numerical spin/strong-sector bridge; until that bridge is stated, claiming a derived $g_n$ is false, and CODATA outside a declared interval would falsify the completed row.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.