IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.EtaCompletionM0a

   1/-
   2  PrimitiveRecognitionCalculus/Grow/EtaCompletionM0a.lean
   3
   4  M0a: the constructive-real carrier ℝδ_pre as Bishop regular sequences over the
   5  δ-rationals, and the unit map η : ℚδ → ℝδ_pre.
   6
   7  A regular sequence is a rule `(a_n)` of δ-rationals with
   8  `|a_m - a_n| ≤ 1/(m+1) + 1/(n+1)`, expressed purely at the integer
   9  cross-multiplication level (no ℚ display), so the whole construction stays on
  10  the `{propext, Quot.sound}` axiom basis (audit tier FORCED). The equivalence
  11  `equiv s t` is "the pointwise difference converges to 0", again integer-level.
  12
  13  Provenance. The carrier (`crossDiff`, `RegularSeq`, `equiv`, `eta`,
  14  `eta_regular`, `equiv_refl`, `eta_respects_crossEq`) was first synthesized by the
  15  `delta_grow` autonomous loop (GLM-5.2 maker, lake + `#print axioms` judge) and
  16  accepted choice-free. This module promotes that artifact into the library and
  17  completes it: `equiv_symm` and `equiv_trans` (the choice-free triangle
  18  argument) make `equivSetoid` a genuine setoid; `RealDelta := Quot equivSetoid`
  19  is the M0a real line; `etaQ : PRCRat → RealDelta` is the unit descended
  20  through both quotients; and `etaQ_injective` (via the Archimedean step
  21  `crossEq_of_equiv_eta`) makes it an embedding. Verified 2026-07-02: every
  22  declaration here has axiom closure exactly `{propext, Quot.sound}`, i.e.
  23  audit tier FORCED, strictly below the NAMED(AC_ω) cost the north-star verdict
  24  budgeted for this rung. The AC_ω completeness rung (limit existence, the
  25  NAMED-tier claim) sits on top of this setoid and is tracked separately.
  26
  27  No project-local axioms. No sorry.
  28-/
  29
  30import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerRational
  31import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder
  32
  33namespace IndisputableMonolith.PRCGrow.EtaCompletionM0a
  34
  35open IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus
  36
  37/-- The cross-difference: the integer numerator of `a - b`,
  38i.e., `a.num * b.den - b.num * a.den`. This avoids the ℚ display entirely. -/
  39def crossDiff (a b : RatioOrbit) : ℤ :=
  40  a.num.toInt * (b.den.toNat : ℤ) - b.num.toInt * (a.den.toNat : ℤ)
  41
  42/-- A rational minus itself has zero cross-difference. -/
  43theorem crossDiff_self (a : RatioOrbit) : crossDiff a a = 0 := by
  44  unfold crossDiff
  45  omega
  46
  47/-- Cross-equal rationals have zero cross-difference. -/
  48theorem crossDiff_of_crossEq (a b : RatioOrbit) (h : RatioOrbit.crossEq a b) :
  49    crossDiff a b = 0 := by
  50  rw [RatioOrbit.crossEq_iff_toIntCross] at h
  51  unfold crossDiff
  52  omega
  53
  54/-- Antisymmetry of the cross-difference: `crossDiff b a = -crossDiff a b`. -/
  55theorem crossDiff_swap (a b : RatioOrbit) : crossDiff b a = -crossDiff a b := by
  56  unfold crossDiff
  57  ring
  58
  59/-- The three-point cross-difference identity, the algebraic backbone of the
  60triangle inequality. As rationals `(a-c) = (a-b) + (b-c)`; clearing the three
  61denominators gives this pure integer identity:
  62`crossDiff a c * den b = crossDiff a b * den c + crossDiff b c * den a`. -/
  63theorem crossDiff_triangle_id (a b c : RatioOrbit) :
  64    crossDiff a c * (b.den.toNat : ℤ) =
  65      crossDiff a b * (c.den.toNat : ℤ) + crossDiff b c * (a.den.toNat : ℤ) := by
  66  unfold crossDiff
  67  ring
  68
  69/-- A regular sequence of delta-rationals.
  70
  71A sequence `(a_n)` is regular when `|a_m - a_n| ≤ 1/(m+1) + 1/(n+1)` for all `m, n`.
  72Expressed via integer cross-multiplication (avoiding the ℚ display):
  73`|crossDiff(a_m, a_n)| * (m+1) * (n+1) ≤ (m+n+2) * den(a_m) * den(a_n)`. -/
  74structure RegularSeq where
  75  seq : ℕ → RatioOrbit
  76  regular : ∀ m n : ℕ,
  77    Int.natAbs (crossDiff (seq m) (seq n)) * (m + 1) * (n + 1) ≤
  78    (m + n + 2) * (seq m).den.toNat * (seq n).den.toNat
  79
  80/-- Working equality on regular sequences: their pointwise difference
  81converges to 0. For every tolerance `1/(k+1)`, eventually
  82`|s_n - t_n| ≤ 1/(k+1)`. -/
  83def equiv (s t : RegularSeq) : Prop :=
  84  ∀ k : ℕ, ∃ N : ℕ, ∀ n : ℕ, n ≥ N →
  85    Int.natAbs (crossDiff (s.seq n) (t.seq n)) * (k + 1) ≤
  86    (s.seq n).den.toNat * (t.seq n).den.toNat
  87
  88/-- Well-formedness of `eta`: the constant sequence satisfies regularity. -/
  89theorem eta_regular (q : RatioOrbit) (m n : ℕ) :
  90  Int.natAbs (crossDiff q q) * (m + 1) * (n + 1) ≤
  91  (m + n + 2) * q.den.toNat * q.den.toNat := by
  92  rw [crossDiff_self, Int.natAbs_zero, Nat.zero_mul, Nat.zero_mul]
  93  exact Nat.zero_le _
  94
  95/-- The unit map: embed a delta-rational as a constant regular sequence. -/
  96def eta (q : RatioOrbit) : RegularSeq :=
  97  ⟨fun _ => q, fun m n => eta_regular q m n⟩
  98
  99/-- The sequence of `eta q` is the constant sequence `q`. -/
 100theorem eta_seq (q : RatioOrbit) (n : ℕ) : (eta q).seq n = q := by
 101  rfl
 102
 103/-- `equiv` is reflexive: every regular sequence is equivalent to itself. -/
 104theorem equiv_refl (s : RegularSeq) : equiv s s := by
 105  intro k
 106  refine ⟨0, ?_⟩
 107  intro n _
 108  rw [crossDiff_self, Int.natAbs_zero, Nat.zero_mul]
 109  exact Nat.zero_le _
 110
 111/-- `equiv` is symmetric. The cross-difference only flips sign, so its absolute
 112value and the denominator product are unchanged. Choice-free. -/
 113theorem equiv_symm {s t : RegularSeq} (h : equiv s t) : equiv t s := by
 114  intro k
 115  obtain ⟨N, hN⟩ := h k
 116  refine ⟨N, ?_⟩
 117  intro n hn
 118  have hcd : crossDiff (t.seq n) (s.seq n) = -crossDiff (s.seq n) (t.seq n) :=
 119    crossDiff_swap (s.seq n) (t.seq n)
 120  rw [hcd, Int.natAbs_neg, Nat.mul_comm (t.seq n).den.toNat (s.seq n).den.toNat]
 121  exact hN n hn
 122
 123/-- `equiv` is transitive: the choice-free triangle argument at the integer
 124cross-multiplication level. From `|s_n - t_n| ≤ 1/(2k+2)` and
 125`|t_n - u_n| ≤ 1/(2k+2)` eventually, the three-point identity plus positivity of
 126the middle denominator give `|s_n - u_n| ≤ 1/(k+1)`, with no ℚ display (so the
 127proof stays on `{propext, Quot.sound}`). -/
 128theorem equiv_trans {s t u : RegularSeq}
 129    (hst : equiv s t) (htu : equiv t u) : equiv s u := by
 130  intro k
 131  obtain ⟨N₁, hN₁⟩ := hst (2 * k + 1)
 132  obtain ⟨N₂, hN₂⟩ := htu (2 * k + 1)
 133  refine ⟨max N₁ N₂, ?_⟩
 134  intro n hn
 135  have hn₁ : n ≥ N₁ := le_trans (Nat.le_max_left N₁ N₂) hn
 136  have hn₂ : n ≥ N₂ := le_trans (Nat.le_max_right N₁ N₂) hn
 137  -- The three participating rationals at index n.
 138  set A := s.seq n with hA
 139  set B := t.seq n with hB
 140  set C := u.seq n with hC
 141  -- Hypotheses at level 2k+1 (i.e. factor 2k+1+1), in Nat. `set` rewrote the
 142  -- goal but not the ∀-hypotheses, so re-fold `s.seq n → A` etc. by hand.
 143  have h1 : (crossDiff A B).natAbs * (2 * k + 1 + 1) ≤ A.den.toNat * B.den.toNat := by
 144    have h := hN₁ n hn₁; rw [← hA, ← hB] at h; exact h
 145  have h2 : (crossDiff B C).natAbs * (2 * k + 1 + 1) ≤ B.den.toNat * C.den.toNat := by
 146    have h := hN₂ n hn₂; rw [← hB, ← hC] at h; exact h
 147  -- Positive denominators.
 148  have hdBpos : 0 < B.den.toNat := Nat.pos_of_ne_zero B.den_toNat_ne_zero
 149  -- Triangle in Nat via the integer identity and `Int.natAbs_add_le`.
 150  have hid : crossDiff A C * (B.den.toNat : ℤ) =
 151      crossDiff A B * (C.den.toNat : ℤ) + crossDiff B C * (A.den.toNat : ℤ) :=
 152    crossDiff_triangle_id A B C
 153  have heq := congrArg Int.natAbs hid
 154  have hnatB : ((B.den.toNat : ℤ)).natAbs = B.den.toNat := Int.natAbs_natCast _
 155  have hnatC : ((C.den.toNat : ℤ)).natAbs = C.den.toNat := Int.natAbs_natCast _
 156  have hnatA : ((A.den.toNat : ℤ)).natAbs = A.den.toNat := Int.natAbs_natCast _
 157  have hL : (crossDiff A C * (B.den.toNat : ℤ)).natAbs
 158      = (crossDiff A C).natAbs * B.den.toNat := by
 159    rw [Int.natAbs_mul, hnatB]
 160  have hR : (crossDiff A B * (C.den.toNat : ℤ) + crossDiff B C * (A.den.toNat : ℤ)).natAbs
 161      ≤ (crossDiff A B).natAbs * C.den.toNat + (crossDiff B C).natAbs * A.den.toNat := by
 162    refine le_trans (Int.natAbs_add_le _ _) ?_
 163    rw [Int.natAbs_mul, Int.natAbs_mul, hnatC, hnatA]
 164  have htriN : (crossDiff A C).natAbs * B.den.toNat
 165      ≤ (crossDiff A B).natAbs * C.den.toNat + (crossDiff B C).natAbs * A.den.toNat := by
 166    rw [hL] at heq; rw [heq]; exact hR
 167  -- Do the ε/2 arithmetic entirely in ℕ, using only monotone product lemmas and
 168  -- `ring`/`omega` (all choice-free). Casting to ℤ via norm_cast smuggles
 169  -- `Classical.choice` here, so we stay in ℕ.
 170  set cAC := (crossDiff A C).natAbs with hcAC
 171  set cAB := (crossDiff A B).natAbs with hcAB
 172  set cBC := (crossDiff B C).natAbs with hcBC
 173  set dA := A.den.toNat with hdA
 174  set dB := B.den.toNat with hdB
 175  set dC := C.den.toNat with hdC
 176  set two := 2 * k + 1 + 1 with htwo_def
 177  -- htriN : cAC*dB ≤ cAB*dC + cBC*dA ;  h1 : cAB*two ≤ dA*dB ;  h2 : cBC*two ≤ dB*dC
 178  have e1 : cAB * two * dC ≤ dA * dB * dC := Nat.mul_le_mul_right dC h1
 179  have e2 : cBC * two * dA ≤ dB * dC * dA := Nat.mul_le_mul_right dA h2
 180  have base : cAC * dB * two ≤ (cAB * dC + cBC * dA) * two := Nat.mul_le_mul_right two htriN
 181  have expand : (cAB * dC + cBC * dA) * two = cAB * two * dC + cBC * two * dA := by ring
 182  have chain : cAC * dB * two ≤ dA * dB * dC + dB * dC * dA := by
 183    rw [expand] at base; exact le_trans base (add_le_add e1 e2)
 184  -- two = 2*(k+1); repackage both sides around the common positive factor 2*dB.
 185  have htwo : two = 2 * (k + 1) := by rw [htwo_def]; ring
 186  have lhs_eq : cAC * dB * two = cAC * (k + 1) * (2 * dB) := by rw [htwo]; ring
 187  have rhs_eq : dA * dB * dC + dB * dC * dA = dA * dC * (2 * dB) := by ring
 188  have cancel_in : cAC * (k + 1) * (2 * dB) ≤ dA * dC * (2 * dB) := by
 189    rw [← lhs_eq, ← rhs_eq]; exact chain
 190  have hpos : 0 < 2 * dB := by rw [hdB]; omega
 191  exact Nat.le_of_mul_le_mul_right cancel_in hpos
 192
 193/-- `eta` respects `crossEq`: if `q` and `r` are cross-equal (represent the same
 194delta-rational), then `eta q` and `eta r` are equivalent regular sequences.
 195This is the key well-definedness property of the unit map. -/
 196theorem eta_respects_crossEq (q r : RatioOrbit) (h : RatioOrbit.crossEq q r) :
 197  equiv (eta q) (eta r) := by
 198  intro k
 199  refine ⟨0, ?_⟩
 200  intro n _
 201  rw [eta_seq q n, eta_seq r n, crossDiff_of_crossEq q r h,
 202    Int.natAbs_zero, Nat.zero_mul]
 203  exact Nat.zero_le _
 204
 205/-- `equiv` is an equivalence relation: reflexive, symmetric, transitive. This is
 206the completion of the M0a carrier into a genuine setoid, all choice-free. -/
 207theorem equiv_equivalence : Equivalence equiv where
 208  refl := equiv_refl
 209  symm := equiv_symm
 210  trans := equiv_trans
 211
 212/-- The M0a real setoid: regular sequences of δ-rationals modulo pointwise
 213convergence to zero. The quotient `Quot equivSetoid` is the constructive real
 214line ℝδ_pre; `eta` descends to the rational embedding on it. -/
 215def equivSetoid : Setoid RegularSeq where
 216  r := equiv
 217  iseqv := equiv_equivalence
 218
 219/-- The M0a constructive real line ℝδ_pre: regular sequences of δ-rationals
 220modulo pointwise convergence to zero. Built with `Quot` only, so the carrier
 221sits on `{propext, Quot.sound}` (audit tier FORCED). -/
 222def RealDelta : Type :=
 223  Quot equivSetoid
 224
 225namespace RealDelta
 226
 227/-- Constructor from a regular-sequence display. -/
 228def mk (s : RegularSeq) : RealDelta :=
 229  Quot.mk equivSetoid s
 230
 231/-- Equivalent regular sequences determine equal constructive reals. -/
 232theorem mk_eq_mk_of_equiv {s t : RegularSeq} (h : equiv s t) : mk s = mk t :=
 233  Quot.sound h
 234
 235end RealDelta
 236
 237/-- The unit map η : ℚδ → ℝδ_pre, descended through both quotients: a PRC
 238rational (ratio orbit modulo cross-equality) maps to the class of its constant
 239regular sequence. Well-definedness is `eta_respects_crossEq`. This is the M0a
 240carrier morphism of the Forced ⊣ Classical adjunction program. -/
 241def etaQ : PRCRat → RealDelta :=
 242  Quot.lift (fun q => RealDelta.mk (eta q))
 243    (fun q r h => RealDelta.mk_eq_mk_of_equiv (eta_respects_crossEq q r h))
 244
 245/-- `etaQ` on a display rational is the class of the constant sequence. -/
 246@[simp] theorem etaQ_mk (q : RatioOrbit) :
 247    etaQ (PRCRat.mk q) = RealDelta.mk (eta q) := rfl
 248
 249/-- The Archimedean step: if the constant sequences at `q` and `r` are
 250equivalent (their fixed difference is below every `1/(k+1)`), then `q` and `r`
 251are cross-equal. Instantiate the tolerance at `k = den q * den r`; then
 252`c * (k+1) ≤ k` forces `c = 0`. Choice-free. -/
 253theorem crossEq_of_equiv_eta {q r : RatioOrbit}
 254    (h : equiv (eta q) (eta r)) : RatioOrbit.crossEq q r := by
 255  set k := q.den.toNat * r.den.toNat with hk
 256  obtain ⟨N, hN⟩ := h k
 257  have hbound := hN N (Nat.le_refl N)
 258  rw [eta_seq q N, eta_seq r N, ← hk] at hbound
 259  -- hbound : |crossDiff q r| * (k+1) ≤ k, so |crossDiff q r| = 0.
 260  have hzero : (crossDiff q r).natAbs = 0 := by
 261    by_contra hne
 262    have hone : 1 ≤ (crossDiff q r).natAbs := Nat.pos_of_ne_zero hne
 263    have : k + 1 ≤ (crossDiff q r).natAbs * (k + 1) := by
 264      calc k + 1 = 1 * (k + 1) := (Nat.one_mul _).symm
 265        _ ≤ (crossDiff q r).natAbs * (k + 1) := Nat.mul_le_mul_right (k + 1) hone
 266    exact absurd (le_trans this hbound) (by omega)
 267  have hcd : crossDiff q r = 0 := Int.natAbs_eq_zero.mp hzero
 268  rw [RatioOrbit.crossEq_iff_toIntCross]
 269  unfold crossDiff at hcd
 270  omega
 271
 272/-- The unit η : ℚδ → ℝδ_pre is injective: no two distinct δ-rationals collapse
 273in the completion. Together with well-definedness this makes η a genuine
 274embedding of the rational base into the M0a real line, choice-free. -/
 275theorem etaQ_injective : Function.Injective etaQ := by
 276  intro a b h
 277  induction a using Quot.ind with
 278  | mk q =>
 279    induction b using Quot.ind with
 280    | mk r =>
 281      have hq : RealDelta.mk (eta q) = RealDelta.mk (eta r) := h
 282      have hequiv : equiv (eta q) (eta r) := by
 283        have := Quot.eqvGen_exact hq
 284        -- Exactness gives `EqvGen`; collapse it with the proved equivalence.
 285        exact (Equivalence.eqvGen_iff equiv_equivalence).mp this
 286      exact Quot.sound (crossEq_of_equiv_eta hequiv)
 287
 288end IndisputableMonolith.PRCGrow.EtaCompletionM0a
 289