IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCJCostDistanceIncrementTriangle

   1/-
   2  PrimitiveRecognitionCalculus/PRCJCostDistanceIncrementTriangle.lean
   3
   4  Round-trip source:
   5    δ/PRC_Universal_Foundation_Execution_Plan_20260526.html
   6
   7  Spec anchor:
   8    Build Order step 9c: prove the one-dimensional additive increment modulus
   9    for the displayed rational J-cost distance.
  10-/
  11
  12import Mathlib
  13import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCJCostDistanceVerifierTriangle
  14
  15namespace IndisputableMonolith
  16namespace Foundation
  17namespace PrimitiveRecognitionCalculus
  18
  19theorem PRCJCostDistanceIncrementDisplay_formula (t : ℚ) :
  20    PRCJCostDistanceIncrementDisplay t =
  21      ((t * t) * (t * t)) / (2 * (1 + t * t)) := by
  22  unfold PRCJCostDistanceIncrementDisplay PRCJCostDistanceRatDisplay
  23  have hg_pos : (0 : ℚ) < 1 + t * t := by
  24    nlinarith [mul_self_nonneg t]
  25  have hg_ne : (1 + t * t : ℚ) ≠ 0 := ne_of_gt hg_pos
  26  field_simp [hg_ne]
  27  ring
  28
  29private theorem increment_display_lt_of_sq_lt
  30    {t eta eps : ℚ} (heta_pos : 0 < eta) (heta_lt_one : eta < 1)
  31    (hsq : t * t < eta) (heta_sq_half_lt_eps : eta * eta / 2 < eps) :
  32    PRCJCostDistanceIncrementDisplay t < eps := by
  33  rw [PRCJCostDistanceIncrementDisplay_formula]
  34  have hs_nonneg : (0 : ℚ) ≤ t * t := mul_self_nonneg t
  35  have hden_pos : (0 : ℚ) < 2 * (1 + t * t) := by positivity
  36  have hden_ne : (2 * (1 + t * t) : ℚ) ≠ 0 := ne_of_gt hden_pos
  37  have hs_lt_one : t * t < 1 := lt_trans hsq heta_lt_one
  38  have hnum_lt : (t * t) * (t * t) < eta * eta := by nlinarith
  39  have hfrac_le : ((t * t) * (t * t)) / (2 * (1 + t * t)) ≤
  40      ((t * t) * (t * t)) / 2 := by
  41    have hden_ge_two : (2 : ℚ) ≤ 2 * (1 + t * t) := by nlinarith
  42    have hnum_nonneg : (0 : ℚ) ≤ (t * t) * (t * t) :=
  43      mul_nonneg hs_nonneg hs_nonneg
  44    exact div_le_div_of_nonneg_left hnum_nonneg (by norm_num) hden_ge_two
  45  have hnum_half_lt : ((t * t) * (t * t)) / 2 < eta * eta / 2 := by
  46    nlinarith
  47  exact lt_of_le_of_lt hfrac_le (lt_trans hnum_half_lt heta_sq_half_lt_eps)
  48
  49private theorem sq_lt_of_display_lt_delta
  50    {t eta delta : ℚ} (heta_pos : 0 < eta) (_hdelta_pos : 0 < delta)
  51    (hdelta_le : delta ≤ eta * eta / (4 * (1 + eta)))
  52    (hsmall : PRCJCostDistanceIncrementDisplay t < delta) :
  53    t * t < eta := by
  54  by_contra hnot
  55  have hge : eta ≤ t * t := by nlinarith
  56  rw [PRCJCostDistanceIncrementDisplay_formula] at hsmall
  57  have hs_nonneg : (0 : ℚ) ≤ t * t := mul_self_nonneg t
  58  have hs_pos : (0 : ℚ) < t * t := lt_of_lt_of_le heta_pos hge
  59  have hden_s_pos : (0 : ℚ) < 2 * (1 + t * t) := by positivity
  60  have hden_eta_pos : (0 : ℚ) < 4 * (1 + eta) := by positivity
  61  have hmono :
  62      eta * eta / (4 * (1 + eta)) ≤
  63        ((t * t) * (t * t)) / (2 * (1 + t * t)) := by
  64    let s : ℚ := t * t
  65    have hs_ge : eta ≤ s := by simpa [s] using hge
  66    have hs_nonneg' : (0 : ℚ) ≤ s := by simpa [s] using hs_nonneg
  67    have hs_den_pos : (0 : ℚ) < 2 * (1 + s) := by positivity
  68    have h_eta_den_two_pos : (0 : ℚ) < 2 * (1 + eta) := by positivity
  69    have h_eta_den_four_pos : (0 : ℚ) < 4 * (1 + eta) := by positivity
  70    have hhalf :
  71        eta * eta / (4 * (1 + eta)) ≤
  72          eta * eta / (2 * (1 + eta)) := by
  73      have hnum_nonneg : (0 : ℚ) ≤ eta * eta := by nlinarith
  74      have hden_le : 2 * (1 + eta) ≤ 4 * (1 + eta) := by nlinarith
  75      exact div_le_div_of_nonneg_left hnum_nonneg h_eta_den_two_pos hden_le
  76    have hmon :
  77        eta * eta / (2 * (1 + eta)) ≤
  78          (s * s) / (2 * (1 + s)) := by
  79      have hdiff_nonneg :
  80          0 ≤ s * s * (1 + eta) - eta * eta * (1 + s) := by
  81        have hleft : 0 ≤ s - eta := by nlinarith
  82        have heta_nonneg : 0 ≤ eta := le_of_lt heta_pos
  83        have hright : 0 ≤ s + eta + s * eta := by
  84          nlinarith [mul_nonneg hs_nonneg' heta_nonneg]
  85        have hprod : 0 ≤ (s - eta) * (s + eta + s * eta) :=
  86          mul_nonneg hleft hright
  87        nlinarith
  88      field_simp [ne_of_gt hs_den_pos, ne_of_gt h_eta_den_two_pos]
  89      nlinarith [hdiff_nonneg]
  90    exact le_trans hhalf (by simpa [s] using hmon)
  91  exact not_lt_of_ge (le_trans hdelta_le hmono) hsmall
  92
  93theorem PRCJCostDistanceIncrementTriangleTarget_proved :
  94    PRCJCostDistanceIncrementTriangleTarget := by
  95  intro eps heps
  96  let two : PRCRat := (1 : PRCRat) + (1 : PRCRat)
  97  let four : PRCRat := two + two
  98  let rho : PRCRat := eps / (1 + eps)
  99  let eta : PRCRat := rho / four
 100  let delta : PRCRat := (eta * eta) / (four * (1 + eta))
 101  refine ⟨delta, ?_, ?_⟩
 102  · rw [PRCRat.positive_iff_toRat_pos]
 103    have heps_pos : (0 : ℚ) < eps.toRat := (PRCRat.positive_iff_toRat_pos eps).mp heps
 104    have htwo : two.toRat = (2 : ℚ) := by
 105      dsimp [two]
 106      change (PRCRat.add PRCRat.one PRCRat.one).toRat = (2 : ℚ)
 107      rw [PRCRat.toRat_add]
 108      norm_num [PRCRat.one_toRat]
 109    have hfour : four.toRat = (4 : ℚ) := by
 110      dsimp [four]
 111      change (PRCRat.add two two).toRat = (4 : ℚ)
 112      rw [PRCRat.toRat_add]
 113      norm_num [htwo]
 114    have h_one_add_eps : ((1 : PRCRat) + eps).toRat = 1 + eps.toRat := by
 115      change (PRCRat.add PRCRat.one eps).toRat = 1 + eps.toRat
 116      rw [PRCRat.toRat_add, PRCRat.one_toRat]
 117    have h_one_add_eta : ((1 : PRCRat) + eta).toRat = 1 + eta.toRat := by
 118      change (PRCRat.add PRCRat.one eta).toRat = 1 + eta.toRat
 119      rw [PRCRat.toRat_add, PRCRat.one_toRat]
 120    have heta_pos : (0 : ℚ) < eta.toRat := by
 121      rw [PRCRat.toRat_div, hfour]
 122      have hrho_pos : (0 : ℚ) < rho.toRat := by
 123        rw [PRCRat.toRat_div, h_one_add_eps]
 124        positivity
 125      positivity
 126    rw [PRCRat.toRat_div, PRCRat.toRat_mul', PRCRat.toRat_mul',
 127      h_one_add_eta, hfour]
 128    positivity
 129  · intro p q hp hq
 130    have heps_pos : (0 : ℚ) < eps.toRat := (PRCRat.positive_iff_toRat_pos eps).mp heps
 131    have htwo : two.toRat = (2 : ℚ) := by
 132      dsimp [two]
 133      change (PRCRat.add PRCRat.one PRCRat.one).toRat = (2 : ℚ)
 134      rw [PRCRat.toRat_add]
 135      norm_num [PRCRat.one_toRat]
 136    have hfour : four.toRat = (4 : ℚ) := by
 137      dsimp [four]
 138      change (PRCRat.add two two).toRat = (4 : ℚ)
 139      rw [PRCRat.toRat_add]
 140      norm_num [htwo]
 141    have h_one_add_eps : ((1 : PRCRat) + eps).toRat = 1 + eps.toRat := by
 142      change (PRCRat.add PRCRat.one eps).toRat = 1 + eps.toRat
 143      rw [PRCRat.toRat_add, PRCRat.one_toRat]
 144    have h_one_add_eta : ((1 : PRCRat) + eta).toRat = 1 + eta.toRat := by
 145      change (PRCRat.add PRCRat.one eta).toRat = 1 + eta.toRat
 146      rw [PRCRat.toRat_add, PRCRat.one_toRat]
 147    have hrho : rho.toRat = eps.toRat / (1 + eps.toRat) := by
 148      rw [PRCRat.toRat_div, h_one_add_eps]
 149    have hrho_pos : (0 : ℚ) < rho.toRat := by
 150      rw [hrho]
 151      positivity
 152    have hrho_lt_one : rho.toRat < 1 := by
 153      rw [hrho]
 154      field_simp [ne_of_gt (by positivity : (0 : ℚ) < 1 + eps.toRat)]
 155      nlinarith
 156    have heta : eta.toRat = rho.toRat / 4 := by
 157      rw [PRCRat.toRat_div, hfour]
 158    have heta_pos : (0 : ℚ) < eta.toRat := by
 159      rw [heta]
 160      positivity
 161    have heta_lt_one : eta.toRat < 1 := by
 162      rw [heta]
 163      nlinarith
 164    have hdelta :
 165        delta.toRat = eta.toRat * eta.toRat / (4 * (1 + eta.toRat)) := by
 166      rw [PRCRat.toRat_div, PRCRat.toRat_mul', PRCRat.toRat_mul',
 167        h_one_add_eta, hfour]
 168    have hdelta_pos : (0 : ℚ) < delta.toRat := by
 169      rw [hdelta]
 170      positivity
 171    have hp_sq : p * p < eta.toRat := by
 172      exact sq_lt_of_display_lt_delta
 173        (t := p) (eta := eta.toRat) (delta := delta.toRat)
 174        heta_pos hdelta_pos (by rw [hdelta]) hp
 175    have hq_sq : q * q < eta.toRat := by
 176      exact sq_lt_of_display_lt_delta
 177        (t := q) (eta := eta.toRat) (delta := delta.toRat)
 178        heta_pos hdelta_pos (by rw [hdelta]) hq
 179    have hpq_sq_lt_rho : (p + q) * (p + q) < rho.toRat := by
 180      have hsq_bound : (p + q) * (p + q) ≤ 2 * (p * p) + 2 * (q * q) := by
 181        nlinarith [mul_self_nonneg (p - q)]
 182      rw [heta] at hp_sq hq_sq
 183      nlinarith
 184    have hrho_sq_half_lt_eps : rho.toRat * rho.toRat / 2 < eps.toRat := by
 185      have hrho_lt_eps : rho.toRat < eps.toRat := by
 186        rw [hrho]
 187        field_simp [ne_of_gt (by positivity : (0 : ℚ) < 1 + eps.toRat)]
 188        nlinarith
 189      nlinarith [hrho_pos, hrho_lt_one, hrho_lt_eps]
 190    exact increment_display_lt_of_sq_lt
 191      (t := p + q) (eta := rho.toRat) (eps := eps.toRat)
 192      hrho_pos hrho_lt_one hpq_sq_lt_rho hrho_sq_half_lt_eps
 193
 194/-- Final closure for the rational increment modulus. -/
 195theorem PRCJCostDistanceVerifierTriangleTarget_proved :
 196    PRCJCostDistanceVerifierTriangleTarget :=
 197  PRCJCostDistanceVerifierTriangleTarget_of_increment
 198    PRCJCostDistanceIncrementTriangleTarget_proved
 199
 200/-- The PRC null-distance setoid target is now closed by the explicit rational
 201increment modulus. -/
 202theorem PRCNullDistanceSetoidTarget_proved :
 203    PRCNullDistanceSetoidTarget :=
 204  PRCNullDistanceSetoidTarget_of_increment_triangle
 205    PRCJCostDistanceIncrementTriangleTarget_proved
 206
 207/-- The PRC triangle modulus is now closed by the explicit rational increment
 208estimate. -/
 209theorem PRCJCostDistanceTriangleModulusTarget_proved :
 210    PRCJCostDistanceTriangleModulusTarget :=
 211  PRCJCostDistanceTriangleModulusTarget_of_verifier
 212    PRCJCostDistanceVerifierTriangleTarget_proved
 213
 214/-- The null-distance relation is transitive. -/
 215theorem PRCNullDistanceTransitiveTarget_proved :
 216    PRCNullDistanceTransitiveTarget :=
 217  PRCNullDistanceTransitiveTarget_of_triangle_modulus
 218    PRCJCostDistanceTriangleModulusTarget_proved
 219
 220/-- The final PRC real carrier: Cauchy ledgers quotiented by null distance. -/
 221def PRCRealNullClosed : Type :=
 222  PRCRealNull PRCNullDistanceTransitiveTarget_proved
 223
 224namespace PRCRealNullClosed
 225
 226/-- Embed a PRC rational into the closed null-distance quotient carrier. -/
 227def ofRat (q : PRCRat) : PRCRealNullClosed :=
 228  PRCRealNull.ofRat PRCNullDistanceTransitiveTarget_proved q
 229
 230end PRCRealNullClosed
 231
 232/-- Build Order step 9c closure certificate. -/
 233structure PRCJCostDistanceIncrementTriangleCertificate : Prop where
 234  increment_formula :
 235    ∀ t : ℚ,
 236      PRCJCostDistanceIncrementDisplay t =
 237        ((t * t) * (t * t)) / (2 * (1 + t * t))
 238  increment_triangle : PRCJCostDistanceIncrementTriangleTarget
 239  verifier_triangle : PRCJCostDistanceVerifierTriangleTarget
 240  triangle_modulus : PRCJCostDistanceTriangleModulusTarget
 241  null_distance_transitive : PRCNullDistanceTransitiveTarget
 242  null_distance_setoid : PRCNullDistanceSetoidTarget
 243  real_null_carrier : Nonempty PRCRealNullClosed
 244  rat_embedding : Nonempty (PRCRat → PRCRealNullClosed)
 245
 246/-- The explicit rational increment estimate closes the whole J-cost
 247null-distance setoid chain. -/
 248theorem prc_jcost_distance_increment_triangle_certificate :
 249    PRCJCostDistanceIncrementTriangleCertificate where
 250  increment_formula := PRCJCostDistanceIncrementDisplay_formula
 251  increment_triangle := PRCJCostDistanceIncrementTriangleTarget_proved
 252  verifier_triangle := PRCJCostDistanceVerifierTriangleTarget_proved
 253  triangle_modulus := PRCJCostDistanceTriangleModulusTarget_proved
 254  null_distance_transitive := PRCNullDistanceTransitiveTarget_proved
 255  null_distance_setoid := PRCNullDistanceSetoidTarget_proved
 256  real_null_carrier := ⟨PRCRealNullClosed.ofRat 0⟩
 257  rat_embedding := ⟨PRCRealNullClosed.ofRat⟩
 258
 259end PrimitiveRecognitionCalculus
 260end Foundation
 261end IndisputableMonolith
 262