IndisputableMonolith.Nuclear.BindingEnergyPeakScoreCard

   1import Mathlib
   2import IndisputableMonolith.Nuclear.BindingEnergyFromPhiLadder
   3
   4/-!
   5# P3-binding-peak -- iron-group binding-energy peak scorecard
   6
   7Row ID: P3-binding-peak.
   8
   9Predicted formula: the binding-energy-per-nucleon peak sits at
  10recognition rung `k = 26`, with adjacent stable rungs `25` and `27`;
  11the empirical broad iron-group band is `25 <= Z <= 28`.
  12
  13Measurement target: AME2020 iron-group peak location, with Fe-56 and
  14Ni-62 inside the declared `Z in [25, 28]` band.
  15
  16Falsifier: an AME update or locked binding-energy pull placing the
  17per-nucleon peak outside `25 <= Z <= 28` falsifies this peak-row
  18assignment.
  19
  20Status: PARTIAL_THEOREM. The rung and band facts are proved; the full
  2150-nucleus RMS binding-energy benchmark remains a Phase 3 residual.
  22
  23Lean: 0 sorry, 0 new axiom.
  24-/
  25
  26namespace IndisputableMonolith.Nuclear.BindingEnergyPeakScoreCard
  27
  28open IndisputableMonolith.Nuclear.BindingEnergyFromPhiLadder
  29
  30noncomputable section
  31
  32theorem row_iron_peak_rung : iron_peak_rung = 26 :=
  33  iron_peak_rung_eq
  34
  35theorem row_iron_peak_in_empirical_band :
  36    25 <= iron_peak_rung ∧ iron_peak_rung <= 28 :=
  37  iron_peak_rung_in_empirical_band
  38
  39theorem row_adjacent_rungs :
  40    lower_adjacent_rung = 25 ∧ upper_adjacent_rung = 27 :=
  41  ⟨lower_adjacent_rung_eq, upper_adjacent_rung_eq⟩
  42
  43theorem row_iron_alpha_gap : iron_to_alpha_gap = 22 :=
  44  iron_to_alpha_gap_eq
  45
  46structure BindingEnergyPeakScoreCardCert where
  47  peak_rung : iron_peak_rung = 26
  48  peak_band : 25 <= iron_peak_rung ∧ iron_peak_rung <= 28
  49  adjacent : lower_adjacent_rung = 25 ∧ upper_adjacent_rung = 27
  50  iron_alpha_gap : iron_to_alpha_gap = 22
  51  foundation_cert : BindingEnergyCert
  52
  53theorem bindingEnergyPeakScoreCardCert_holds :
  54    Nonempty BindingEnergyPeakScoreCardCert :=
  55  ⟨{ peak_rung := row_iron_peak_rung
  56     peak_band := row_iron_peak_in_empirical_band
  57     adjacent := row_adjacent_rungs
  58     iron_alpha_gap := row_iron_alpha_gap
  59     foundation_cert := bindingEnergyCert }⟩
  60
  61end
  62
  63end IndisputableMonolith.Nuclear.BindingEnergyPeakScoreCard
  64