IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealOrderCongruence

   1/-
   2  PrimitiveRecognitionCalculus/RealOrderCongruence.lean
   3
   4  Round-trip source:
   5    δ/PRC_Universal_Foundation_Execution_Plan_20260526.html
   6
   7  Spec anchor:
   8    Build Order step 10d: prove that the eventual non-strict order candidate
   9    descends to the null-distance quotient.
  10
  11  The proof uses verifier rationals only to read the J-cost distance as an
  12  ordinary small increment. The order statement itself remains over PRC raw
  13  ledgers.
  14-/
  15
  16import Mathlib
  17import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealProductContinuity
  18
  19namespace IndisputableMonolith
  20namespace Foundation
  21namespace PrimitiveRecognitionCalculus
  22
  23private theorem rat_sq_lt_sq_bounds {x gamma : ℚ}
  24    (hgamma : 0 < gamma) (hsq : x * x < gamma * gamma) :
  25    -gamma < x ∧ x < gamma := by
  26  constructor
  27  · by_contra hnot
  28    have hxle : x ≤ -gamma := by linarith
  29    have hnonneg : 0 ≤ -x - gamma := by linarith
  30    have hprod : 0 ≤ (-x - gamma) * (-x + gamma) := by
  31      have hright : 0 ≤ -x + gamma := by linarith
  32      exact mul_nonneg hnonneg hright
  33    nlinarith
  34  · by_contra hnot
  35    have hxge : gamma ≤ x := by linarith
  36    have hnonneg : 0 ≤ x - gamma := by linarith
  37    have hprod : 0 ≤ (x - gamma) * (x + gamma) := by
  38      have hright : 0 ≤ x + gamma := by linarith
  39      exact mul_nonneg hnonneg hright
  40    nlinarith
  41
  42theorem PRCJCostDistance_sq_diff_lt_of_lt_modulus
  43    {a b eta delta : PRCRat}
  44    (heta : PRCRat.positive eta)
  45    (hdelta_pos : PRCRat.positive delta)
  46    (hdelta_le :
  47      delta.toRat ≤ eta.toRat * eta.toRat / (4 * (1 + eta.toRat)))
  48    (hsmall : PRCRat.lt (PRCJCostDistance a b) delta) :
  49    (a.toRat - b.toRat) * (a.toRat - b.toRat) < eta.toRat := by
  50  have heta_pos : 0 < eta.toRat := (PRCRat.positive_iff_toRat_pos eta).mp heta
  51  have hdelta_pos_rat : 0 < delta.toRat :=
  52    (PRCRat.positive_iff_toRat_pos delta).mp hdelta_pos
  53  have hdisplay :
  54      PRCJCostDistanceIncrementDisplay (a.toRat - b.toRat) < delta.toRat := by
  55    rw [PRCRat.lt_iff_toRat_lt] at hsmall
  56    rw [PRCJCostDistance_toRat, PRCJCostDistanceRatDisplay_as_increment] at hsmall
  57    exact hsmall
  58  exact PRCJCostDistance_sq_lt_of_display_lt_delta
  59    (t := a.toRat - b.toRat) (eta := eta.toRat) (delta := delta.toRat)
  60    heta_pos hdelta_pos_rat hdelta_le hdisplay
  61
  62theorem PRCJCostDistance_abs_diff_lt_of_lt_order_delta
  63    {a b gamma delta : PRCRat}
  64    (hgamma : PRCRat.positive gamma)
  65    (hdelta_pos : PRCRat.positive delta)
  66    (hdelta_le :
  67      delta.toRat ≤
  68        (gamma.toRat * gamma.toRat) * (gamma.toRat * gamma.toRat) /
  69          (4 * (1 + gamma.toRat * gamma.toRat)))
  70    (hsmall : PRCRat.lt (PRCJCostDistance a b) delta) :
  71    -gamma.toRat < a.toRat - b.toRat ∧
  72      a.toRat - b.toRat < gamma.toRat := by
  73  let eta : PRCRat := gamma * gamma
  74  have heta : PRCRat.positive eta := by
  75    rw [PRCRat.positive_iff_toRat_pos]
  76    have hgamma_pos : 0 < gamma.toRat :=
  77      (PRCRat.positive_iff_toRat_pos gamma).mp hgamma
  78    simp [eta, PRCRat.toRat_mul]
  79    nlinarith
  80  have heta_toRat : eta.toRat = gamma.toRat * gamma.toRat := by
  81    simp [eta, PRCRat.toRat_mul]
  82  have hsq :
  83      (a.toRat - b.toRat) * (a.toRat - b.toRat) <
  84        gamma.toRat * gamma.toRat := by
  85    have hcore := PRCJCostDistance_sq_diff_lt_of_lt_modulus
  86      (a := a) (b := b) (eta := eta) (delta := delta)
  87      heta hdelta_pos (by simpa [heta_toRat] using hdelta_le) hsmall
  88    simpa [heta_toRat] using hcore
  89  exact rat_sq_lt_sq_bounds
  90    ((PRCRat.positive_iff_toRat_pos gamma).mp hgamma) hsq
  91
  92theorem PRCRawEventuallyLe_of_null_equiv
  93    {u u' v v' : PRCCauchySeq}
  94    (huu : PRCNullEquivalent u u')
  95    (hvv : PRCNullEquivalent v v')
  96    (hle : PRCRawEventuallyLe u.raw v.raw) :
  97    PRCRawEventuallyLe u'.raw v'.raw := by
  98  intro eps heps
  99  let two : PRCRat := (1 : PRCRat) + (1 : PRCRat)
 100  let four : PRCRat := two * two
 101  let gamma : PRCRat := eps * (four⁻¹)
 102  let eta : PRCRat := gamma * gamma
 103  let delta : PRCRat := (eta * eta) * ((four * ((1 : PRCRat) + eta))⁻¹)
 104  have heps_pos : 0 < eps.toRat :=
 105    (PRCRat.positive_iff_toRat_pos eps).mp heps
 106  have htwo : two.toRat = (2 : ℚ) := by
 107    dsimp [two]
 108    change (PRCRat.add PRCRat.one PRCRat.one).toRat = (2 : ℚ)
 109    rw [PRCRat.toRat_add, PRCRat.one_toRat]
 110    norm_num
 111  have hfour : four.toRat = (4 : ℚ) := by
 112    dsimp [four]
 113    change (PRCRat.mul two two).toRat = (4 : ℚ)
 114    rw [PRCRat.toRat_mul]
 115    norm_num [htwo]
 116  have hgamma_toRat : gamma.toRat = eps.toRat / 4 := by
 117    dsimp [gamma]
 118    rw [PRCRat.toRat_mul, PRCRat.toRat_recip, hfour]
 119    ring
 120  have hgamma_pos_rat : 0 < gamma.toRat := by
 121    rw [hgamma_toRat]
 122    positivity
 123  have hgamma_pos : PRCRat.positive gamma := by
 124    rw [PRCRat.positive_iff_toRat_pos]
 125    exact hgamma_pos_rat
 126  have heta_toRat : eta.toRat = gamma.toRat * gamma.toRat := by
 127    simp [eta, PRCRat.toRat_mul]
 128  have heta_pos_rat : 0 < eta.toRat := by
 129    rw [heta_toRat]
 130    nlinarith
 131  have h_one_add_eta :
 132      (((1 : PRCRat) + eta).toRat) = 1 + eta.toRat := by
 133    change (PRCRat.add PRCRat.one eta).toRat = 1 + eta.toRat
 134    rw [PRCRat.toRat_add, PRCRat.one_toRat]
 135  have hdelta_toRat :
 136      delta.toRat =
 137        eta.toRat * eta.toRat / (4 * (1 + eta.toRat)) := by
 138    dsimp [delta]
 139    simp [PRCRat.toRat_mul, PRCRat.toRat_recip, PRCRat.toRat_add,
 140      PRCRat.one_toRat, hfour]
 141    have hden_pos : (0 : ℚ) < 4 * (1 + eta.toRat) := by positivity
 142    field_simp [ne_of_gt hden_pos]
 143  have hdelta_pos_rat : 0 < delta.toRat := by
 144    rw [hdelta_toRat]
 145    positivity
 146  have hdelta_pos : PRCRat.positive delta := by
 147    rw [PRCRat.positive_iff_toRat_pos]
 148    exact hdelta_pos_rat
 149  rcases huu delta hdelta_pos with ⟨Nu, hNu⟩
 150  rcases hvv delta hdelta_pos with ⟨Nv, hNv⟩
 151  rcases hle gamma hgamma_pos with ⟨Nle, hNle⟩
 152  refine ⟨max (max Nu Nv) Nle, ?_⟩
 153  intro n hn
 154  have hNu_n : Nu ≤ n :=
 155    le_trans (Nat.le_max_left Nu Nv)
 156      (le_trans (Nat.le_max_left (max Nu Nv) Nle) hn)
 157  have hNv_n : Nv ≤ n :=
 158    le_trans (Nat.le_max_right Nu Nv)
 159      (le_trans (Nat.le_max_left (max Nu Nv) Nle) hn)
 160  have hNle_n : Nle ≤ n :=
 161    le_trans (Nat.le_max_right (max Nu Nv) Nle) hn
 162  have hu_close := PRCJCostDistance_abs_diff_lt_of_lt_order_delta
 163    (a := u.term n) (b := u'.term n) (gamma := gamma) (delta := delta)
 164    hgamma_pos hdelta_pos (by simp [hdelta_toRat, heta_toRat])
 165    (hNu n hNu_n)
 166  have hv_close := PRCJCostDistance_abs_diff_lt_of_lt_order_delta
 167    (a := v.term n) (b := v'.term n) (gamma := gamma) (delta := delta)
 168    hgamma_pos hdelta_pos (by simp [hdelta_toRat, heta_toRat])
 169    (hNv n hNv_n)
 170  have hu'_lt : (u'.term n).toRat < (u.term n).toRat + gamma.toRat := by
 171    rcases hu_close with ⟨hlo, _hhi⟩
 172    nlinarith
 173  have hv_lt : (v.term n).toRat < (v'.term n).toRat + gamma.toRat := by
 174    rcases hv_close with ⟨hlo, _hhi⟩
 175    nlinarith
 176  have huv_lt : (u.term n).toRat < (v.term n).toRat + gamma.toRat := by
 177    have hle_n := hNle n hNle_n
 178    rw [PRCRat.lt_iff_toRat_lt] at hle_n
 179    simpa [PRCCauchySeq.raw, PRCRat.toRat_add] using hle_n
 180  rw [PRCRat.lt_iff_toRat_lt]
 181  simp [PRCCauchySeq.raw, PRCRat.toRat_add]
 182  have hthree_gamma_lt_eps : 3 * gamma.toRat < eps.toRat := by
 183    rw [hgamma_toRat]
 184    nlinarith
 185  nlinarith
 186
 187theorem PRCRealOrderCongruenceTarget_proved :
 188    PRCRealOrderCongruenceTarget := by
 189  intro u u' v v' huu hvv
 190  constructor
 191  · intro hle
 192    exact PRCRawEventuallyLe_of_null_equiv huu hvv hle
 193  · intro hle
 194    exact PRCRawEventuallyLe_of_null_equiv
 195      (PRCNullEquivalent.symm huu) (PRCNullEquivalent.symm hvv) hle
 196
 197structure PRCRealOrderCongruenceCertificate : Prop where
 198  order_congruence : PRCRealOrderCongruenceTarget
 199
 200theorem prc_real_order_congruence_certificate :
 201    PRCRealOrderCongruenceCertificate where
 202  order_congruence := PRCRealOrderCongruenceTarget_proved
 203
 204end PrimitiveRecognitionCalculus
 205end Foundation
 206end IndisputableMonolith
 207