IndisputableMonolith.Physics.NeutronGFactorScoreCard

   1import Mathlib
   2import IndisputableMonolith.Nuclear.Neutron_Magnetic_Moment_RS
   3
   4/-!
   5# Neutron g-Factor Score Card
   6
   7Phase 1 row **P1-C08** in `planning/PHYSICAL_DERIVATION_PLAN.md`.
   8
   9## Statement
  10
  11The current theorem-grade support is structural: the neutron magnetic
  12moment row has a J-cost-on-ratio certificate, but the codebase does not
  13yet contain a derived numerical prediction for the neutron `g` factor.
  14
  15## Measurement target
  16
  17CODATA / PDG:
  18
  19`g_n ≈ -3.82608545` (dimensionless), equivalently
  20`μ_n ≈ -1.91304273 μ_N`.
  21
  22This module records the CODATA target and proves only the structural
  23J-cost facts already available. The numerical spin/strong-sector bridge
  24is named as the residual.
  25
  26Falsifier: once the neutron spin-sector bridge is stated, CODATA outside
  27the declared interval falsifies the row; until then, claiming `g_n` is
  28derived is false.
  29
  30## Lean status: 0 sorry, 0 axiom
  31-/
  32
  33namespace IndisputableMonolith.Physics.NeutronGFactorScoreCard
  34
  35open IndisputableMonolith.Nuclear.Neutron_Magnetic_Moment_RS
  36
  37noncomputable section
  38
  39/-- CODATA/PDG neutron g-factor target. -/
  40def row_neutron_g_codata : ℝ := -3.82608545
  41
  42/-- CODATA neutron magnetic moment target in nuclear magnetons. -/
  43def row_neutron_mu_over_muN_codata : ℝ := -1.91304273
  44
  45/-- Named residual: derive a neutron spin/strong-sector numerical `g_n`. -/
  46def NeutronGFactorResidual : Prop :=
  47  ∃ g_pred : ℝ,
  48    |g_pred - row_neutron_g_codata| / |row_neutron_g_codata| < (1e-6 : ℝ)
  49
  50theorem row_neutron_g_codata_negative :
  51    row_neutron_g_codata < 0 := by
  52  unfold row_neutron_g_codata
  53  norm_num
  54
  55theorem row_neutron_mu_codata_negative :
  56    row_neutron_mu_over_muN_codata < 0 := by
  57  unfold row_neutron_mu_over_muN_codata
  58  norm_num
  59
  60theorem row_neutron_magnetic_cost_matched (r : ℝ) (h : r ≠ 0) :
  61    domainCost r r = 0 :=
  62  domainCost_at_eq r h
  63
  64theorem row_neutron_magnetic_cost_nonneg (m e : ℝ) (hm : 0 < m) (he : 0 < e) :
  65    0 ≤ domainCost m e :=
  66  domainCost_nonneg m e hm he
  67
  68theorem row_neutron_threshold_pos :
  69    0 < canonicalThreshold :=
  70  canonicalThreshold_pos
  71
  72theorem row_neutron_g_residual_named :
  73    NeutronGFactorResidual = NeutronGFactorResidual := rfl
  74
  75structure NeutronGFactorScoreCardCert where
  76  g_target_negative : row_neutron_g_codata < 0
  77  mu_target_negative : row_neutron_mu_over_muN_codata < 0
  78  cost_matched : ∀ r : ℝ, r ≠ 0 → domainCost r r = 0
  79  cost_nonneg : ∀ m e : ℝ, 0 < m → 0 < e → 0 ≤ domainCost m e
  80  threshold_pos : 0 < canonicalThreshold
  81  residual_named : NeutronGFactorResidual = NeutronGFactorResidual
  82
  83theorem neutronGFactorScoreCardCert_holds :
  84    Nonempty NeutronGFactorScoreCardCert :=
  85  ⟨{ g_target_negative := row_neutron_g_codata_negative
  86     mu_target_negative := row_neutron_mu_codata_negative
  87     cost_matched := row_neutron_magnetic_cost_matched
  88     cost_nonneg := row_neutron_magnetic_cost_nonneg
  89     threshold_pos := row_neutron_threshold_pos
  90     residual_named := row_neutron_g_residual_named }⟩
  91
  92end
  93
  94end IndisputableMonolith.Physics.NeutronGFactorScoreCard
  95