IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealCompleteness
IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealCompleteness.lean · 593 lines · 37 declarations
show as:
view math explainer →
1/-
2 PrimitiveRecognitionCalculus/RealCompleteness.lean
3
4 Round-trip source:
5 δ/PRC_Universal_Foundation_Execution_Plan_20260526.html
6
7 Spec anchor:
8 Build Order step 10e: replace the placeholder completeness target with a
9 theorem-shaped internal Cauchy-of-Cauchy statement and isolate the exact
10 diagonal blocker.
11
12 This file closes the construction fact that every raw PRC rational Cauchy
13 ledger already determines a point of the null quotient, then closes the
14 explicit `PRCRealCompletenessTarget` diagonal theorem.
15-/
16
17import Mathlib
18import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealOrderCongruence
19
20namespace IndisputableMonolith
21namespace Foundation
22namespace PrimitiveRecognitionCalculus
23
24/-- Every raw rational Cauchy ledger can be packaged as a `PRCCauchySeq`. -/
25def PRCRawCauchyRealizationTarget : Prop :=
26 ∀ s : PRCRawRatLedger,
27 PRCRawCauchy s →
28 ∃ u : PRCCauchySeq, u.raw = s
29
30theorem PRCRawCauchyRealizationTarget_proved :
31 PRCRawCauchyRealizationTarget := by
32 intro s hs
33 refine ⟨{ term := s, cauchy := hs }, ?_⟩
34 rfl
35
36/-- Every raw rational Cauchy ledger determines a point of the final
37null-distance quotient. -/
38def PRCRawCauchyQuotientPointTarget : Prop :=
39 ∀ s : PRCRawRatLedger,
40 PRCRawCauchy s →
41 Nonempty PRCRealNullClosed
42
43theorem PRCRawCauchyQuotientPointTarget_proved :
44 PRCRawCauchyQuotientPointTarget := by
45 intro s hs
46 rcases PRCRawCauchyRealizationTarget_proved s hs with ⟨u, _hu⟩
47 exact ⟨Quot.mk
48 (PRCNullDistanceSetoidOfTransitive PRCNullDistanceTransitiveTarget_proved)
49 u⟩
50
51/-- Named diagonal selection blocker for internal completeness. It asks for an
52actual Cauchy ledger limit for every representative-Cauchy sequence of Cauchy
53ledgers. -/
54def PRCRealDiagonalSelectionTarget : Prop :=
55 ∀ U : Nat → PRCCauchySeq,
56 PRCRealRepresentativeCauchy U →
57 ∃ L : PRCCauchySeq, PRCRealRepresentativeLimit U L
58
59/-- Sharper diagonal blocker: construct the raw rational ledger underneath the
60limit and prove both its Cauchy property and its limit property. This is the
61mathematical work left after the quotient and packaging bookkeeping is removed. -/
62def PRCRealRawDiagonalLedgerTarget : Prop :=
63 ∀ U : Nat → PRCCauchySeq,
64 PRCRealRepresentativeCauchy U →
65 ∃ s : PRCRawRatLedger,
66 PRCRawCauchy s ∧
67 ∀ eps : PRCRat, PRCRat.positive eps →
68 ∃ N : Nat, ∀ n : Nat, N ≤ n →
69 PRCRawEventuallyClose (U n).raw s eps
70
71/-- Tail-selection version of the raw diagonal theorem. It asks for an explicit
72choice of a sufficiently deep raw index in each representative, so the diagonal
73ledger is made from actual terms of the input Cauchy ledgers. -/
74def PRCRealTailSelectionTarget : Prop :=
75 ∀ U : Nat → PRCCauchySeq,
76 PRCRealRepresentativeCauchy U →
77 ∃ pick : Nat → Nat,
78 let s : PRCRawRatLedger := fun n => (U n).term (pick n)
79 PRCRawCauchy s ∧
80 ∀ eps : PRCRat, PRCRat.positive eps →
81 ∃ N : Nat, ∀ n : Nat, N ≤ n →
82 PRCRawEventuallyClose (U n).raw s eps
83
84/-- The PRC rational unit-fraction tolerance `1 / (n+1)`. This is verifier
85display machinery for the completeness proof, not a new PRC primitive. -/
86def PRCUnitFraction (n : Nat) : PRCRat :=
87 let den : DistinctionNat := DistinctionNat.ofNat (n + 1)
88 have hden : den ≠ DistinctionNat.zero := by
89 intro h
90 have hnat := congrArg DistinctionNat.toNat h
91 rw [DistinctionNat.toNat_ofNat, DistinctionNat.toNat_zero] at hnat
92 omega
93 PRCRat.mk {
94 num := SignedOrbit.one
95 den := den
96 den_ne_zero := hden
97 }
98
99theorem PRCUnitFraction_toRat (n : Nat) :
100 (PRCUnitFraction n).toRat = (1 : ℚ) / (n + 1 : Nat) := by
101 unfold PRCUnitFraction
102 rw [PRCRat.toRat_mk]
103 unfold RatioOrbit.toRat
104 simp [SignedOrbit.one_toInt, DistinctionNat.toNat_ofNat]
105
106theorem PRCUnitFraction_positive (n : Nat) :
107 PRCRat.positive (PRCUnitFraction n) := by
108 rw [PRCRat.positive_iff_toRat_pos, PRCUnitFraction_toRat]
109 positivity
110
111/-- Exact cofinal tolerance-schedule target needed by the tail-selection
112diagonal proof. -/
113def PRCRealCofinalToleranceScheduleTarget : Prop :=
114 ∃ tau : Nat → PRCRat,
115 (∀ n : Nat, PRCRat.positive (tau n)) ∧
116 ∀ eps : PRCRat, PRCRat.positive eps →
117 ∃ N : Nat, ∀ n : Nat, N ≤ n → PRCRat.lt (tau n) eps
118
119theorem PRCUnitFraction_eventually_lt
120 {eps : PRCRat} (heps : PRCRat.positive eps) :
121 ∃ N : Nat, ∀ n : Nat, N ≤ n →
122 PRCRat.lt (PRCUnitFraction n) eps := by
123 have heps_pos : (0 : ℚ) < eps.toRat :=
124 (PRCRat.positive_iff_toRat_pos eps).mp heps
125 rcases exists_nat_gt (1 / eps.toRat) with ⟨N, hN⟩
126 refine ⟨N, ?_⟩
127 intro n hn
128 rw [PRCRat.lt_iff_toRat_lt, PRCUnitFraction_toRat]
129 have hN_le_n : (N : ℚ) ≤ (n : ℚ) := by exact_mod_cast hn
130 have hn_lt_succ : (n : ℚ) < (n + 1 : Nat) := by
131 norm_num
132 have hgt : (1 / eps.toRat : ℚ) < (n + 1 : Nat) := by
133 exact lt_of_lt_of_le hN (le_trans hN_le_n (le_of_lt hn_lt_succ))
134 have hprod : (1 : ℚ) < eps.toRat * (n + 1 : Nat) := by
135 have hmul := mul_lt_mul_of_pos_left hgt heps_pos
136 have hone : eps.toRat * (1 / eps.toRat) = (1 : ℚ) := by
137 field_simp [ne_of_gt heps_pos]
138 rw [hone] at hmul
139 simpa [mul_comm] using hmul
140 have hden_pos : (0 : ℚ) < (n + 1 : Nat) := by positivity
141 field_simp [ne_of_gt hden_pos]
142 linarith
143
144theorem PRCRealCofinalToleranceScheduleTarget_proved :
145 PRCRealCofinalToleranceScheduleTarget := by
146 refine ⟨PRCUnitFraction, PRCUnitFraction_positive, ?_⟩
147 intro eps heps
148 exact PRCUnitFraction_eventually_lt heps
149
150theorem PRCRat.lt_trans {a b c : PRCRat}
151 (hab : PRCRat.lt a b) (hbc : PRCRat.lt b c) :
152 PRCRat.lt a c := by
153 rw [PRCRat.lt_iff_toRat_lt] at hab hbc ⊢
154 exact _root_.lt_trans hab hbc
155
156/-- Three-leg form of the J-cost distance modulus. The diagonal proof naturally
157travels from a selected diagonal point to an intermediate raw point, then across
158representatives, then back down another selected diagonal point. -/
159def PRCJCostDistanceThreeLegModulusTarget : Prop :=
160 ∀ eps : PRCRat, PRCRat.positive eps →
161 ∃ delta : PRCRat, PRCRat.positive delta ∧
162 ∀ a b c d : PRCRat,
163 PRCRat.lt (PRCJCostDistance a b) delta →
164 PRCRat.lt (PRCJCostDistance b c) delta →
165 PRCRat.lt (PRCJCostDistance c d) delta →
166 PRCRat.lt (PRCJCostDistance a d) eps
167
168theorem PRCJCostDistanceThreeLegModulusTarget_proved :
169 PRCJCostDistanceThreeLegModulusTarget := by
170 intro eps heps
171 rcases PRCJCostDistanceTriangleModulusTarget_proved eps heps with
172 ⟨eta, heta_pos, heta_tri⟩
173 rcases PRCJCostDistanceTriangleModulusTarget_proved eta heta_pos with
174 ⟨theta, htheta_pos, htheta_tri⟩
175 rcases PRCUnitFraction_eventually_lt heta_pos with ⟨Neta, hNeta⟩
176 rcases PRCUnitFraction_eventually_lt htheta_pos with ⟨Ntheta, hNtheta⟩
177 let delta := PRCUnitFraction (max Neta Ntheta)
178 have hdelta_pos : PRCRat.positive delta := PRCUnitFraction_positive _
179 have hdelta_lt_eta : PRCRat.lt delta eta := by
180 exact hNeta (max Neta Ntheta) (Nat.le_max_left Neta Ntheta)
181 have hdelta_lt_theta : PRCRat.lt delta theta := by
182 exact hNtheta (max Neta Ntheta) (Nat.le_max_right Neta Ntheta)
183 refine ⟨delta, hdelta_pos, ?_⟩
184 intro a b c d hab hbc hcd
185 have hab_eta : PRCRat.lt (PRCJCostDistance a b) eta :=
186 PRCRat.lt_trans hab hdelta_lt_eta
187 have hbc_theta : PRCRat.lt (PRCJCostDistance b c) theta :=
188 PRCRat.lt_trans hbc hdelta_lt_theta
189 have hcd_theta : PRCRat.lt (PRCJCostDistance c d) theta :=
190 PRCRat.lt_trans hcd hdelta_lt_theta
191 have hbd_eta : PRCRat.lt (PRCJCostDistance b d) eta :=
192 htheta_tri b c d hbc_theta hcd_theta
193 exact heta_tri a b d hab_eta hbd_eta
194
195/-- A candidate index is deep enough for one raw Cauchy ledger at one
196tolerance. -/
197def PRCRowTailBound (u : PRCCauchySeq) (eps : PRCRat) (N : Nat) : Prop :=
198 ∀ m n : Nat, N ≤ m → N ≤ n →
199 PRCRat.lt (PRCJCostDistance (u.term m) (u.term n)) eps
200
201theorem PRCRowTailBound_mono {u : PRCCauchySeq} {eps : PRCRat}
202 {N M : Nat} (hNM : N ≤ M) (hN : PRCRowTailBound u eps N) :
203 PRCRowTailBound u eps M := by
204 intro m n hm hn
205 exact hN m n (le_trans hNM hm) (le_trans hNM hn)
206
207theorem PRCRealFiniteRowTailBound_exists
208 (U : Nat → PRCCauchySeq) (eps : PRCRat)
209 (heps : PRCRat.positive eps) :
210 ∀ r : Nat,
211 ∃ N : Nat, ∀ i : Nat, i ≤ r → PRCRowTailBound (U i) eps N
212 | 0 => by
213 rcases (U 0).cauchy eps heps with ⟨N, hN⟩
214 refine ⟨N, ?_⟩
215 intro i hi
216 have hi0 : i = 0 := by omega
217 subst hi0
218 exact hN
219 | Nat.succ r => by
220 rcases PRCRealFiniteRowTailBound_exists U eps heps r with
221 ⟨Nprev, hprev⟩
222 rcases (U (Nat.succ r)).cauchy eps heps with ⟨Nlast, hlast⟩
223 refine ⟨max Nprev Nlast, ?_⟩
224 intro i hi
225 by_cases hir : i ≤ r
226 · exact PRCRowTailBound_mono
227 (Nat.le_max_left Nprev Nlast) (hprev i hir)
228 · have hi_last : i = Nat.succ r := by omega
229 subst hi_last
230 exact PRCRowTailBound_mono
231 (Nat.le_max_right Nprev Nlast) hlast
232
233/-- Exact finite-row scheduler needed by the diagonal tail-selection proof:
234for every diagonal row `r`, choose one raw index deep enough for all rows
235`0,...,r` at the tolerance `1/(r+1)`. -/
236def PRCRealFiniteRowTailSelectionTarget : Prop :=
237 ∀ U : Nat → PRCCauchySeq,
238 ∃ pick : Nat → Nat,
239 ∀ r i : Nat, i ≤ r →
240 PRCRowTailBound (U i) (PRCUnitFraction r) (pick r)
241
242theorem PRCRealFiniteRowTailSelectionTarget_proved :
243 PRCRealFiniteRowTailSelectionTarget := by
244 intro U
245 choose pick hpick using
246 fun r => PRCRealFiniteRowTailBound_exists
247 U (PRCUnitFraction r) (PRCUnitFraction_positive r) r
248 exact ⟨pick, hpick⟩
249
250/-- A raw index is deep enough for every eligible representative row
251`i ≤ r` to be close to the target row `r`, once the outer representative
252threshold has been crossed. -/
253def PRCRepresentativeFiniteTailBound
254 (U : Nat → PRCCauchySeq) (eps : PRCRat)
255 (outer r N : Nat) : Prop :=
256 ∀ i k : Nat, outer ≤ i → i ≤ r → N ≤ k →
257 PRCRat.lt (PRCJCostDistance ((U i).term k) ((U r).term k)) eps
258
259theorem PRCRepresentativeFiniteTailBound_mono
260 {U : Nat → PRCCauchySeq} {eps : PRCRat}
261 {outer r N M : Nat} (hNM : N ≤ M)
262 (hN : PRCRepresentativeFiniteTailBound U eps outer r N) :
263 PRCRepresentativeFiniteTailBound U eps outer r M := by
264 intro i k hoi hir hMk
265 exact hN i k hoi hir (le_trans hNM hMk)
266
267theorem PRCRepresentativeFiniteTailBound_exists
268 (U : Nat → PRCCauchySeq) (eps : PRCRat)
269 (outer r : Nat)
270 (houter : ∀ m n : Nat, outer ≤ m → outer ≤ n →
271 PRCRawEventuallyClose (U m).raw (U n).raw eps) :
272 ∃ N : Nat, PRCRepresentativeFiniteTailBound U eps outer r N := by
273 suffices hfinite :
274 ∀ limit : Nat,
275 limit ≤ r →
276 ∃ N : Nat,
277 ∀ i k : Nat, outer ≤ i → i ≤ limit → N ≤ k →
278 PRCRat.lt
279 (PRCJCostDistance ((U i).term k) ((U r).term k)) eps by
280 rcases hfinite r (Nat.le_refl r) with ⟨N, hN⟩
281 exact ⟨N, hN⟩
282 intro limit
283 induction limit with
284 | zero =>
285 intro _hlim
286 by_cases houter_zero : outer ≤ 0
287 · have houter_r : outer ≤ r := by omega
288 rcases houter 0 r houter_zero houter_r with ⟨N, hN⟩
289 refine ⟨N, ?_⟩
290 intro i k hoi hir hNk
291 have hi0 : i = 0 := by omega
292 subst hi0
293 simpa [PRCCauchySeq.raw] using hN k hNk
294 · refine ⟨0, ?_⟩
295 intro i _k hoi hir _h0k
296 have : outer ≤ 0 := by omega
297 exact False.elim (houter_zero this)
298 | succ limit ih =>
299 intro hlim
300 rcases ih (Nat.le_of_succ_le hlim) with ⟨Nprev, hprev⟩
301 by_cases hlast : outer ≤ Nat.succ limit
302 · rcases houter (Nat.succ limit) r hlast
303 (le_trans hlast hlim) with
304 ⟨Nlast, hNlast⟩
305 refine ⟨max Nprev Nlast, ?_⟩
306 intro i k hoi hir hmaxk
307 by_cases hir_prev : i ≤ limit
308 · exact hprev i k hoi hir_prev
309 (le_trans (Nat.le_max_left Nprev Nlast) hmaxk)
310 · have hi_last : i = Nat.succ limit := by omega
311 subst hi_last
312 simpa [PRCCauchySeq.raw] using
313 hNlast k (le_trans (Nat.le_max_right Nprev Nlast) hmaxk)
314 · refine ⟨Nprev, ?_⟩
315 intro i k hoi hir hNprevk
316 have hir_prev : i ≤ limit := by omega
317 exact hprev i k hoi hir_prev hNprevk
318
319/-- Exact finite representative scheduler needed by the diagonal proof. For
320each tolerance rung it chooses the outer Cauchy-representative threshold and a
321raw depth that realizes all finite representative-tail comparisons up to that
322rung. -/
323def PRCRealFiniteRepresentativeTailSelectionTarget : Prop :=
324 ∀ U : Nat → PRCCauchySeq,
325 PRCRealRepresentativeCauchy U →
326 ∃ outer pick : Nat → Nat,
327 (∀ r m n : Nat, outer r ≤ m → outer r ≤ n →
328 PRCRawEventuallyClose (U m).raw (U n).raw (PRCUnitFraction r)) ∧
329 ∀ r : Nat,
330 PRCRepresentativeFiniteTailBound
331 U (PRCUnitFraction r) (outer r) r (pick r)
332
333theorem PRCRealFiniteRepresentativeTailSelectionTarget_proved :
334 PRCRealFiniteRepresentativeTailSelectionTarget := by
335 intro U hU
336 choose outer houter using
337 fun r => hU (PRCUnitFraction r) (PRCUnitFraction_positive r)
338 choose pick hpick using
339 fun r => PRCRepresentativeFiniteTailBound_exists
340 U (PRCUnitFraction r) (outer r) r (houter r)
341 exact ⟨outer, pick, houter, hpick⟩
342
343/-- Single finite diagonal scheduler: one raw choice function satisfies both
344finite row-tail and finite representative-tail constraints at each tolerance
345rung. This is still finite-rung scheduling, not yet the completed global
346tail-selection theorem. -/
347def PRCRealFiniteDiagonalScheduleTarget : Prop :=
348 ∀ U : Nat → PRCCauchySeq,
349 PRCRealRepresentativeCauchy U →
350 ∃ outer pick : Nat → Nat,
351 (∀ r m n : Nat, outer r ≤ m → outer r ≤ n →
352 PRCRawEventuallyClose (U m).raw (U n).raw (PRCUnitFraction r)) ∧
353 (∀ r i : Nat, i ≤ r →
354 PRCRowTailBound (U i) (PRCUnitFraction r) (pick r)) ∧
355 ∀ r : Nat,
356 PRCRepresentativeFiniteTailBound
357 U (PRCUnitFraction r) (outer r) r (pick r)
358
359theorem PRCRealFiniteDiagonalScheduleTarget_proved :
360 PRCRealFiniteDiagonalScheduleTarget := by
361 intro U hU
362 rcases PRCRealFiniteRowTailSelectionTarget_proved U with
363 ⟨rowPick, hrowPick⟩
364 rcases PRCRealFiniteRepresentativeTailSelectionTarget_proved U hU with
365 ⟨outer, repPick, houter, hrepPick⟩
366 refine ⟨outer, fun r => max (rowPick r) (repPick r), houter, ?_, ?_⟩
367 · intro r i hir
368 exact PRCRowTailBound_mono
369 (Nat.le_max_left (rowPick r) (repPick r))
370 (hrowPick r i hir)
371 · intro r
372 exact PRCRepresentativeFiniteTailBound_mono
373 (Nat.le_max_right (rowPick r) (repPick r))
374 (hrepPick r)
375
376theorem PRCRealTailSelectionTarget_proved :
377 PRCRealTailSelectionTarget := by
378 intro U hU
379 rcases PRCRealFiniteDiagonalScheduleTarget_proved U hU with
380 ⟨_outer, pick, _houterTau, hrow, _hrep⟩
381 refine ⟨pick, ?_, ?_⟩
382 · intro eps heps
383 rcases PRCJCostDistanceThreeLegModulusTarget_proved eps heps with
384 ⟨delta, hdelta_pos, hthree⟩
385 rcases hU delta hdelta_pos with ⟨Nrep, hNrep⟩
386 rcases PRCUnitFraction_eventually_lt hdelta_pos with ⟨Ntau, hNtau⟩
387 refine ⟨max Nrep Ntau, ?_⟩
388 intro m n hm hn
389 have hm_rep : Nrep ≤ m := le_trans (Nat.le_max_left Nrep Ntau) hm
390 have hn_rep : Nrep ≤ n := le_trans (Nat.le_max_left Nrep Ntau) hn
391 have hm_tauN : Ntau ≤ m := le_trans (Nat.le_max_right Nrep Ntau) hm
392 have hn_tauN : Ntau ≤ n := le_trans (Nat.le_max_right Nrep Ntau) hn
393 have htaum_delta : PRCRat.lt (PRCUnitFraction m) delta :=
394 hNtau m hm_tauN
395 have htaun_delta : PRCRat.lt (PRCUnitFraction n) delta :=
396 hNtau n hn_tauN
397 rcases hNrep m n hm_rep hn_rep with ⟨Npair, hNpair⟩
398 let K : Nat := max (pick m) (max (pick n) Npair)
399 have hpickmK : pick m ≤ K := Nat.le_max_left (pick m) (max (pick n) Npair)
400 have hpicknK : pick n ≤ K :=
401 le_trans (Nat.le_max_left (pick n) Npair)
402 (Nat.le_max_right (pick m) (max (pick n) Npair))
403 have hpairK : Npair ≤ K :=
404 le_trans (Nat.le_max_right (pick n) Npair)
405 (Nat.le_max_right (pick m) (max (pick n) Npair))
406 have hleg1_tau :
407 PRCRat.lt
408 (PRCJCostDistance ((U m).term (pick m)) ((U m).term K))
409 (PRCUnitFraction m) :=
410 (hrow m m (Nat.le_refl m)) (pick m) K (Nat.le_refl (pick m)) hpickmK
411 have hleg1 :
412 PRCRat.lt
413 (PRCJCostDistance ((U m).term (pick m)) ((U m).term K))
414 delta :=
415 PRCRat.lt_trans hleg1_tau htaum_delta
416 have hleg2 :
417 PRCRat.lt
418 (PRCJCostDistance ((U m).term K) ((U n).term K))
419 delta := by
420 simpa [PRCCauchySeq.raw] using hNpair K hpairK
421 have hleg3_tau :
422 PRCRat.lt
423 (PRCJCostDistance ((U n).term K) ((U n).term (pick n)))
424 (PRCUnitFraction n) :=
425 (hrow n n (Nat.le_refl n)) K (pick n) hpicknK (Nat.le_refl (pick n))
426 have hleg3 :
427 PRCRat.lt
428 (PRCJCostDistance ((U n).term K) ((U n).term (pick n)))
429 delta :=
430 PRCRat.lt_trans hleg3_tau htaun_delta
431 exact hthree
432 ((U m).term (pick m)) ((U m).term K)
433 ((U n).term K) ((U n).term (pick n))
434 hleg1 hleg2 hleg3
435 · intro eps heps
436 rcases PRCJCostDistanceThreeLegModulusTarget_proved eps heps with
437 ⟨delta, hdelta_pos, hthree⟩
438 rcases hU delta hdelta_pos with ⟨Nrep, hNrep⟩
439 rcases PRCUnitFraction_eventually_lt hdelta_pos with ⟨Ntau, hNtau⟩
440 refine ⟨max Nrep Ntau, ?_⟩
441 intro n hn
442 have hn_rep : Nrep ≤ n := le_trans (Nat.le_max_left Nrep Ntau) hn
443 rcases (U n).cauchy delta hdelta_pos with ⟨NrowN, hNrowN⟩
444 refine ⟨max (max Nrep Ntau) NrowN, ?_⟩
445 intro l hl
446 have hl_rep : Nrep ≤ l :=
447 le_trans (Nat.le_max_left Nrep Ntau)
448 (le_trans (Nat.le_max_left (max Nrep Ntau) NrowN) hl)
449 have hl_tauN : Ntau ≤ l :=
450 le_trans (Nat.le_max_right Nrep Ntau)
451 (le_trans (Nat.le_max_left (max Nrep Ntau) NrowN) hl)
452 have hl_rowN : NrowN ≤ l :=
453 le_trans (Nat.le_max_right (max Nrep Ntau) NrowN) hl
454 have htaul_delta : PRCRat.lt (PRCUnitFraction l) delta :=
455 hNtau l hl_tauN
456 rcases hNrep n l hn_rep hl_rep with ⟨Npair, hNpair⟩
457 let K : Nat := max l (max (pick l) Npair)
458 have hlK : l ≤ K := Nat.le_max_left l (max (pick l) Npair)
459 have hpicklK : pick l ≤ K :=
460 le_trans (Nat.le_max_left (pick l) Npair)
461 (Nat.le_max_right l (max (pick l) Npair))
462 have hpairK : Npair ≤ K :=
463 le_trans (Nat.le_max_right (pick l) Npair)
464 (Nat.le_max_right l (max (pick l) Npair))
465 have hrowNK : NrowN ≤ K := le_trans hl_rowN hlK
466 have hleg1 :
467 PRCRat.lt
468 (PRCJCostDistance ((U n).term l) ((U n).term K))
469 delta :=
470 hNrowN l K hl_rowN hrowNK
471 have hleg2 :
472 PRCRat.lt
473 (PRCJCostDistance ((U n).term K) ((U l).term K))
474 delta := by
475 simpa [PRCCauchySeq.raw] using hNpair K hpairK
476 have hleg3_tau :
477 PRCRat.lt
478 (PRCJCostDistance ((U l).term K) ((U l).term (pick l)))
479 (PRCUnitFraction l) :=
480 (hrow l l (Nat.le_refl l)) K (pick l) hpicklK (Nat.le_refl (pick l))
481 have hleg3 :
482 PRCRat.lt
483 (PRCJCostDistance ((U l).term K) ((U l).term (pick l)))
484 delta :=
485 PRCRat.lt_trans hleg3_tau htaul_delta
486 exact hthree
487 ((U n).term l) ((U n).term K)
488 ((U l).term K) ((U l).term (pick l))
489 hleg1 hleg2 hleg3
490
491/-- An explicit tail-selection diagonal is enough to build the raw diagonal
492ledger target. -/
493theorem PRCRealRawDiagonalLedgerTarget_of_tail_selection
494 (htail : PRCRealTailSelectionTarget) :
495 PRCRealRawDiagonalLedgerTarget := by
496 intro U hU
497 rcases htail U hU with ⟨pick, hs_cauchy, hs_limit⟩
498 exact ⟨fun n => (U n).term (pick n), hs_cauchy, hs_limit⟩
499
500theorem PRCRealRawDiagonalLedgerTarget_proved :
501 PRCRealRawDiagonalLedgerTarget :=
502 PRCRealRawDiagonalLedgerTarget_of_tail_selection
503 PRCRealTailSelectionTarget_proved
504
505/-- A raw diagonal ledger packages immediately as the representative limit
506needed by the quotient-level diagonal selection target. -/
507theorem PRCRealDiagonalSelectionTarget_of_raw_diagonal_ledger
508 (hraw : PRCRealRawDiagonalLedgerTarget) :
509 PRCRealDiagonalSelectionTarget := by
510 intro U hU
511 rcases hraw U hU with ⟨s, hs_cauchy, hs_limit⟩
512 refine ⟨{ term := s, cauchy := hs_cauchy }, ?_⟩
513 simpa [PRCRealRepresentativeLimit, PRCCauchySeq.raw] using hs_limit
514
515theorem PRCRealDiagonalSelectionTarget_proved :
516 PRCRealDiagonalSelectionTarget :=
517 PRCRealDiagonalSelectionTarget_of_raw_diagonal_ledger
518 PRCRealRawDiagonalLedgerTarget_proved
519
520/-- The diagonal selection target is exactly the sharpened completeness target. -/
521theorem PRCRealCompletenessTarget_of_diagonal_selection
522 (hdiag : PRCRealDiagonalSelectionTarget) :
523 PRCRealCompletenessTarget := by
524 exact hdiag
525
526theorem PRCRealCompletenessTarget_proved :
527 PRCRealCompletenessTarget :=
528 PRCRealCompletenessTarget_of_diagonal_selection
529 PRCRealDiagonalSelectionTarget_proved
530
531/-- The full internal completeness theorem is now the concrete representative
532Cauchy-of-Cauchy diagonal target. -/
533theorem PRCRealCompletenessTarget_sharpened :
534 PRCRealCompletenessTarget = PRCRealCompletenessTarget := rfl
535
536/-- Step 10e certificate. It records the closed raw-ledger realization fact,
537the tail-selection diagonal, and the representative-completeness theorem for
538`PRCRealNullClosed`. -/
539structure PRCRealCompletenessSharpenedCertificate : Prop where
540 raw_cauchy_realization : PRCRawCauchyRealizationTarget
541 raw_cauchy_quotient_point : PRCRawCauchyQuotientPointTarget
542 diagonal_selection_from_raw_diagonal :
543 PRCRealRawDiagonalLedgerTarget → PRCRealDiagonalSelectionTarget
544 raw_diagonal_from_tail_selection :
545 PRCRealTailSelectionTarget → PRCRealRawDiagonalLedgerTarget
546 cofinal_tolerance_schedule : PRCRealCofinalToleranceScheduleTarget
547 three_leg_distance_modulus : PRCJCostDistanceThreeLegModulusTarget
548 finite_row_tail_selection : PRCRealFiniteRowTailSelectionTarget
549 finite_representative_tail_selection :
550 PRCRealFiniteRepresentativeTailSelectionTarget
551 finite_diagonal_schedule : PRCRealFiniteDiagonalScheduleTarget
552 tail_selection : PRCRealTailSelectionTarget
553 raw_diagonal : PRCRealRawDiagonalLedgerTarget
554 diagonal_selection : PRCRealDiagonalSelectionTarget
555 completeness_from_diagonal_selection :
556 PRCRealDiagonalSelectionTarget → PRCRealCompletenessTarget
557 completeness : PRCRealCompletenessTarget
558 completeness_target : PRCRealCompletenessTarget = PRCRealCompletenessTarget
559
560theorem prc_real_completeness_sharpened_certificate :
561 PRCRealCompletenessSharpenedCertificate where
562 raw_cauchy_realization := PRCRawCauchyRealizationTarget_proved
563 raw_cauchy_quotient_point := PRCRawCauchyQuotientPointTarget_proved
564 diagonal_selection_from_raw_diagonal :=
565 PRCRealDiagonalSelectionTarget_of_raw_diagonal_ledger
566 raw_diagonal_from_tail_selection :=
567 PRCRealRawDiagonalLedgerTarget_of_tail_selection
568 cofinal_tolerance_schedule :=
569 PRCRealCofinalToleranceScheduleTarget_proved
570 three_leg_distance_modulus :=
571 PRCJCostDistanceThreeLegModulusTarget_proved
572 finite_row_tail_selection :=
573 PRCRealFiniteRowTailSelectionTarget_proved
574 finite_representative_tail_selection :=
575 PRCRealFiniteRepresentativeTailSelectionTarget_proved
576 finite_diagonal_schedule :=
577 PRCRealFiniteDiagonalScheduleTarget_proved
578 tail_selection :=
579 PRCRealTailSelectionTarget_proved
580 raw_diagonal :=
581 PRCRealRawDiagonalLedgerTarget_proved
582 diagonal_selection :=
583 PRCRealDiagonalSelectionTarget_proved
584 completeness_from_diagonal_selection :=
585 PRCRealCompletenessTarget_of_diagonal_selection
586 completeness :=
587 PRCRealCompletenessTarget_proved
588 completeness_target := PRCRealCompletenessTarget_sharpened
589
590end PrimitiveRecognitionCalculus
591end Foundation
592end IndisputableMonolith
593