IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealCompleteOrderedField
IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealCompleteOrderedField.lean · 371 lines · 31 declarations
show as:
view math explainer →
1/-
2 PrimitiveRecognitionCalculus/RealCompleteOrderedField.lean
3
4 Round-trip source:
5 δ/PRC_Universal_Foundation_Execution_Plan_20260526.html
6
7 Spec anchor:
8 Build Order step 10: start the complete ordered field surface over the
9 closed null-distance quotient `PRCRealNullClosed`.
10
11 This pass does not alias the carrier to Lean `ℝ`. It exposes the exact
12 quotient-algebra blockers for addition, multiplication, negation, and order.
13-/
14
15import Mathlib
16import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCJCostDistanceIncrementTriangle
17
18namespace IndisputableMonolith
19namespace Foundation
20namespace PrimitiveRecognitionCalculus
21
22/-- Raw completed-orbit rational ledger, before a Cauchy proof is attached. -/
23abbrev PRCRawRatLedger := Nat → PRCRat
24
25/-- Cauchy predicate on raw ledgers, using the same J-cost distance as
26`PRCCauchySeq`. -/
27def PRCRawCauchy (s : PRCRawRatLedger) : Prop :=
28 ∀ eps : PRCRat, PRCRat.positive eps →
29 ∃ N : Nat, ∀ m n : Nat, N ≤ m → N ≤ n →
30 PRCRat.lt (PRCJCostDistance (s m) (s n)) eps
31
32/-- Null equivalence on raw ledgers. -/
33def PRCRawNullEquivalent (s t : PRCRawRatLedger) : Prop :=
34 ∀ eps : PRCRat, PRCRat.positive eps →
35 ∃ N : Nat, ∀ n : Nat, N ≤ n →
36 PRCRat.lt (PRCJCostDistance (s n) (t n)) eps
37
38namespace PRCCauchySeq
39
40/-- Forget a Cauchy ledger to its raw rational ledger. -/
41def raw (u : PRCCauchySeq) : PRCRawRatLedger :=
42 u.term
43
44theorem raw_cauchy (u : PRCCauchySeq) : PRCRawCauchy u.raw :=
45 u.cauchy
46
47@[simp] theorem raw_apply (u : PRCCauchySeq) (n : Nat) :
48 u.raw n = u.term n := rfl
49
50end PRCCauchySeq
51
52/-- Pointwise addition of raw ledgers. -/
53def PRCRawAdd (u v : PRCRawRatLedger) : PRCRawRatLedger :=
54 fun n => u n + v n
55
56/-- Pointwise negation of raw ledgers. -/
57def PRCRawNeg (u : PRCRawRatLedger) : PRCRawRatLedger :=
58 fun n => -u n
59
60/-- Pointwise multiplication of raw ledgers. -/
61def PRCRawMul (u v : PRCRawRatLedger) : PRCRawRatLedger :=
62 fun n => u n * v n
63
64/-- Pointwise non-strict order candidate for raw ledgers. -/
65def PRCRawEventuallyLe (u v : PRCRawRatLedger) : Prop :=
66 ∀ eps : PRCRat, PRCRat.positive eps →
67 ∃ N : Nat, ∀ n : Nat, N ≤ n →
68 PRCRat.lt (u n) (v n + eps)
69
70/-- J-cost distance is invariant under translating both endpoints on the
71right. -/
72theorem PRCJCostDistance_add_right (a b c : PRCRat) :
73 PRCJCostDistance (a + c) (b + c) = PRCJCostDistance a b := by
74 apply PRCRat.toRat_injective
75 rw [PRCJCostDistance_toRat, PRCJCostDistance_toRat]
76 simp [PRCJCostDistanceRatDisplay]
77
78/-- J-cost distance is invariant under translating both endpoints on the left. -/
79theorem PRCJCostDistance_add_left (a b c : PRCRat) :
80 PRCJCostDistance (c + a) (c + b) = PRCJCostDistance a b := by
81 apply PRCRat.toRat_injective
82 rw [PRCJCostDistance_toRat, PRCJCostDistance_toRat]
83 simp [PRCJCostDistanceRatDisplay]
84
85/-- J-cost distance is invariant under negating both endpoints. -/
86theorem PRCJCostDistance_neg_neg (a b : PRCRat) :
87 PRCJCostDistance (-a) (-b) = PRCJCostDistance a b := by
88 apply PRCRat.toRat_injective
89 rw [PRCJCostDistance_toRat, PRCJCostDistance_toRat]
90 simp [PRCJCostDistanceRatDisplay]
91 ring_nf
92
93/-- Exact blocker for addition: pointwise sums of Cauchy ledgers are Cauchy. -/
94def PRCRealAddClosureTarget : Prop :=
95 ∀ u v : PRCCauchySeq, PRCRawCauchy (PRCRawAdd u.raw v.raw)
96
97/-- Exact blocker for additive quotient well-definedness under null distance. -/
98def PRCRealAddCongruenceTarget : Prop :=
99 ∀ u u' v v' : PRCCauchySeq,
100 PRCNullEquivalent u u' →
101 PRCNullEquivalent v v' →
102 PRCRawNullEquivalent
103 (PRCRawAdd u.raw v.raw)
104 (PRCRawAdd u'.raw v'.raw)
105
106/-- Exact blocker for negation: pointwise negations of Cauchy ledgers are
107Cauchy. -/
108def PRCRealNegClosureTarget : Prop :=
109 ∀ u : PRCCauchySeq, PRCRawCauchy (PRCRawNeg u.raw)
110
111/-- Exact blocker for negation quotient well-definedness. -/
112def PRCRealNegCongruenceTarget : Prop :=
113 ∀ u v : PRCCauchySeq,
114 PRCNullEquivalent u v →
115 PRCRawNullEquivalent (PRCRawNeg u.raw) (PRCRawNeg v.raw)
116
117/-- Exact blocker for multiplication: pointwise products of Cauchy ledgers are
118Cauchy. This is expected to require a boundedness lemma for Cauchy ledgers. -/
119def PRCRealMulClosureTarget : Prop :=
120 ∀ u v : PRCCauchySeq, PRCRawCauchy (PRCRawMul u.raw v.raw)
121
122/-- Exact blocker for multiplicative quotient well-definedness under null
123distance. This is also expected to require eventual boundedness. -/
124def PRCRealMulCongruenceTarget : Prop :=
125 ∀ u u' v v' : PRCCauchySeq,
126 PRCNullEquivalent u u' →
127 PRCNullEquivalent v v' →
128 PRCRawNullEquivalent
129 (PRCRawMul u.raw v.raw)
130 (PRCRawMul u'.raw v'.raw)
131
132/-- Exact blocker for the order relation descending to the null-distance
133quotient. -/
134def PRCRealOrderCongruenceTarget : Prop :=
135 ∀ u u' v v' : PRCCauchySeq,
136 PRCNullEquivalent u u' →
137 PRCNullEquivalent v v' →
138 (PRCRawEventuallyLe u.raw v.raw ↔
139 PRCRawEventuallyLe u'.raw v'.raw)
140
141/-- Quantitative closeness for two raw ledgers at a fixed PRC tolerance. -/
142def PRCRawEventuallyClose (s t : PRCRawRatLedger) (eps : PRCRat) : Prop :=
143 ∃ N : Nat, ∀ n : Nat, N ≤ n →
144 PRCRat.lt (PRCJCostDistance (s n) (t n)) eps
145
146/-- A sequence of Cauchy ledgers is Cauchy as a sequence of null-quotient
147representatives when its representative tails are eventually close at every
148positive PRC tolerance. -/
149def PRCRealRepresentativeCauchy (U : Nat → PRCCauchySeq) : Prop :=
150 ∀ eps : PRCRat, PRCRat.positive eps →
151 ∃ N : Nat, ∀ m n : Nat, N ≤ m → N ≤ n →
152 PRCRawEventuallyClose (U m).raw (U n).raw eps
153
154/-- A Cauchy ledger `L` is a representative limit of a sequence of null-quotient
155representatives. -/
156def PRCRealRepresentativeLimit (U : Nat → PRCCauchySeq)
157 (L : PRCCauchySeq) : Prop :=
158 ∀ eps : PRCRat, PRCRat.positive eps →
159 ∃ N : Nat, ∀ n : Nat, N ≤ n →
160 PRCRawEventuallyClose (U n).raw L.raw eps
161
162/-- Exact blocker for completeness of the internal null quotient. This is the
163diagonal theorem: every Cauchy sequence of Cauchy-ledger representatives has a
164Cauchy-ledger representative limit. -/
165def PRCRealCompletenessTarget : Prop :=
166 ∀ U : Nat → PRCCauchySeq,
167 PRCRealRepresentativeCauchy U →
168 ∃ L : PRCCauchySeq, PRCRealRepresentativeLimit U L
169
170/-- Pointwise sums of Cauchy ledgers are Cauchy. -/
171theorem PRCRealAddClosureTarget_proved : PRCRealAddClosureTarget := by
172 intro u v eps heps
173 rcases PRCJCostDistanceTriangleModulusTarget_proved eps heps with
174 ⟨delta, hdelta_pos, hdelta⟩
175 rcases u.cauchy delta hdelta_pos with ⟨Nu, hNu⟩
176 rcases v.cauchy delta hdelta_pos with ⟨Nv, hNv⟩
177 refine ⟨max Nu Nv, ?_⟩
178 intro m n hm hn
179 have hmu : Nu ≤ m := le_trans (Nat.le_max_left Nu Nv) hm
180 have hnu : Nu ≤ n := le_trans (Nat.le_max_left Nu Nv) hn
181 have hmv : Nv ≤ m := le_trans (Nat.le_max_right Nu Nv) hm
182 have hnv : Nv ≤ n := le_trans (Nat.le_max_right Nu Nv) hn
183 exact hdelta
184 ((u.term m) + (v.term m))
185 ((u.term n) + (v.term m))
186 ((u.term n) + (v.term n))
187 (by
188 rw [PRCJCostDistance_add_right]
189 exact hNu m n hmu hnu)
190 (by
191 rw [PRCJCostDistance_add_left]
192 exact hNv m n hmv hnv)
193
194/-- Pointwise negations of Cauchy ledgers are Cauchy. -/
195theorem PRCRealNegClosureTarget_proved : PRCRealNegClosureTarget := by
196 intro u eps heps
197 rcases u.cauchy eps heps with ⟨N, hN⟩
198 refine ⟨N, ?_⟩
199 intro m n hm hn
200 change PRCRat.lt (PRCJCostDistance (-(u.term m)) (-(u.term n))) eps
201 rw [PRCJCostDistance_neg_neg]
202 exact hN m n hm hn
203
204/-- Addition respects null equivalence. -/
205theorem PRCRealAddCongruenceTarget_proved :
206 PRCRealAddCongruenceTarget := by
207 intro u u' v v' huu hvv eps heps
208 rcases PRCJCostDistanceTriangleModulusTarget_proved eps heps with
209 ⟨delta, hdelta_pos, hdelta⟩
210 rcases huu delta hdelta_pos with ⟨Nu, hNu⟩
211 rcases hvv delta hdelta_pos with ⟨Nv, hNv⟩
212 refine ⟨max Nu Nv, ?_⟩
213 intro n hn
214 have hnu : Nu ≤ n := le_trans (Nat.le_max_left Nu Nv) hn
215 have hnv : Nv ≤ n := le_trans (Nat.le_max_right Nu Nv) hn
216 exact hdelta
217 ((u.term n) + (v.term n))
218 ((u'.term n) + (v.term n))
219 ((u'.term n) + (v'.term n))
220 (by
221 rw [PRCJCostDistance_add_right]
222 exact hNu n hnu)
223 (by
224 rw [PRCJCostDistance_add_left]
225 exact hNv n hnv)
226
227/-- Negation respects null equivalence. -/
228theorem PRCRealNegCongruenceTarget_proved :
229 PRCRealNegCongruenceTarget := by
230 intro u v huv eps heps
231 rcases huv eps heps with ⟨N, hN⟩
232 refine ⟨N, ?_⟩
233 intro n hn
234 change PRCRat.lt (PRCJCostDistance (-(u.term n)) (-(v.term n))) eps
235 rw [PRCJCostDistance_neg_neg]
236 exact hN n hn
237
238/-- Conditional construction of a pointwise-sum Cauchy ledger from the addition
239closure target. -/
240def PRCCauchySeq.addOf
241 (hadd : PRCRealAddClosureTarget) (u v : PRCCauchySeq) : PRCCauchySeq where
242 term := PRCRawAdd u.raw v.raw
243 cauchy := hadd u v
244
245/-- Conditional construction of a pointwise-negation Cauchy ledger from the
246negation closure target. -/
247def PRCCauchySeq.negOf
248 (hneg : PRCRealNegClosureTarget) (u : PRCCauchySeq) : PRCCauchySeq where
249 term := PRCRawNeg u.raw
250 cauchy := hneg u
251
252/-- Conditional construction of a pointwise-product Cauchy ledger from the
253multiplication closure target. -/
254def PRCCauchySeq.mulOf
255 (hmul : PRCRealMulClosureTarget) (u v : PRCCauchySeq) : PRCCauchySeq where
256 term := PRCRawMul u.raw v.raw
257 cauchy := hmul u v
258
259/-- Conditional addition on the closed null quotient. -/
260noncomputable def PRCRealNullClosed.addOf
261 (hadd : PRCRealAddClosureTarget)
262 (hcong : PRCRealAddCongruenceTarget) :
263 PRCRealNullClosed → PRCRealNullClosed → PRCRealNullClosed :=
264 Quot.lift₂
265 (fun u v =>
266 Quot.mk (PRCNullDistanceSetoidOfTransitive PRCNullDistanceTransitiveTarget_proved)
267 (PRCCauchySeq.addOf hadd u v))
268 (by
269 intro u v₁ v₂ hv
270 apply Quot.sound
271 exact hcong u u v₁ v₂ (PRCNullEquivalent.refl u) hv)
272 (by
273 intro u₁ u₂ v hu
274 apply Quot.sound
275 exact hcong u₁ u₂ v v hu (PRCNullEquivalent.refl v))
276
277/-- Conditional negation on the closed null quotient. -/
278noncomputable def PRCRealNullClosed.negOf
279 (hneg : PRCRealNegClosureTarget)
280 (hcong : PRCRealNegCongruenceTarget) :
281 PRCRealNullClosed → PRCRealNullClosed :=
282 Quot.lift
283 (fun u =>
284 Quot.mk (PRCNullDistanceSetoidOfTransitive PRCNullDistanceTransitiveTarget_proved)
285 (PRCCauchySeq.negOf hneg u))
286 (by
287 intro u v huv
288 apply Quot.sound
289 exact hcong u v huv)
290
291/-- Conditional multiplication on the closed null quotient. -/
292noncomputable def PRCRealNullClosed.mulOf
293 (hmul : PRCRealMulClosureTarget)
294 (hcong : PRCRealMulCongruenceTarget) :
295 PRCRealNullClosed → PRCRealNullClosed → PRCRealNullClosed :=
296 Quot.lift₂
297 (fun u v =>
298 Quot.mk (PRCNullDistanceSetoidOfTransitive PRCNullDistanceTransitiveTarget_proved)
299 (PRCCauchySeq.mulOf hmul u v))
300 (by
301 intro u v₁ v₂ hv
302 apply Quot.sound
303 exact hcong u u v₁ v₂ (PRCNullEquivalent.refl u) hv)
304 (by
305 intro u₁ u₂ v hu
306 apply Quot.sound
307 exact hcong u₁ u₂ v v hu (PRCNullEquivalent.refl v))
308
309/-- Bundle of exact blockers for the next real-completion phase. -/
310structure PRCRealCompleteOrderedFieldTargets : Prop where
311 add_closure : PRCRealAddClosureTarget
312 add_congruence : PRCRealAddCongruenceTarget
313 neg_closure : PRCRealNegClosureTarget
314 neg_congruence : PRCRealNegCongruenceTarget
315 mul_closure : PRCRealMulClosureTarget = PRCRealMulClosureTarget
316 mul_congruence : PRCRealMulCongruenceTarget = PRCRealMulCongruenceTarget
317 order_congruence : PRCRealOrderCongruenceTarget = PRCRealOrderCongruenceTarget
318 completeness : PRCRealCompletenessTarget = PRCRealCompletenessTarget
319
320/-- Conditional first complete-ordered-field surface. It records that the
321carrier and rational embedding are closed, while algebra/order/completeness are
322reduced to named exact targets. -/
323structure PRCRealCompleteOrderedFieldConditionalCertificate : Prop where
324 carrier : Nonempty PRCRealNullClosed
325 rat_embedding : Nonempty (PRCRat → PRCRealNullClosed)
326 targets : PRCRealCompleteOrderedFieldTargets
327 add_operation_from_targets :
328 PRCRealAddClosureTarget →
329 PRCRealAddCongruenceTarget →
330 Nonempty (PRCRealNullClosed → PRCRealNullClosed → PRCRealNullClosed)
331 neg_operation_from_targets :
332 PRCRealNegClosureTarget →
333 PRCRealNegCongruenceTarget →
334 Nonempty (PRCRealNullClosed → PRCRealNullClosed)
335 mul_operation_from_targets :
336 PRCRealMulClosureTarget →
337 PRCRealMulCongruenceTarget →
338 Nonempty (PRCRealNullClosed → PRCRealNullClosed → PRCRealNullClosed)
339 strength_tag : StrengthTag.traceClosure = StrengthTag.traceClosure
340
341/-- Build Order step 10, first pass: quotient algebra is reduced to exact
342closure and congruence targets. -/
343theorem prc_real_complete_ordered_field_conditional_certificate :
344 PRCRealCompleteOrderedFieldConditionalCertificate where
345 carrier := ⟨PRCRealNullClosed.ofRat 0⟩
346 rat_embedding := ⟨PRCRealNullClosed.ofRat⟩
347 targets := {
348 add_closure := PRCRealAddClosureTarget_proved
349 add_congruence := PRCRealAddCongruenceTarget_proved
350 neg_closure := PRCRealNegClosureTarget_proved
351 neg_congruence := PRCRealNegCongruenceTarget_proved
352 mul_closure := rfl
353 mul_congruence := rfl
354 order_congruence := rfl
355 completeness := rfl
356 }
357 add_operation_from_targets := by
358 intro hadd hcong
359 exact ⟨PRCRealNullClosed.addOf hadd hcong⟩
360 neg_operation_from_targets := by
361 intro hneg hcong
362 exact ⟨PRCRealNullClosed.negOf hneg hcong⟩
363 mul_operation_from_targets := by
364 intro hmul hcong
365 exact ⟨PRCRealNullClosed.mulOf hmul hcong⟩
366 strength_tag := rfl
367
368end PrimitiveRecognitionCalculus
369end Foundation
370end IndisputableMonolith
371