Physics Neutron Gfactor Score Card

The neutron g-factor score card

The neutron, though electrically neutral, carries a magnetic moment: it behaves like a tiny bar magnet. Its g-factor is the dimensionless number that sets the strength of that magnet in units of the nuclear magneton. The accepted value, from CODATA/PDG, is g_n ≈ −3.82608545, equivalently a magnetic moment μ_n ≈ −1.91304273 μ_N. The negative sign means the neutron's spin and its magnetic moment point in opposite directions, a fact that has been measured precisely and is not in dispute.

In Recognition Science, the score card is a formal record of what the framework's machinery has and has not established for this row of its physical derivation plan. The framework models physical quantities through a recognition cost, a forced measure of how expensive it is for reality to register a ratio between two quantities. The score card proves the structural facts: the cost of matching a quantity to itself is zero, the cost is never negative for positive inputs, and the canonical threshold is positive. These are theorem-grade results, machine-checked in the framework's library of formal theorems, and they certify that the neutron's magnetic row is consistent with the cost structure.

What the score card does not do is derive the number −3.82608545. The numerical bridge from the neutron's spin and strong-sector structure to a predicted g-factor is named as a residual: a named open problem within the framework. The falsifier is explicit: once that bridge is stated, a CODATA value outside the declared interval would refute the row. Until then, claiming the g-factor is derived would be false. The score card records the target, proves the structural cost facts, and leaves the numerical derivation as a clearly marked target.

The practical consequence is a clean separation between what the framework has earned and what it has not. A reader can see at a glance that the neutron magnetic moment is a measured input, not a derived output, and that the framework's contribution today is structural consistency, not a new prediction. That honesty is the point of a score card.

/-- CODATA/PDG neutron g-factor target. -/
def row_neutron_g_codata : ℝ := -3.82608545

/-- CODATA neutron magnetic moment target in nuclear magnetons. -/
def row_neutron_mu_over_muN_codata : ℝ := -1.91304273

theorem row_neutron_magnetic_cost_matched (r : ℝ) (h : r ≠ 0) :
    domainCost r r = 0 :=
  domainCost_at_eq r h

theorem row_neutron_magnetic_cost_nonneg (m e : ℝ) (hm : 0 < m) (he : 0 < e) :
    0 ≤ domainCost m e :=
  domainCost_nonneg m e hm he

theorem row_neutron_threshold_pos :
    0 < canonicalThreshold :=
  canonicalThreshold_pos

/-- Named residual: derive a neutron spin/strong-sector numerical `g_n`. -/
def NeutronGFactorResidual : Prop :=
  ∃ g_pred : ℝ,
    |g_pred - row_neutron_g_codata| / |row_neutron_g_codata| < (1e-6 : ℝ)

What this page does not claim

The neutron g-factor is derived from the framework; it is a measured target. The score card proves any numerical prediction for the neutron's magnetic moment. The cost theorems here are specific to the neutron; they are general structural facts.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Physics/NeutronGFactorScoreCard.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: