IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealProductContinuity

   1/-
   2  PrimitiveRecognitionCalculus/RealProductContinuity.lean
   3
   4  Round-trip source:
   5    δ/PRC_Universal_Foundation_Execution_Plan_20260526.html
   6
   7  Spec anchor:
   8    Build Order step 10c: prove the bounded product-continuity modulus for
   9    `PRCJCostDistance`.
  10
  11  The object-level statement remains PRC-rational. The proof uses verifier
  12  rationals only as display transport for the analytic inequality.
  13-/
  14
  15import Mathlib
  16import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealBoundednessModulus
  17
  18namespace IndisputableMonolith
  19namespace Foundation
  20namespace PrimitiveRecognitionCalculus
  21
  22theorem PRCJCostDistanceIncrementDisplay_lt_of_sq_lt
  23    {t eta eps : ℚ} (heta_pos : 0 < eta) (heta_lt_one : eta < 1)
  24    (hsq : t * t < eta) (heta_sq_half_lt_eps : eta * eta / 2 < eps) :
  25    PRCJCostDistanceIncrementDisplay t < eps := by
  26  rw [PRCJCostDistanceIncrementDisplay_formula]
  27  have hs_nonneg : (0 : ℚ) ≤ t * t := mul_self_nonneg t
  28  have hden_pos : (0 : ℚ) < 2 * (1 + t * t) := by positivity
  29  have hs_lt_one : t * t < 1 := lt_trans hsq heta_lt_one
  30  have hnum_lt : (t * t) * (t * t) < eta * eta := by nlinarith
  31  have hfrac_le : ((t * t) * (t * t)) / (2 * (1 + t * t)) ≤
  32      ((t * t) * (t * t)) / 2 := by
  33    have hden_ge_two : (2 : ℚ) ≤ 2 * (1 + t * t) := by nlinarith
  34    have hnum_nonneg : (0 : ℚ) ≤ (t * t) * (t * t) :=
  35      mul_nonneg hs_nonneg hs_nonneg
  36    exact div_le_div_of_nonneg_left hnum_nonneg (by norm_num) hden_ge_two
  37  have hnum_half_lt : ((t * t) * (t * t)) / 2 < eta * eta / 2 := by
  38    nlinarith
  39  exact lt_of_le_of_lt hfrac_le (lt_trans hnum_half_lt heta_sq_half_lt_eps)
  40
  41theorem PRCJCostDistance_sq_lt_of_display_lt_delta
  42    {t eta delta : ℚ} (heta_pos : 0 < eta) (_hdelta_pos : 0 < delta)
  43    (hdelta_le : delta ≤ eta * eta / (4 * (1 + eta)))
  44    (hsmall : PRCJCostDistanceIncrementDisplay t < delta) :
  45    t * t < eta := by
  46  by_contra hnot
  47  have hge : eta ≤ t * t := by nlinarith
  48  rw [PRCJCostDistanceIncrementDisplay_formula] at hsmall
  49  have hs_nonneg : (0 : ℚ) ≤ t * t := mul_self_nonneg t
  50  have hs_pos : (0 : ℚ) < t * t := lt_of_lt_of_le heta_pos hge
  51  have hden_s_pos : (0 : ℚ) < 2 * (1 + t * t) := by positivity
  52  have hmono :
  53      eta * eta / (4 * (1 + eta)) ≤
  54        ((t * t) * (t * t)) / (2 * (1 + t * t)) := by
  55    let s : ℚ := t * t
  56    have hs_ge : eta ≤ s := by simpa [s] using hge
  57    have hs_nonneg' : (0 : ℚ) ≤ s := by simpa [s] using hs_nonneg
  58    have hs_den_pos : (0 : ℚ) < 2 * (1 + s) := by positivity
  59    have h_eta_den_two_pos : (0 : ℚ) < 2 * (1 + eta) := by positivity
  60    have h_eta_den_four_pos : (0 : ℚ) < 4 * (1 + eta) := by positivity
  61    have hhalf :
  62        eta * eta / (4 * (1 + eta)) ≤
  63          eta * eta / (2 * (1 + eta)) := by
  64      have hnum_nonneg : (0 : ℚ) ≤ eta * eta := by nlinarith
  65      have hden_le : 2 * (1 + eta) ≤ 4 * (1 + eta) := by nlinarith
  66      exact div_le_div_of_nonneg_left hnum_nonneg h_eta_den_two_pos hden_le
  67    have hmon :
  68        eta * eta / (2 * (1 + eta)) ≤
  69          (s * s) / (2 * (1 + s)) := by
  70      have hdiff_nonneg :
  71          0 ≤ s * s * (1 + eta) - eta * eta * (1 + s) := by
  72        have hleft : 0 ≤ s - eta := by nlinarith
  73        have heta_nonneg : 0 ≤ eta := le_of_lt heta_pos
  74        have hright : 0 ≤ s + eta + s * eta := by
  75          nlinarith [mul_nonneg hs_nonneg' heta_nonneg]
  76        have hprod : 0 ≤ (s - eta) * (s + eta + s * eta) :=
  77          mul_nonneg hleft hright
  78        nlinarith
  79      field_simp [ne_of_gt hs_den_pos, ne_of_gt h_eta_den_two_pos]
  80      nlinarith [hdiff_nonneg]
  81    exact le_trans hhalf (by simpa [s] using hmon)
  82  exact not_lt_of_ge (le_trans hdelta_le hmono) hsmall
  83
  84theorem PRCRat.InBound_sq_lt {B x : PRCRat}
  85    (hB : PRCRat.positive B) (hx : PRCRat.InBound B x) :
  86    x.toRat * x.toRat < B.toRat * B.toRat := by
  87  rcases hx with ⟨hlo, hhi⟩
  88  rw [PRCRat.lt_iff_toRat_lt] at hlo hhi
  89  have hB_pos : (0 : ℚ) < B.toRat := (PRCRat.positive_iff_toRat_pos B).mp hB
  90  have hneg : (-B).toRat = -B.toRat := by simp
  91  rw [hneg] at hlo
  92  have hleft : 0 < B.toRat - x.toRat := by nlinarith
  93  have hright : 0 < B.toRat + x.toRat := by nlinarith
  94  have hprod : 0 < (B.toRat - x.toRat) * (B.toRat + x.toRat) :=
  95    mul_pos hleft hright
  96  nlinarith
  97
  98private theorem product_factor_sq_lt
  99    {da b eta M : ℚ}
 100    (hda : da * da < eta)
 101    (hb : b * b < M * M)
 102    (hM_pos : 0 < M) :
 103    (da * b) * (da * b) < eta * (M * M) := by
 104  have hda_nonneg : 0 ≤ da * da := mul_self_nonneg da
 105  have hb_nonneg : 0 ≤ b * b := mul_self_nonneg b
 106  have hM_sq_pos : 0 < M * M := mul_pos hM_pos hM_pos
 107  have hgap1 : 0 < eta - da * da := by nlinarith
 108  have hgap2 : 0 < M * M - b * b := by nlinarith
 109  have hterm1 : 0 < (eta - da * da) * (M * M) :=
 110    mul_pos hgap1 hM_sq_pos
 111  have hterm2 : 0 ≤ (da * da) * (M * M - b * b) :=
 112    mul_nonneg hda_nonneg (le_of_lt hgap2)
 113  have hgap :
 114      0 < eta * (M * M) - (da * da) * (b * b) := by
 115    nlinarith
 116  have hsq : (da * b) * (da * b) = (da * da) * (b * b) := by ring
 117  rw [hsq]
 118  nlinarith
 119
 120private theorem rational_product_increment_sq_lt
 121    {a a' b b' M eta rho : ℚ}
 122    (hM_pos : 0 < M) (hrho_pos : 0 < rho)
 123    (heta_eq : eta = rho / (4 * (1 + M * M)))
 124    (ha' : a' * a' < M * M)
 125    (hb : b * b < M * M)
 126    (hda : (a - a') * (a - a') < eta)
 127    (hdb : (b - b') * (b - b') < eta) :
 128    (a * b - a' * b') * (a * b - a' * b') < rho := by
 129  let u : ℚ := (a - a') * b
 130  let v : ℚ := a' * (b - b')
 131  have hu : u * u < eta * (M * M) := by
 132    simpa [u] using product_factor_sq_lt
 133      (da := a - a') (b := b) (eta := eta) (M := M)
 134      hda hb hM_pos
 135  have hv : v * v < eta * (M * M) := by
 136    simpa [v, mul_comm, mul_left_comm, mul_assoc] using product_factor_sq_lt
 137      (da := b - b') (b := a') (eta := eta) (M := M)
 138      hdb ha' hM_pos
 139  have hsum_le : (u + v) * (u + v) ≤ 2 * (u * u) + 2 * (v * v) := by
 140    nlinarith [mul_self_nonneg (u - v)]
 141  have hsum_lt : (u + v) * (u + v) < 4 * eta * (M * M) := by
 142    nlinarith
 143  have hscale : 4 * eta * (M * M) < rho := by
 144    rw [heta_eq]
 145    have hden_pos : (0 : ℚ) < 4 * (1 + M * M) := by positivity
 146    field_simp [ne_of_gt hden_pos]
 147    have hM_sq_pos : 0 < M * M := mul_pos hM_pos hM_pos
 148    nlinarith
 149  have hidentity : a * b - a' * b' = u + v := by
 150    dsimp [u, v]
 151    ring
 152  rw [hidentity]
 153  exact lt_trans hsum_lt hscale
 154
 155theorem PRCJCostDistanceMulBoundedContinuityTarget_proved :
 156    PRCJCostDistanceMulBoundedContinuityTarget := by
 157  intro eps B heps hB
 158  let two : PRCRat := (1 : PRCRat) + (1 : PRCRat)
 159  let four : PRCRat := two * two
 160  let rho : PRCRat := eps * (((1 : PRCRat) + eps)⁻¹)
 161  let K : PRCRat := (1 : PRCRat) + (B * B)
 162  let eta : PRCRat := rho * ((four * K)⁻¹)
 163  let delta : PRCRat := (eta * eta) * ((four * ((1 : PRCRat) + eta))⁻¹)
 164  have heps_pos : (0 : ℚ) < eps.toRat :=
 165    (PRCRat.positive_iff_toRat_pos eps).mp heps
 166  have hB_pos : (0 : ℚ) < B.toRat :=
 167    (PRCRat.positive_iff_toRat_pos B).mp hB
 168  have htwo : two.toRat = (2 : ℚ) := by
 169    dsimp [two]
 170    change (PRCRat.add PRCRat.one PRCRat.one).toRat = (2 : ℚ)
 171    rw [PRCRat.toRat_add]
 172    norm_num [PRCRat.one_toRat]
 173  have hfour : four.toRat = (4 : ℚ) := by
 174    dsimp [four]
 175    change (PRCRat.mul two two).toRat = (4 : ℚ)
 176    rw [PRCRat.toRat_mul]
 177    norm_num [htwo]
 178  have h_one_add_eps :
 179      (((1 : PRCRat) + eps).toRat) = 1 + eps.toRat := by
 180    change (PRCRat.add PRCRat.one eps).toRat = 1 + eps.toRat
 181    rw [PRCRat.toRat_add, PRCRat.one_toRat]
 182  have hK : K.toRat = 1 + B.toRat * B.toRat := by
 183    dsimp [K]
 184    change (PRCRat.add PRCRat.one (PRCRat.mul B B)).toRat =
 185      1 + B.toRat * B.toRat
 186    rw [PRCRat.toRat_add, PRCRat.one_toRat, PRCRat.toRat_mul]
 187  have hK_pos : (0 : ℚ) < K.toRat := by
 188    rw [hK]
 189    nlinarith [mul_self_nonneg B.toRat]
 190  have hrho : rho.toRat = eps.toRat / (1 + eps.toRat) := by
 191    dsimp [rho]
 192    simp [PRCRat.toRat_mul, PRCRat.toRat_recip, PRCRat.toRat_add,
 193      PRCRat.one_toRat]
 194    ring
 195  have hrho_pos : (0 : ℚ) < rho.toRat := by
 196    rw [hrho]
 197    positivity
 198  have hrho_lt_one : rho.toRat < 1 := by
 199    rw [hrho]
 200    field_simp [ne_of_gt (by positivity : (0 : ℚ) < 1 + eps.toRat)]
 201    nlinarith
 202  have hrho_sq_half_lt_eps : rho.toRat * rho.toRat / 2 < eps.toRat := by
 203    have hrho_lt_eps : rho.toRat < eps.toRat := by
 204      rw [hrho]
 205      field_simp [ne_of_gt (by positivity : (0 : ℚ) < 1 + eps.toRat)]
 206      nlinarith
 207    nlinarith [hrho_pos, hrho_lt_one, hrho_lt_eps]
 208  have heta : eta.toRat = rho.toRat / (4 * K.toRat) := by
 209    dsimp [eta]
 210    rw [PRCRat.toRat_mul, PRCRat.toRat_recip, PRCRat.toRat_mul, hfour]
 211    ring
 212  have heta_pos : (0 : ℚ) < eta.toRat := by
 213    rw [heta]
 214    positivity
 215  have heta_lt_one : eta.toRat < 1 := by
 216    rw [heta]
 217    have hden_pos : (0 : ℚ) < 4 * K.toRat := by positivity
 218    field_simp [ne_of_gt hden_pos]
 219    have hK_gt_zero : 0 < 4 * K.toRat := by positivity
 220    nlinarith [hrho_lt_one, hrho_pos, hK_pos]
 221  have h_one_add_eta :
 222      (((1 : PRCRat) + eta).toRat) = 1 + eta.toRat := by
 223    change (PRCRat.add PRCRat.one eta).toRat = 1 + eta.toRat
 224    rw [PRCRat.toRat_add, PRCRat.one_toRat]
 225  have hdelta :
 226      delta.toRat = eta.toRat * eta.toRat / (4 * (1 + eta.toRat)) := by
 227    dsimp [delta]
 228    simp [PRCRat.toRat_mul, PRCRat.toRat_recip, PRCRat.toRat_add,
 229      PRCRat.one_toRat, hfour]
 230    have hden_pos : (0 : ℚ) < 4 * (1 + eta.toRat) := by positivity
 231    field_simp [ne_of_gt hden_pos]
 232  have hdelta_pos_rat : (0 : ℚ) < delta.toRat := by
 233    rw [hdelta]
 234    positivity
 235  have hdelta_pos : PRCRat.positive delta := by
 236    rw [PRCRat.positive_iff_toRat_pos]
 237    exact hdelta_pos_rat
 238  refine ⟨delta, hdelta_pos, ?_⟩
 239  intro a a' b b' ha ha' hb hb' haa hbb
 240  have ha'_sq : a'.toRat * a'.toRat < B.toRat * B.toRat :=
 241    PRCRat.InBound_sq_lt hB ha'
 242  have hb_sq : b.toRat * b.toRat < B.toRat * B.toRat :=
 243    PRCRat.InBound_sq_lt hB hb
 244  have haa_rat : PRCJCostDistanceIncrementDisplay (a.toRat - a'.toRat) < delta.toRat := by
 245    rw [PRCRat.lt_iff_toRat_lt] at haa
 246    rw [PRCJCostDistance_toRat, PRCJCostDistanceRatDisplay_as_increment] at haa
 247    exact haa
 248  have hbb_rat : PRCJCostDistanceIncrementDisplay (b.toRat - b'.toRat) < delta.toRat := by
 249    rw [PRCRat.lt_iff_toRat_lt] at hbb
 250    rw [PRCJCostDistance_toRat, PRCJCostDistanceRatDisplay_as_increment] at hbb
 251    exact hbb
 252  have hda_sq : (a.toRat - a'.toRat) * (a.toRat - a'.toRat) < eta.toRat :=
 253    PRCJCostDistance_sq_lt_of_display_lt_delta
 254      (t := a.toRat - a'.toRat) (eta := eta.toRat) (delta := delta.toRat)
 255      heta_pos hdelta_pos_rat (by rw [hdelta]) haa_rat
 256  have hdb_sq : (b.toRat - b'.toRat) * (b.toRat - b'.toRat) < eta.toRat :=
 257    PRCJCostDistance_sq_lt_of_display_lt_delta
 258      (t := b.toRat - b'.toRat) (eta := eta.toRat) (delta := delta.toRat)
 259      heta_pos hdelta_pos_rat (by rw [hdelta]) hbb_rat
 260  have hprod_sq :
 261      ((a * b).toRat - (a' * b').toRat) *
 262          ((a * b).toRat - (a' * b').toRat) < rho.toRat := by
 263    simp [PRCRat.toRat_mul]
 264    exact rational_product_increment_sq_lt
 265      (a := a.toRat) (a' := a'.toRat) (b := b.toRat) (b' := b'.toRat)
 266      (M := B.toRat) (eta := eta.toRat) (rho := rho.toRat)
 267      hB_pos hrho_pos (by rw [heta, hK]) ha'_sq hb_sq hda_sq hdb_sq
 268  rw [PRCRat.lt_iff_toRat_lt]
 269  rw [PRCJCostDistance_toRat, PRCJCostDistanceRatDisplay_as_increment]
 270  exact PRCJCostDistanceIncrementDisplay_lt_of_sq_lt
 271    (t := (a * b).toRat - (a' * b').toRat)
 272    (eta := rho.toRat) (eps := eps.toRat)
 273    hrho_pos hrho_lt_one hprod_sq hrho_sq_half_lt_eps
 274
 275structure PRCRealProductContinuityCertificate : Prop where
 276  product_continuity : PRCJCostDistanceMulBoundedContinuityTarget
 277  mul_closure : PRCRealMulClosureTarget
 278  mul_congruence : PRCRealMulCongruenceTarget
 279  mul_operation :
 280    Nonempty (PRCRealNullClosed → PRCRealNullClosed → PRCRealNullClosed)
 281
 282theorem prc_real_product_continuity_certificate :
 283    PRCRealProductContinuityCertificate where
 284  product_continuity := PRCJCostDistanceMulBoundedContinuityTarget_proved
 285  mul_closure :=
 286    PRCRealMulClosureTarget_of_bounded_continuity
 287      PRCCauchySeqEventuallyBoundedTarget_proved
 288      PRCJCostDistanceMulBoundedContinuityTarget_proved
 289  mul_congruence :=
 290    PRCRealMulCongruenceTarget_of_bounded_continuity
 291      PRCCauchySeqEventuallyBoundedTarget_proved
 292      PRCJCostDistanceMulBoundedContinuityTarget_proved
 293  mul_operation := by
 294    exact ⟨PRCRealNullClosed.mulOf
 295      (PRCRealMulClosureTarget_of_bounded_continuity
 296        PRCCauchySeqEventuallyBoundedTarget_proved
 297        PRCJCostDistanceMulBoundedContinuityTarget_proved)
 298      (PRCRealMulCongruenceTarget_of_bounded_continuity
 299        PRCCauchySeqEventuallyBoundedTarget_proved
 300        PRCJCostDistanceMulBoundedContinuityTarget_proved)⟩
 301
 302end PrimitiveRecognitionCalculus
 303end Foundation
 304end IndisputableMonolith
 305