IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealMulBoundedContinuity

   1/-
   2  PrimitiveRecognitionCalculus/RealMulBoundedContinuity.lean
   3
   4  Round-trip source:
   5    δ/PRC_Universal_Foundation_Execution_Plan_20260526.html
   6
   7  Spec anchor:
   8    Build Order step 10a: reduce multiplication on `PRCRealNullClosed` to
   9    boundedness and bounded product-continuity moduli.
  10
  11  The object-level carrier remains the PRC null quotient. Verifier rationals
  12  appear only in display lemmas for analytic moduli.
  13-/
  14
  15import Mathlib
  16import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealCompleteOrderedField
  17
  18namespace IndisputableMonolith
  19namespace Foundation
  20namespace PrimitiveRecognitionCalculus
  21
  22/-- Eventual PRC-native boundedness for a raw rational ledger. -/
  23def PRCRawEventuallyBounded (s : PRCRawRatLedger) : Prop :=
  24  ∃ B : PRCRat, PRCRat.positive B ∧
  25    ∃ N : Nat, ∀ n : Nat, N ≤ n →
  26      PRCRat.lt (-B) (s n) ∧ PRCRat.lt (s n) B
  27
  28/-- Exact boundedness target for Cauchy ledgers. -/
  29def PRCCauchySeqEventuallyBoundedTarget : Prop :=
  30  ∀ u : PRCCauchySeq, PRCRawEventuallyBounded u.raw
  31
  32/-- A rational lies inside the symmetric PRC interval `[-B,B]`. -/
  33def PRCRat.InBound (B x : PRCRat) : Prop :=
  34  PRCRat.lt (-B) x ∧ PRCRat.lt x B
  35
  36/-- Enlarging a symmetric PRC rational bound preserves membership in it. -/
  37theorem PRCRat.InBound_mono {B C x : PRCRat}
  38    (hCB : C.toRat ≤ B.toRat) (hx : PRCRat.InBound C x) :
  39    PRCRat.InBound B x := by
  40  rcases hx with ⟨hlo, hhi⟩
  41  constructor
  42  · rw [PRCRat.lt_iff_toRat_lt] at hlo ⊢
  43    have hnegB : (-B).toRat = -B.toRat := by simp
  44    have hnegC : (-C).toRat = -C.toRat := by simp
  45    rw [hnegC] at hlo
  46    rw [hnegB]
  47    nlinarith
  48  · rw [PRCRat.lt_iff_toRat_lt] at hhi ⊢
  49    exact lt_of_lt_of_le hhi hCB
  50
  51/-- Exact product-continuity modulus on bounded rational windows. This is the
  52local analytic input needed by Cauchy multiplication and multiplication
  53congruence. -/
  54def PRCJCostDistanceMulBoundedContinuityTarget : Prop :=
  55  ∀ eps B : PRCRat, PRCRat.positive eps → PRCRat.positive B →
  56    ∃ delta : PRCRat, PRCRat.positive delta ∧
  57      ∀ a a' b b' : PRCRat,
  58        PRCRat.InBound B a →
  59          PRCRat.InBound B a' →
  60            PRCRat.InBound B b →
  61              PRCRat.InBound B b' →
  62                PRCRat.lt (PRCJCostDistance a a') delta →
  63                  PRCRat.lt (PRCJCostDistance b b') delta →
  64                    PRCRat.lt (PRCJCostDistance (a * b) (a' * b')) eps
  65
  66/-- Conditional proof of product Cauchy closure from eventual boundedness and
  67bounded product-continuity. -/
  68theorem PRCRealMulClosureTarget_of_bounded_continuity
  69    (hbounded : PRCCauchySeqEventuallyBoundedTarget)
  70    (hmul_cont : PRCJCostDistanceMulBoundedContinuityTarget) :
  71    PRCRealMulClosureTarget := by
  72  intro u v eps heps
  73  rcases hbounded u with ⟨Bu, hBu_pos, NuB, hNuB⟩
  74  rcases hbounded v with ⟨Bv, hBv_pos, NvB, hNvB⟩
  75  let B : PRCRat := Bu + Bv + 1
  76  have hB_pos : PRCRat.positive B := by
  77    rw [PRCRat.positive_iff_toRat_pos]
  78    have hBu : (0 : ℚ) < Bu.toRat := (PRCRat.positive_iff_toRat_pos Bu).mp hBu_pos
  79    have hBv : (0 : ℚ) < Bv.toRat := (PRCRat.positive_iff_toRat_pos Bv).mp hBv_pos
  80    simp [B]
  81    nlinarith
  82  have hBu_le_B : Bu.toRat ≤ B.toRat := by
  83    have hBv : (0 : ℚ) < Bv.toRat := (PRCRat.positive_iff_toRat_pos Bv).mp hBv_pos
  84    simp [B]
  85    nlinarith
  86  have hBv_le_B : Bv.toRat ≤ B.toRat := by
  87    have hBu : (0 : ℚ) < Bu.toRat := (PRCRat.positive_iff_toRat_pos Bu).mp hBu_pos
  88    simp [B]
  89    nlinarith
  90  rcases hmul_cont eps B heps hB_pos with ⟨delta, hdelta_pos, hdelta⟩
  91  rcases u.cauchy delta hdelta_pos with ⟨NuC, hNuC⟩
  92  rcases v.cauchy delta hdelta_pos with ⟨NvC, hNvC⟩
  93  let N := max (max NuB NvB) (max NuC NvC)
  94  refine ⟨N, ?_⟩
  95  intro m n hm hn
  96  have hNuB_m : NuB ≤ m := le_trans (le_trans (Nat.le_max_left NuB NvB)
  97    (Nat.le_max_left (max NuB NvB) (max NuC NvC))) hm
  98  have hNuB_n : NuB ≤ n := le_trans (le_trans (Nat.le_max_left NuB NvB)
  99    (Nat.le_max_left (max NuB NvB) (max NuC NvC))) hn
 100  have hNvB_m : NvB ≤ m := le_trans (le_trans (Nat.le_max_right NuB NvB)
 101    (Nat.le_max_left (max NuB NvB) (max NuC NvC))) hm
 102  have hNvB_n : NvB ≤ n := le_trans (le_trans (Nat.le_max_right NuB NvB)
 103    (Nat.le_max_left (max NuB NvB) (max NuC NvC))) hn
 104  have hNuC_m : NuC ≤ m := le_trans (le_trans (Nat.le_max_left NuC NvC)
 105    (Nat.le_max_right (max NuB NvB) (max NuC NvC))) hm
 106  have hNuC_n : NuC ≤ n := le_trans (le_trans (Nat.le_max_left NuC NvC)
 107    (Nat.le_max_right (max NuB NvB) (max NuC NvC))) hn
 108  have hNvC_m : NvC ≤ m := le_trans (le_trans (Nat.le_max_right NuC NvC)
 109    (Nat.le_max_right (max NuB NvB) (max NuC NvC))) hm
 110  have hNvC_n : NvC ≤ n := le_trans (le_trans (Nat.le_max_right NuC NvC)
 111    (Nat.le_max_right (max NuB NvB) (max NuC NvC))) hn
 112  have hu_m_small : PRCRat.InBound B (u.term m) :=
 113    PRCRat.InBound_mono hBu_le_B (hNuB m hNuB_m)
 114  have hu_n_small : PRCRat.InBound B (u.term n) :=
 115    PRCRat.InBound_mono hBu_le_B (hNuB n hNuB_n)
 116  have hv_m_small : PRCRat.InBound B (v.term m) :=
 117    PRCRat.InBound_mono hBv_le_B (hNvB m hNvB_m)
 118  have hv_n_small : PRCRat.InBound B (v.term n) :=
 119    PRCRat.InBound_mono hBv_le_B (hNvB n hNvB_n)
 120  exact hdelta (u.term m) (u.term n) (v.term m) (v.term n)
 121    hu_m_small hu_n_small hv_m_small hv_n_small
 122    (hNuC m n hNuC_m hNuC_n)
 123    (hNvC m n hNvC_m hNvC_n)
 124
 125/-- Conditional proof of product congruence from eventual boundedness and
 126bounded product-continuity. -/
 127theorem PRCRealMulCongruenceTarget_of_bounded_continuity
 128    (hbounded : PRCCauchySeqEventuallyBoundedTarget)
 129    (hmul_cont : PRCJCostDistanceMulBoundedContinuityTarget) :
 130    PRCRealMulCongruenceTarget := by
 131  intro u u' v v' huu hvv eps heps
 132  rcases hbounded u with ⟨Bu, hBu_pos, NuB, hNuB⟩
 133  rcases hbounded u' with ⟨Bu', hBu'_pos, Nu'B, hNu'B⟩
 134  rcases hbounded v with ⟨Bv, hBv_pos, NvB, hNvB⟩
 135  rcases hbounded v' with ⟨Bv', hBv'_pos, Nv'B, hNv'B⟩
 136  let B : PRCRat := Bu + Bu' + Bv + Bv' + 1
 137  have hB_pos : PRCRat.positive B := by
 138    rw [PRCRat.positive_iff_toRat_pos]
 139    have hBu : (0 : ℚ) < Bu.toRat := (PRCRat.positive_iff_toRat_pos Bu).mp hBu_pos
 140    have hBu' : (0 : ℚ) < Bu'.toRat := (PRCRat.positive_iff_toRat_pos Bu').mp hBu'_pos
 141    have hBv : (0 : ℚ) < Bv.toRat := (PRCRat.positive_iff_toRat_pos Bv).mp hBv_pos
 142    have hBv' : (0 : ℚ) < Bv'.toRat := (PRCRat.positive_iff_toRat_pos Bv').mp hBv'_pos
 143    simp [B]
 144    nlinarith
 145  have hBu_le_B : Bu.toRat ≤ B.toRat := by
 146    have hBu' : (0 : ℚ) < Bu'.toRat := (PRCRat.positive_iff_toRat_pos Bu').mp hBu'_pos
 147    have hBv : (0 : ℚ) < Bv.toRat := (PRCRat.positive_iff_toRat_pos Bv).mp hBv_pos
 148    have hBv' : (0 : ℚ) < Bv'.toRat := (PRCRat.positive_iff_toRat_pos Bv').mp hBv'_pos
 149    simp [B]
 150    nlinarith
 151  have hBu'_le_B : Bu'.toRat ≤ B.toRat := by
 152    have hBu : (0 : ℚ) < Bu.toRat := (PRCRat.positive_iff_toRat_pos Bu).mp hBu_pos
 153    have hBv : (0 : ℚ) < Bv.toRat := (PRCRat.positive_iff_toRat_pos Bv).mp hBv_pos
 154    have hBv' : (0 : ℚ) < Bv'.toRat := (PRCRat.positive_iff_toRat_pos Bv').mp hBv'_pos
 155    simp [B]
 156    nlinarith
 157  have hBv_le_B : Bv.toRat ≤ B.toRat := by
 158    have hBu : (0 : ℚ) < Bu.toRat := (PRCRat.positive_iff_toRat_pos Bu).mp hBu_pos
 159    have hBu' : (0 : ℚ) < Bu'.toRat := (PRCRat.positive_iff_toRat_pos Bu').mp hBu'_pos
 160    have hBv' : (0 : ℚ) < Bv'.toRat := (PRCRat.positive_iff_toRat_pos Bv').mp hBv'_pos
 161    simp [B]
 162    nlinarith
 163  have hBv'_le_B : Bv'.toRat ≤ B.toRat := by
 164    have hBu : (0 : ℚ) < Bu.toRat := (PRCRat.positive_iff_toRat_pos Bu).mp hBu_pos
 165    have hBu' : (0 : ℚ) < Bu'.toRat := (PRCRat.positive_iff_toRat_pos Bu').mp hBu'_pos
 166    have hBv : (0 : ℚ) < Bv.toRat := (PRCRat.positive_iff_toRat_pos Bv).mp hBv_pos
 167    simp [B]
 168    nlinarith
 169  rcases hmul_cont eps B heps hB_pos with ⟨delta, hdelta_pos, hdelta⟩
 170  rcases huu delta hdelta_pos with ⟨NuC, hNuC⟩
 171  rcases hvv delta hdelta_pos with ⟨NvC, hNvC⟩
 172  let N := max (max (max NuB Nu'B) (max NvB Nv'B)) (max NuC NvC)
 173  refine ⟨N, ?_⟩
 174  intro n hn
 175  have hNuB_n : NuB ≤ n := le_trans
 176    (le_trans (Nat.le_max_left NuB Nu'B) (Nat.le_max_left (max NuB Nu'B) (max NvB Nv'B)))
 177    (le_trans (Nat.le_max_left (max (max NuB Nu'B) (max NvB Nv'B)) (max NuC NvC)) hn)
 178  have hNu'B_n : Nu'B ≤ n := le_trans
 179    (le_trans (Nat.le_max_right NuB Nu'B) (Nat.le_max_left (max NuB Nu'B) (max NvB Nv'B)))
 180    (le_trans (Nat.le_max_left (max (max NuB Nu'B) (max NvB Nv'B)) (max NuC NvC)) hn)
 181  have hNvB_n : NvB ≤ n := le_trans
 182    (le_trans (Nat.le_max_left NvB Nv'B) (Nat.le_max_right (max NuB Nu'B) (max NvB Nv'B)))
 183    (le_trans (Nat.le_max_left (max (max NuB Nu'B) (max NvB Nv'B)) (max NuC NvC)) hn)
 184  have hNv'B_n : Nv'B ≤ n := le_trans
 185    (le_trans (Nat.le_max_right NvB Nv'B) (Nat.le_max_right (max NuB Nu'B) (max NvB Nv'B)))
 186    (le_trans (Nat.le_max_left (max (max NuB Nu'B) (max NvB Nv'B)) (max NuC NvC)) hn)
 187  have hNuC_n : NuC ≤ n :=
 188    le_trans (Nat.le_max_left NuC NvC)
 189      (le_trans (Nat.le_max_right (max (max NuB Nu'B) (max NvB Nv'B)) (max NuC NvC)) hn)
 190  have hNvC_n : NvC ≤ n :=
 191    le_trans (Nat.le_max_right NuC NvC)
 192      (le_trans (Nat.le_max_right (max (max NuB Nu'B) (max NvB Nv'B)) (max NuC NvC)) hn)
 193  exact hdelta (u.term n) (u'.term n) (v.term n) (v'.term n)
 194    (PRCRat.InBound_mono hBu_le_B (hNuB n hNuB_n))
 195    (PRCRat.InBound_mono hBu'_le_B (hNu'B n hNu'B_n))
 196    (PRCRat.InBound_mono hBv_le_B (hNvB n hNvB_n))
 197    (PRCRat.InBound_mono hBv'_le_B (hNv'B n hNv'B_n))
 198    (hNuC n hNuC_n)
 199    (hNvC n hNvC_n)
 200
 201/-- Conditional certificate: the multiplication targets reduce to eventual
 202boundedness plus bounded product continuity. -/
 203structure PRCRealMulBoundedContinuityConditionalCertificate : Prop where
 204  boundedness_target :
 205    PRCCauchySeqEventuallyBoundedTarget = PRCCauchySeqEventuallyBoundedTarget
 206  product_continuity_target :
 207    PRCJCostDistanceMulBoundedContinuityTarget =
 208      PRCJCostDistanceMulBoundedContinuityTarget
 209  mul_closure_from_targets :
 210    PRCCauchySeqEventuallyBoundedTarget →
 211      PRCJCostDistanceMulBoundedContinuityTarget →
 212        PRCRealMulClosureTarget
 213  mul_congruence_from_targets :
 214    PRCCauchySeqEventuallyBoundedTarget →
 215      PRCJCostDistanceMulBoundedContinuityTarget →
 216        PRCRealMulCongruenceTarget
 217  mul_operation_from_targets :
 218    PRCCauchySeqEventuallyBoundedTarget →
 219      PRCJCostDistanceMulBoundedContinuityTarget →
 220        Nonempty (PRCRealNullClosed → PRCRealNullClosed → PRCRealNullClosed)
 221
 222theorem prc_real_mul_bounded_continuity_conditional_certificate :
 223    PRCRealMulBoundedContinuityConditionalCertificate where
 224  boundedness_target := rfl
 225  product_continuity_target := rfl
 226  mul_closure_from_targets := PRCRealMulClosureTarget_of_bounded_continuity
 227  mul_congruence_from_targets := PRCRealMulCongruenceTarget_of_bounded_continuity
 228  mul_operation_from_targets := by
 229    intro hbounded hcont
 230    exact ⟨PRCRealNullClosed.mulOf
 231      (PRCRealMulClosureTarget_of_bounded_continuity hbounded hcont)
 232      (PRCRealMulCongruenceTarget_of_bounded_continuity hbounded hcont)⟩
 233
 234end PrimitiveRecognitionCalculus
 235end Foundation
 236end IndisputableMonolith
 237