IndisputableMonolith.Recognition.Certification

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace Recognition
   5namespace Certification
   6
   7noncomputable section
   8open Classical
   9
  10/-- Closed interval with endpoints `lo ≤ hi`. -/
  11structure Interval where
  12  lo : ℝ
  13  hi : ℝ
  14  lo_le_hi : lo ≤ hi
  15
  16@[simp] def memI (I : Interval) (x : ℝ) : Prop := I.lo ≤ x ∧ x ≤ I.hi
  17
  18@[simp] def width (I : Interval) : ℝ := I.hi - I.lo
  19
  20/-- If `x,y` lie in the same interval `I`, then `|x − y| ≤ width(I)`. -/
  21lemma abs_sub_le_width_of_memI {I : Interval} {x y : ℝ}
  22  (hx : memI I x) (hy : memI I y) : |x - y| ≤ width I := by
  23  have : I.lo ≤ x ∧ x ≤ I.hi := hx
  24  have : I.lo ≤ y ∧ y ≤ I.hi := hy
  25  have : x - y ≤ I.hi - I.lo := by linarith
  26  have : y - x ≤ I.hi - I.lo := by linarith
  27  have : -(I.hi - I.lo) ≤ x - y ∧ x - y ≤ I.hi - I.lo := by
  28    constructor
  29    · linarith
  30    · linarith
  31  simpa [width, abs_le] using this
  32
  33/-! ## Certificate schema -/
  34
  35/-- Anchor certificate: per-species residue intervals plus charge-wise gap intervals. -/
  36structure AnchorCert (Species : Type) where
  37  M0 : Interval
  38  Ires : Species → Interval
  39  center : Int → ℝ
  40  eps : Int → ℝ
  41  eps_nonneg : ∀ z, 0 ≤ eps z
  42
  43@[simp] def Igap {Species : Type} (C : AnchorCert Species) (z : Int) : Interval :=
  44{ lo := C.center z - C.eps z
  45, hi := C.center z + C.eps z
  46, lo_le_hi := by have := C.eps_nonneg z; linarith }
  47
  48/-- Validity of a certificate w.r.t. a charge map `Z` and display function `Fgap`. -/
  49structure Valid {Species : Type} (Z : Species → Int) (Fgap : Int → ℝ) (C : AnchorCert Species) : Prop where
  50  M0_pos : 0 < C.M0.lo
  51  Fgap_in : ∀ i : Species, memI (Igap C (Z i)) (Fgap (Z i))
  52  Ires_in_Igap : ∀ i : Species,
  53    (Igap C (Z i)).lo ≤ (C.Ires i).lo ∧ (C.Ires i).hi ≤ (Igap C (Z i)).hi
  54
  55lemma M0_pos_of_cert {Species : Type} {Z : Species → Int} {Fgap : Int → ℝ}
  56    {C : AnchorCert Species} (hC : Valid Z Fgap C) : 0 < C.M0.lo :=
  57  hC.M0_pos
  58
  59/-- Certificate replacement for the anchor identity (inequality form). -/
  60lemma anchorIdentity_cert {Species : Type} {Z : Species → Int} {Fgap : Int → ℝ}
  61    {C : AnchorCert Species} (hC : Valid Z Fgap C)
  62  (res : Species → ℝ) (hres : ∀ i, memI (C.Ires i) (res i)) :
  63  ∀ i : Species, |res i - Fgap (Z i)| ≤ 2 * C.eps (Z i) := by
  64  intro i
  65  have hF : memI (Igap C (Z i)) (Fgap (Z i)) := hC.Fgap_in i
  66  have hI : (Igap C (Z i)).lo ≤ (C.Ires i).lo ∧ (C.Ires i).hi ≤ (Igap C (Z i)).hi :=
  67    hC.Ires_in_Igap i
  68  have hr : memI (Igap C (Z i)) (res i) := by
  69    have hr0 := hres i
  70    refine ⟨le_trans hI.1 hr0.1, le_trans hr0.2 hI.2⟩
  71  have hbound :=
  72    abs_sub_le_width_of_memI (I := Igap C (Z i)) (x := res i) (y := Fgap (Z i)) hr hF
  73  -- width(Igap) = 2*eps
  74  have hw :
  75      width (Igap C (Z i)) = 2 * C.eps (Z i) := by
  76    simp [Igap, width]
  77    ring
  78  simpa [hw, two_mul] using hbound
  79
  80/-- Equal‑Z degeneracy (inequality form) from a certificate. -/
  81lemma equalZ_residue_of_cert {Species : Type} {Z : Species → Int} {Fgap : Int → ℝ}
  82    {C : AnchorCert Species} (hC : Valid Z Fgap C)
  83  (res : Species → ℝ) (hres : ∀ i, memI (C.Ires i) (res i))
  84  {i j : Species} (hZ : Z i = Z j) :
  85  |res i - res j| ≤ 2 * C.eps (Z i) := by
  86  have hI_i : (Igap C (Z i)).lo ≤ (C.Ires i).lo ∧ (C.Ires i).hi ≤ (Igap C (Z i)).hi :=
  87    hC.Ires_in_Igap i
  88  have hI_j : (Igap C (Z j)).lo ≤ (C.Ires j).lo ∧ (C.Ires j).hi ≤ (Igap C (Z j)).hi :=
  89    hC.Ires_in_Igap j
  90  have hres_i : memI (Igap C (Z i)) (res i) := by
  91    have hr0 := hres i
  92    exact ⟨le_trans hI_i.1 hr0.1, le_trans hr0.2 hI_i.2⟩
  93  have hres_j : memI (Igap C (Z i)) (res j) := by
  94    have hr0 := hres j
  95    have hlo_j : (Igap C (Z i)).lo ≤ (C.Ires j).lo := by simpa [hZ] using hI_j.1
  96    have hhi_j : (C.Ires j).hi ≤ (Igap C (Z i)).hi := by simpa [hZ] using hI_j.2
  97    exact ⟨le_trans hlo_j hr0.1, le_trans hr0.2 hhi_j⟩
  98  have hbound :=
  99    abs_sub_le_width_of_memI (I := Igap C (Z i)) (x := res i) (y := res j) hres_i hres_j
 100  have hw :
 101      width (Igap C (Z i)) = 2 * C.eps (Z i) := by
 102    simp [Igap, width]
 103    ring
 104  simpa [hw, two_mul] using hbound
 105
 106/-! ### Zero-width anchor certificate (exact equality) -/
 107
 108/-- Zero-width certificate: each interval collapses to the center value `Fgap(Z i)`. -/
 109noncomputable def zeroWidthCert {Species : Type} (Z : Species → Int) (Fgap : Int → ℝ) : AnchorCert Species :=
 110{ M0 := { lo := 1, hi := 1, lo_le_hi := by norm_num }
 111, Ires := fun i => { lo := Fgap (Z i), hi := Fgap (Z i), lo_le_hi := by linarith }
 112, center := fun z => Fgap z
 113, eps := fun _ => 0
 114, eps_nonneg := by intro _; norm_num }
 115
 116lemma zeroWidthCert_valid {Species : Type} (Z : Species → Int) (Fgap : Int → ℝ) :
 117    Valid Z Fgap (zeroWidthCert Z Fgap) := by
 118  refine {
 119    M0_pos := by simp [zeroWidthCert]
 120  , Fgap_in := by
 121      intro i
 122      dsimp [zeroWidthCert, Igap, memI]
 123      constructor <;> linarith
 124  , Ires_in_Igap := by
 125      intro i
 126      dsimp [zeroWidthCert, Igap]
 127      constructor <;> linarith
 128  }
 129
 130/-- Exact anchor identity from a zero-width certificate. -/
 131lemma anchorIdentity_of_zeroWidthCert {Species : Type} (Z : Species → Int) (Fgap : Int → ℝ)
 132    (res : Species → ℝ) (hres : ∀ i, memI ((zeroWidthCert Z Fgap).Ires i) (res i)) :
 133  ∀ i : Species, res i = Fgap (Z i) := by
 134  intro i
 135  have h := hres i
 136  dsimp [zeroWidthCert, memI] at h
 137  exact le_antisymm h.2 h.1
 138
 139end
 140
 141end Certification
 142end Recognition
 143end IndisputableMonolith
 144