IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealBoundednessModulus

   1/-
   2  PrimitiveRecognitionCalculus/RealBoundednessModulus.lean
   3
   4  Round-trip source:
   5    δ/PRC_Universal_Foundation_Execution_Plan_20260526.html
   6
   7  Spec anchor:
   8    Build Order step 10b: prove every J-cost Cauchy ledger is eventually
   9    PRC-bounded.
  10
  11  The proof uses the verifier rational display only to extract the ordinary
  12  square bound from small J-cost distance. The eventual bound itself is stated
  13  on the PRC rational ledger.
  14-/
  15
  16import Mathlib
  17import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealMulBoundedContinuity
  18
  19namespace IndisputableMonolith
  20namespace Foundation
  21namespace PrimitiveRecognitionCalculus
  22
  23/-- A fixed PRC rational distance threshold small enough to force ordinary
  24increment square below one. -/
  25def PRCBoundednessDelta : PRCRat :=
  26  let two : PRCRat := (1 : PRCRat) + (1 : PRCRat)
  27  let four : PRCRat := two * two
  28  (1 : PRCRat) * ((four * two)⁻¹)
  29
  30theorem PRCBoundednessDelta_toRat :
  31    PRCBoundednessDelta.toRat = (1 / 8 : ℚ) := by
  32  unfold PRCBoundednessDelta
  33  simp [PRCRat.toRat_mul, PRCRat.toRat_recip]
  34  norm_num
  35
  36theorem PRCBoundednessDelta_positive :
  37    PRCRat.positive PRCBoundednessDelta := by
  38  rw [PRCRat.positive_iff_toRat_pos, PRCBoundednessDelta_toRat]
  39  norm_num
  40
  41/-- Small increment display at the fixed threshold forces ordinary square
  42increment below one. -/
  43theorem PRCJCostDistanceIncrementDisplay_sq_lt_one {t : ℚ}
  44    (hsmall : PRCJCostDistanceIncrementDisplay t < (1 / 8 : ℚ)) :
  45    t * t < 1 := by
  46  by_contra hnot
  47  have hge : (1 : ℚ) ≤ t * t := by
  48    have hsq_nonneg : (0 : ℚ) ≤ t * t := mul_self_nonneg t
  49    nlinarith
  50  rw [PRCJCostDistanceIncrementDisplay_formula] at hsmall
  51  let s : ℚ := t * t
  52  have hs_ge : (1 : ℚ) ≤ s := by simpa [s] using hge
  53  have hs_den_pos : (0 : ℚ) < 2 * (1 + s) := by nlinarith
  54  have hmono : (1 / 8 : ℚ) ≤ (s * s) / (2 * (1 + s)) := by
  55    field_simp [ne_of_gt hs_den_pos]
  56    nlinarith [mul_self_nonneg s]
  57  exact not_lt_of_ge hmono (by simpa [s] using hsmall)
  58
  59/-- Small PRC J-cost distance at the fixed threshold forces the ordinary
  60rational display increment to have square below one. -/
  61theorem PRCJCostDistance_sq_diff_lt_one_of_lt_boundedness_delta
  62    {a b : PRCRat}
  63    (hsmall : PRCRat.lt (PRCJCostDistance a b) PRCBoundednessDelta) :
  64    (a.toRat - b.toRat) * (a.toRat - b.toRat) < 1 := by
  65  rw [PRCRat.lt_iff_toRat_lt] at hsmall
  66  rw [PRCJCostDistance_toRat, PRCJCostDistanceRatDisplay_as_increment,
  67    PRCBoundednessDelta_toRat] at hsmall
  68  exact PRCJCostDistanceIncrementDisplay_sq_lt_one hsmall
  69
  70/-- A J-cost Cauchy ledger is eventually contained in a PRC symmetric rational
  71interval. -/
  72theorem PRCCauchySeqEventuallyBoundedTarget_proved :
  73    PRCCauchySeqEventuallyBoundedTarget := by
  74  intro u
  75  rcases u.cauchy PRCBoundednessDelta PRCBoundednessDelta_positive with
  76    ⟨N, hN⟩
  77  let anchor : PRCRat := u.term N
  78  let two : PRCRat := (1 : PRCRat) + (1 : PRCRat)
  79  let B : PRCRat := anchor * anchor + two
  80  have hB_pos : PRCRat.positive B := by
  81    rw [PRCRat.positive_iff_toRat_pos]
  82    have hsq : (0 : ℚ) ≤ anchor.toRat * anchor.toRat :=
  83      mul_self_nonneg anchor.toRat
  84    simp [B, two]
  85    nlinarith
  86  refine ⟨B, hB_pos, N, ?_⟩
  87  intro n hn
  88  have hdist : PRCRat.lt (PRCJCostDistance (u.term n) anchor) PRCBoundednessDelta := by
  89    simpa [anchor] using hN n N hn (Nat.le_refl N)
  90  have hsquare :
  91      ((u.term n).toRat - anchor.toRat) *
  92          ((u.term n).toRat - anchor.toRat) < 1 :=
  93    PRCJCostDistance_sq_diff_lt_one_of_lt_boundedness_delta hdist
  94  let x : ℚ := (u.term n).toRat
  95  let q : ℚ := anchor.toRat
  96  have hsquare_xq : (x - q) * (x - q) < 1 := by
  97    simpa [x, q] using hsquare
  98  have hdiff_lt_one : x - q < 1 := by
  99    nlinarith [mul_self_nonneg ((x - q) - 1)]
 100  have hdiff_gt_neg_one : -1 < x - q := by
 101    nlinarith [mul_self_nonneg ((x - q) + 1)]
 102  constructor
 103  · rw [PRCRat.lt_iff_toRat_lt]
 104    simp [B, two, anchor]
 105    nlinarith [mul_self_nonneg (2 * q + 1)]
 106  · rw [PRCRat.lt_iff_toRat_lt]
 107    simp [B, two, anchor]
 108    nlinarith [mul_self_nonneg (2 * q - 1)]
 109
 110/-- Step 10b closure certificate: eventual boundedness is proved, so the
 111remaining multiplication blocker is only bounded product-continuity. -/
 112structure PRCRealBoundednessModulusCertificate : Prop where
 113  boundedness_delta_positive : PRCRat.positive PRCBoundednessDelta
 114  distance_sq_bound :
 115    ∀ a b : PRCRat,
 116      PRCRat.lt (PRCJCostDistance a b) PRCBoundednessDelta →
 117        (a.toRat - b.toRat) * (a.toRat - b.toRat) < 1
 118  eventual_boundedness : PRCCauchySeqEventuallyBoundedTarget
 119  mul_closure_from_product_continuity :
 120    PRCJCostDistanceMulBoundedContinuityTarget → PRCRealMulClosureTarget
 121  mul_congruence_from_product_continuity :
 122    PRCJCostDistanceMulBoundedContinuityTarget → PRCRealMulCongruenceTarget
 123
 124theorem prc_real_boundedness_modulus_certificate :
 125    PRCRealBoundednessModulusCertificate where
 126  boundedness_delta_positive := PRCBoundednessDelta_positive
 127  distance_sq_bound := by
 128    intro a b h
 129    exact PRCJCostDistance_sq_diff_lt_one_of_lt_boundedness_delta h
 130  eventual_boundedness := PRCCauchySeqEventuallyBoundedTarget_proved
 131  mul_closure_from_product_continuity := by
 132    intro hcont
 133    exact PRCRealMulClosureTarget_of_bounded_continuity
 134      PRCCauchySeqEventuallyBoundedTarget_proved hcont
 135  mul_congruence_from_product_continuity := by
 136    intro hcont
 137    exact PRCRealMulCongruenceTarget_of_bounded_continuity
 138      PRCCauchySeqEventuallyBoundedTarget_proved hcont
 139
 140end PrimitiveRecognitionCalculus
 141end Foundation
 142end IndisputableMonolith
 143