IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealCauchy

   1/-
   2  PrimitiveRecognitionCalculus/RealCauchy.lean
   3
   4  Round-trip source:
   5    δ/PRC_Universal_Foundation_Execution_Plan_20260526.html
   6
   7  Spec anchor:
   8    Build Order step 8: start the internal PRC real completion by forming
   9    Cauchy ledgers over `PRCRat`, a J-cost-derived closeness relation, and the
  10    first internal quotient carrier.
  11
  12  Strength: δ + trace-closure. The completed sequence index is the completed
  13  orbit ledger from `TraceClosure`; verifier rationals appear only in display
  14  theorems and proofs.
  15-/
  16
  17import Mathlib
  18import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RationalField
  19import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.TraceClosure
  20
  21namespace IndisputableMonolith
  22namespace Foundation
  23namespace PrimitiveRecognitionCalculus
  24
  25namespace PRCRat
  26
  27/-! ## Rational comparison surface used by Cauchy ledgers -/
  28
  29/-- PRC-native strict order on rationals: `a < b` means the positive gap
  30`b - a` has a positive ratio-orbit representative. -/
  31def lt (a b : PRCRat) : Prop :=
  32  positive (b - a)
  33
  34theorem lt_iff_toRat_lt (a b : PRCRat) :
  35    lt a b ↔ a.toRat < b.toRat := by
  36  unfold lt
  37  rw [positive_iff_toRat_pos]
  38  rw [PRCRat.sub_eq, PRCRat.toRat_sub]
  39  constructor
  40  · intro h
  41    linarith
  42  · intro h
  43    linarith
  44
  45theorem zero_lt_of_positive {q : PRCRat}
  46    (h : positive q) : lt 0 q := by
  47  rw [lt_iff_toRat_lt]
  48  simpa using (positive_iff_toRat_pos q).mp h
  49
  50end PRCRat
  51
  52/-! ## J-cost-derived distance on PRC rationals -/
  53
  54/-- A positive comparison gap for additive rational separation. The square
  55removes the need for a rational absolute value in this first Cauchy pass. -/
  56def PRCSquareGap (a b : PRCRat) : PRCRat :=
  57  1 + (a - b) * (a - b)
  58
  59theorem PRCSquareGap_toRat (a b : PRCRat) :
  60    (PRCSquareGap a b).toRat = 1 + (a.toRat - b.toRat) * (a.toRat - b.toRat) := by
  61  unfold PRCSquareGap
  62  rw [PRCRat.toRat_add', PRCRat.toRat_mul']
  63  simp [PRCRat.sub_eq]
  64
  65/-- J-cost distance used by the first PRC Cauchy surface. It sends additive
  66separation through the positive ratio `1 + (a-b)^2`, then applies the PRC
  67rational J-cost. -/
  68def PRCJCostDistance (a b : PRCRat) : PRCRat :=
  69  PRCJCost.onPRCRat (PRCSquareGap a b)
  70
  71theorem PRCJCostDistance_self_zero (a : PRCRat) :
  72    PRCJCostDistance a a = 0 := by
  73  apply PRCRat.toRat_injective
  74  unfold PRCJCostDistance
  75  rw [PRCJCost.onPRCRat_toRat, PRCSquareGap_toRat]
  76  simp
  77
  78theorem PRCJCostDistance_symmetric (a b : PRCRat) :
  79    PRCJCostDistance a b = PRCJCostDistance b a := by
  80  apply PRCRat.toRat_injective
  81  unfold PRCJCostDistance
  82  rw [PRCJCost.onPRCRat_toRat, PRCJCost.onPRCRat_toRat,
  83    PRCSquareGap_toRat, PRCSquareGap_toRat]
  84  ring
  85
  86/-! ## PRC Cauchy ledgers -/
  87
  88/-- A PRC Cauchy sequence is a completed orbit-indexed rational ledger whose
  89J-cost distance eventually falls below every positive PRC rational tolerance. -/
  90structure PRCCauchySeq where
  91  term : Nat → PRCRat
  92  cauchy :
  93    ∀ eps : PRCRat, PRCRat.positive eps →
  94      ∃ N : Nat, ∀ m n : Nat, N ≤ m → N ≤ n →
  95        PRCRat.lt (PRCJCostDistance (term m) (term n)) eps
  96
  97namespace PRCCauchySeq
  98
  99/-- Constant rational ledgers are Cauchy. -/
 100def constant (q : PRCRat) : PRCCauchySeq where
 101  term := fun _ => q
 102  cauchy := by
 103    intro eps heps
 104    refine ⟨0, ?_⟩
 105    intro m n _hm _hn
 106    rw [PRCJCostDistance_self_zero]
 107    exact PRCRat.zero_lt_of_positive heps
 108
 109@[simp] theorem constant_term (q : PRCRat) (n : Nat) :
 110    (constant q).term n = q := by
 111  rfl
 112
 113end PRCCauchySeq
 114
 115/-- The intended null-distance relation between two Cauchy ledgers. This is
 116the relation that should become the final real quotient once transitivity is
 117proved from the J-cost distance surface. -/
 118def PRCNullEquivalent (u v : PRCCauchySeq) : Prop :=
 119  ∀ eps : PRCRat, PRCRat.positive eps →
 120    ∃ N : Nat, ∀ n : Nat, N ≤ n →
 121      PRCRat.lt (PRCJCostDistance (u.term n) (v.term n)) eps
 122
 123theorem PRCNullEquivalent.refl (u : PRCCauchySeq) :
 124    PRCNullEquivalent u u := by
 125  intro eps heps
 126  refine ⟨0, ?_⟩
 127  intro n _hn
 128  rw [PRCJCostDistance_self_zero]
 129  exact PRCRat.zero_lt_of_positive heps
 130
 131theorem PRCNullEquivalent.symm {u v : PRCCauchySeq}
 132    (h : PRCNullEquivalent u v) : PRCNullEquivalent v u := by
 133  intro eps heps
 134  rcases h eps heps with ⟨N, hN⟩
 135  refine ⟨N, ?_⟩
 136  intro n hn
 137  rw [PRCJCostDistance_symmetric]
 138  exact hN n hn
 139
 140/-- Exact blocker for the final null-distance quotient: prove triangle-style
 141transitivity for the J-cost distance surface. -/
 142def PRCNullDistanceTransitiveTarget : Prop :=
 143  ∀ u v w : PRCCauchySeq,
 144    PRCNullEquivalent u v →
 145      PRCNullEquivalent v w →
 146        PRCNullEquivalent u w
 147
 148/-- Exact target that turns the intended null-distance relation into the real
 149setoid. Reflexivity and symmetry are proved above; transitivity is the live
 150mathematical obligation. -/
 151def PRCNullDistanceSetoidTarget : Prop :=
 152  Equivalence PRCNullEquivalent
 153
 154/-! ## First internal quotient carrier -/
 155
 156/-- Sequence identity, used only as the first quotient carrier while the
 157null-distance transitivity target remains open. -/
 158def PRCSameTerm (u v : PRCCauchySeq) : Prop :=
 159  ∀ n : Nat, u.term n = v.term n
 160
 161theorem PRCSameTerm.equivalence : Equivalence PRCSameTerm := by
 162  constructor
 163  · intro u n
 164    rfl
 165  · intro u v h n
 166    exact (h n).symm
 167  · intro u v w huv hvw n
 168    exact (huv n).trans (hvw n)
 169
 170/-- The first internal setoid available without the null-distance triangle
 171lemma. It is intentionally stronger than the final null-distance setoid. -/
 172def PRCSameTermSetoid : Setoid PRCCauchySeq where
 173  r := PRCSameTerm
 174  iseqv := PRCSameTerm.equivalence
 175
 176/-- First internal PRC real carrier. It is a Cauchy-ledger quotient, not Lean
 177`ℝ`; the final quotient relation is recorded as `PRCNullDistanceSetoidTarget`. -/
 178def PRCReal : Type :=
 179  Quot PRCSameTermSetoid
 180
 181namespace PRCReal
 182
 183/-- Embed a PRC rational as a constant Cauchy ledger. -/
 184def ofRat (q : PRCRat) : PRCReal :=
 185  Quot.mk PRCSameTermSetoid (PRCCauchySeq.constant q)
 186
 187end PRCReal
 188
 189/-- K1/R9. Audit record: internal Cauchy real ledgers require trace closure. -/
 190def realCauchyClaim : StrengthClaim where
 191  label := "BuildOrder8_real_cauchy_internal_quotient"
 192  tag := StrengthTag.traceClosure
 193  statement :=
 194    "PRC Cauchy ledgers and their first internal quotient use completed orbit indexing."
 195
 196/-- First-pass real Cauchy certificate. The carrier is internal and
 197trace-closure tagged. The final null-distance quotient is left as an exact
 198Lean target rather than hidden behind a classical real alias. -/
 199structure PRCRealCauchyCertificate : Prop where
 200  cauchy_sequences : Nonempty PRCCauchySeq
 201  constant_embedding_exists : Nonempty (PRCRat → PRCCauchySeq)
 202  jcost_distance_self_zero :
 203    ∀ q : PRCRat, PRCJCostDistance q q = 0
 204  null_relation_reflexive :
 205    ∀ u : PRCCauchySeq, PRCNullEquivalent u u
 206  null_relation_symmetric :
 207    ∀ u v : PRCCauchySeq, PRCNullEquivalent u v → PRCNullEquivalent v u
 208  same_term_setoid : Nonempty (Setoid PRCCauchySeq)
 209  real_quotient : Nonempty PRCReal
 210  rat_embedding : Nonempty (PRCRat → PRCReal)
 211  null_transitivity_target :
 212    PRCNullDistanceTransitiveTarget = PRCNullDistanceTransitiveTarget
 213  null_setoid_target :
 214    PRCNullDistanceSetoidTarget = PRCNullDistanceSetoidTarget
 215  strength_tag : realCauchyClaim.tag = StrengthTag.traceClosure
 216
 217/-- Build Order step 8, first pass: internal Cauchy ledgers and an internal
 218quotient carrier exist, with the exact null-distance setoid target named. -/
 219theorem real_cauchy_certificate : PRCRealCauchyCertificate where
 220  cauchy_sequences := ⟨PRCCauchySeq.constant 0⟩
 221  constant_embedding_exists := ⟨PRCCauchySeq.constant⟩
 222  jcost_distance_self_zero := PRCJCostDistance_self_zero
 223  null_relation_reflexive := PRCNullEquivalent.refl
 224  null_relation_symmetric := by
 225    intro u v h
 226    exact PRCNullEquivalent.symm h
 227  same_term_setoid := ⟨PRCSameTermSetoid⟩
 228  real_quotient := ⟨PRCReal.ofRat 0⟩
 229  rat_embedding := ⟨PRCReal.ofRat⟩
 230  null_transitivity_target := rfl
 231  null_setoid_target := rfl
 232  strength_tag := rfl
 233
 234end PrimitiveRecognitionCalculus
 235end Foundation
 236end IndisputableMonolith
 237