IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaReal
IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/DeltaReal.lean · 484 lines · 40 declarations
show as:
view math explainer →
1/-
2 PrimitiveRecognitionCalculus/DeltaReal.lean
3
4 Phase 1 of the Delta-Native Analysis frontier: ℝδ.
5
6 A Delta-real is not a completed point on an uncountable continuum. It is a
7 lawful rational-interval refinement protocol: a rule that, at every finite
8 precision, returns a rational interval containing the intended quantity, with
9 width shrinking to zero and each interval nested inside the previous one.
10
11 This module builds that object directly over the rationals and proves:
12
13 * `value` : the unique real lying in every interval of a protocol;
14 * `value_mem` : the protocol's intervals all contain its value;
15 * `value_unique` : any real in every interval is the value (squeeze);
16 * `ObsEq` : observational equality = interval overlap at every
17 precision, proved equivalent to equal value;
18 * `ofRat` : the rational embedding, with `value (ofRat q) = q`;
19 * `add`, `neg`, `sub`: native protocol operations, with `value` a homomorphism;
20 * `value_surjective` : every real is the value of a (dyadic) protocol;
21 * `display_real_forgetful` : the headline. The classical real is the forgetful
22 value of a protocol; protocol-reals present ℝ faithfully
23 (ObsEq ⇔ equal value) and natively (operations are
24 interval rules, not relabelled reals), with ℚ embedded.
25
26 The honest separation: `DeltaReal` is the protocol interface used for analysis.
27 Its `value` in ℝ is the display. The classical completion (RealCompletion.lean)
28 is the separate completed object; this module does not need it.
29
30 No project-local axioms. No sorry.
31-/
32
33import Mathlib
34
35namespace IndisputableMonolith
36namespace Foundation
37namespace PrimitiveRecognitionCalculus
38namespace DeltaReal
39
40/-! ## Rational intervals -/
41
42/-- A closed rational interval. -/
43structure RatInterval where
44 lo : ℚ
45 hi : ℚ
46 le : lo ≤ hi
47
48namespace RatInterval
49
50/-- The rational width of an interval. -/
51def width (I : RatInterval) : ℚ := I.hi - I.lo
52
53theorem width_nonneg (I : RatInterval) : 0 ≤ I.width := by
54 have := I.le; unfold width; linarith
55
56/-- `I ⊆ J`: `J` contains `I`. -/
57def Subset (I J : RatInterval) : Prop := J.lo ≤ I.lo ∧ I.hi ≤ J.hi
58
59/-- Two intervals overlap when neither lies strictly to one side of the other. -/
60def Overlap (I J : RatInterval) : Prop := I.lo ≤ J.hi ∧ J.lo ≤ I.hi
61
62end RatInterval
63
64/-! ## Delta-reals as refinement protocols -/
65
66/-- A Delta-real: a nested family of rational intervals with width controlled by
67`1/(n+1)` at precision `n`. The intended quantity is the unique real common to
68all the intervals. -/
69structure Protocol where
70 approx : ℕ → RatInterval
71 nested : ∀ n, (approx (n + 1)).Subset (approx n)
72 width_bound : ∀ n, (approx n).width ≤ 1 / (n + 1)
73
74namespace Protocol
75
76/-- Lower endpoints as reals. -/
77def lo (x : Protocol) (n : ℕ) : ℝ := ((x.approx n).lo : ℝ)
78
79/-- Upper endpoints as reals. -/
80def hi (x : Protocol) (n : ℕ) : ℝ := ((x.approx n).hi : ℝ)
81
82theorem lo_le_hi (x : Protocol) (n : ℕ) : x.lo n ≤ x.hi n := by
83 have := (x.approx n).le; unfold lo hi; exact_mod_cast this
84
85theorem lo_mono (x : Protocol) : Monotone x.lo := by
86 apply monotone_nat_of_le_succ
87 intro n
88 have h := (x.nested n).1
89 unfold lo; exact_mod_cast h
90
91theorem hi_anti (x : Protocol) : Antitone x.hi := by
92 apply antitone_nat_of_succ_le
93 intro n
94 have h := (x.nested n).2
95 unfold hi; exact_mod_cast h
96
97/-- Any lower endpoint is below any upper endpoint. -/
98theorem lo_le_hi_cross (x : Protocol) (a b : ℕ) : x.lo a ≤ x.hi b := by
99 have h1 : x.lo a ≤ x.lo (max a b) := x.lo_mono (le_max_left a b)
100 have h2 : x.lo (max a b) ≤ x.hi (max a b) := x.lo_le_hi _
101 have h3 : x.hi (max a b) ≤ x.hi b := x.hi_anti (le_max_right a b)
102 linarith
103
104theorem bddAbove_lo (x : Protocol) : BddAbove (Set.range x.lo) := by
105 refine ⟨x.hi 0, ?_⟩
106 rintro y ⟨n, rfl⟩
107 exact x.lo_le_hi_cross n 0
108
109/-- The real value denoted by a protocol: the supremum of its lower endpoints,
110equivalently the unique real in every interval. -/
111noncomputable def value (x : Protocol) : ℝ := ⨆ n, x.lo n
112
113theorem lo_le_value (x : Protocol) (n : ℕ) : x.lo n ≤ x.value :=
114 le_ciSup x.bddAbove_lo n
115
116theorem value_le_hi (x : Protocol) (n : ℕ) : x.value ≤ x.hi n :=
117 ciSup_le (fun k => x.lo_le_hi_cross k n)
118
119/-- The value lies in every interval. -/
120theorem value_mem (x : Protocol) (n : ℕ) : x.lo n ≤ x.value ∧ x.value ≤ x.hi n :=
121 ⟨x.lo_le_value n, x.value_le_hi n⟩
122
123theorem width_real_bound (x : Protocol) (n : ℕ) : x.hi n - x.lo n ≤ 1 / (n + 1) := by
124 have h := x.width_bound n
125 unfold RatInterval.width at h
126 unfold lo hi
127 have : ((x.approx n).hi : ℝ) - ((x.approx n).lo : ℝ) = (((x.approx n).hi - (x.approx n).lo : ℚ) : ℝ) := by
128 push_cast; ring
129 rw [this]
130 have hc : (((x.approx n).hi - (x.approx n).lo : ℚ) : ℝ) ≤ ((1 / (n + 1) : ℚ) : ℝ) := by
131 exact_mod_cast h
132 refine hc.trans ?_
133 push_cast; rfl
134
135/-- A nonnegative real bounded by `1/(n+1)` for all `n` is zero. -/
136theorem tiny_le_zero {a : ℝ} (h0 : 0 ≤ a) (hsmall : ∀ n : ℕ, a ≤ 1 / (n + 1)) : a = 0 := by
137 by_contra hne
138 have hpos : 0 < a := lt_of_le_of_ne h0 (Ne.symm hne)
139 obtain ⟨n, hn⟩ := exists_nat_gt (1 / a)
140 have hnpos : (0 : ℝ) < n + 1 := by positivity
141 have : 1 / a < (n + 1 : ℝ) := lt_trans hn (by linarith)
142 have hcontra : 1 / (n + 1 : ℝ) < a := by
143 rw [div_lt_iff₀ hnpos]
144 rw [div_lt_iff₀ hpos] at this
145 linarith
146 exact absurd (hsmall n) (not_le.mpr hcontra)
147
148/-- Squeeze: any real in every interval equals the value. -/
149theorem value_unique (x : Protocol) (y : ℝ)
150 (hy : ∀ n, x.lo n ≤ y ∧ y ≤ x.hi n) : y = x.value := by
151 have hbound : ∀ n : ℕ, |y - x.value| ≤ 1 / (n + 1) := by
152 intro n
153 obtain ⟨h1l, h1r⟩ := hy n
154 obtain ⟨h2l, h2r⟩ := x.value_mem n
155 have hw := x.width_real_bound n
156 rw [abs_le]
157 constructor <;> linarith
158 have : |y - x.value| = 0 := tiny_le_zero (abs_nonneg _) hbound
159 have := abs_eq_zero.mp this
160 linarith
161
162/-! ## Observational equality -/
163
164/-- Observational equality: intervals overlap at every precision. -/
165def ObsEq (x y : Protocol) : Prop := ∀ n, (x.approx n).Overlap (y.approx n)
166
167/-- Observational equality is exactly equality of value. This is the central
168faithfulness statement: the protocol distinguishes two reals iff their values
169differ. -/
170theorem obsEq_iff_value (x y : Protocol) : ObsEq x y ↔ x.value = y.value := by
171 constructor
172 · intro h
173 have hbound : ∀ n : ℕ, |x.value - y.value| ≤ 2 * (1 / ((n : ℝ) + 1)) := by
174 intro n
175 obtain ⟨hxy, hyx⟩ := h n
176 obtain ⟨hxl, hxr⟩ := x.value_mem n
177 obtain ⟨hyl, hyr⟩ := y.value_mem n
178 have hxw := x.width_real_bound n
179 have hyw := y.width_real_bound n
180 have ov1 : x.lo n ≤ y.hi n := by unfold Protocol.lo Protocol.hi; exact_mod_cast hxy
181 have ov2 : y.lo n ≤ x.hi n := by unfold Protocol.lo Protocol.hi; exact_mod_cast hyx
182 rw [abs_le]
183 constructor <;> linarith
184 have : |x.value - y.value| = 0 := by
185 apply tiny_le_zero (abs_nonneg _)
186 intro n
187 have hb := hbound (2 * n + 1)
188 have heq : 2 * (1 / ((↑(2 * n + 1) : ℝ) + 1)) = 1 / ((n : ℝ) + 1) := by
189 have hne : (n : ℝ) + 1 ≠ 0 := by positivity
190 push_cast
191 field_simp
192 ring
193 rw [heq] at hb
194 exact hb
195 have := abs_eq_zero.mp this
196 linarith
197 · intro h n
198 have hx := x.value_mem n
199 have hy := y.value_mem n
200 rw [h] at hx
201 refine ⟨?_, ?_⟩
202 · -- (x.approx n).lo ≤ (y.approx n).hi
203 have : x.lo n ≤ y.hi n := le_trans hx.1 (y.value_le_hi n)
204 unfold Protocol.lo Protocol.hi at this; exact_mod_cast this
205 · -- (y.approx n).lo ≤ (x.approx n).hi
206 have h1 := hy.1 -- y.lo n ≤ y.value
207 have h2 := hx.2 -- y.value ≤ x.hi n
208 have : y.lo n ≤ x.hi n := by linarith
209 unfold Protocol.lo Protocol.hi at this; exact_mod_cast this
210
211theorem obsEq_refl (x : Protocol) : ObsEq x x := (obsEq_iff_value x x).mpr rfl
212
213theorem obsEq_symm {x y : Protocol} (h : ObsEq x y) : ObsEq y x :=
214 (obsEq_iff_value y x).mpr ((obsEq_iff_value x y).mp h).symm
215
216theorem obsEq_trans {x y z : Protocol} (hxy : ObsEq x y) (hyz : ObsEq y z) : ObsEq x z :=
217 (obsEq_iff_value x z).mpr (((obsEq_iff_value x y).mp hxy).trans ((obsEq_iff_value y z).mp hyz))
218
219/-- Observational equality as a `Setoid`. The quotient is the display real line. -/
220def obsSetoid : Setoid Protocol where
221 r := ObsEq
222 iseqv := ⟨obsEq_refl, obsEq_symm, obsEq_trans⟩
223
224/-! ## Rational embedding -/
225
226/-- The constant protocol at a rational. -/
227def ofRat (q : ℚ) : Protocol where
228 approx := fun _ => ⟨q, q, le_refl q⟩
229 nested := fun _ => ⟨le_refl q, le_refl q⟩
230 width_bound := fun n => by
231 unfold RatInterval.width
232 simp only [sub_self]
233 positivity
234
235@[simp] theorem value_ofRat (q : ℚ) : (ofRat q).value = (q : ℝ) := by
236 unfold value Protocol.lo ofRat
237 simp
238
239/-- The rational embedding is faithful: two rational protocols are observationally
240equal iff the rationals are equal. -/
241theorem ofRat_obsEq_iff (q r : ℚ) : ObsEq (ofRat q) (ofRat r) ↔ q = r := by
242 rw [obsEq_iff_value, value_ofRat, value_ofRat]
243 exact_mod_cast Iff.rfl
244
245/-! ## Native operations -/
246
247/-- Addition of protocols. At precision `n` it reads both operands at precision
248`2n+1`, so the combined width is again `≤ 1/(n+1)`. -/
249def add (x y : Protocol) : Protocol where
250 approx := fun n =>
251 let k := 2 * n + 1
252 ⟨(x.approx k).lo + (y.approx k).lo, (x.approx k).hi + (y.approx k).hi, by
253 have := (x.approx k).le; have := (y.approx k).le; linarith⟩
254 nested := fun n => by
255 refine ⟨?_, ?_⟩
256 · have hx : (x.approx (2 * n + 1)).lo ≤ (x.approx (2 * (n + 1) + 1)).lo := by
257 have : 2 * n + 1 ≤ 2 * (n + 1) + 1 := by omega
258 have hm := x.lo_mono this
259 unfold Protocol.lo at hm; exact_mod_cast hm
260 have hy : (y.approx (2 * n + 1)).lo ≤ (y.approx (2 * (n + 1) + 1)).lo := by
261 have : 2 * n + 1 ≤ 2 * (n + 1) + 1 := by omega
262 have hm := y.lo_mono this
263 unfold Protocol.lo at hm; exact_mod_cast hm
264 simp only; linarith
265 · have hx : (x.approx (2 * (n + 1) + 1)).hi ≤ (x.approx (2 * n + 1)).hi := by
266 have : 2 * n + 1 ≤ 2 * (n + 1) + 1 := by omega
267 have hm := x.hi_anti this
268 unfold Protocol.hi at hm; exact_mod_cast hm
269 have hy : (y.approx (2 * (n + 1) + 1)).hi ≤ (y.approx (2 * n + 1)).hi := by
270 have : 2 * n + 1 ≤ 2 * (n + 1) + 1 := by omega
271 have hm := y.hi_anti this
272 unfold Protocol.hi at hm; exact_mod_cast hm
273 simp only; linarith
274 width_bound := fun n => by
275 have hx := x.width_bound (2 * n + 1)
276 have hy := y.width_bound (2 * n + 1)
277 unfold RatInterval.width at hx hy ⊢
278 simp only
279 have hsum : (x.approx (2*n+1)).hi + (y.approx (2*n+1)).hi
280 - ((x.approx (2*n+1)).lo + (y.approx (2*n+1)).lo)
281 = ((x.approx (2*n+1)).hi - (x.approx (2*n+1)).lo)
282 + ((y.approx (2*n+1)).hi - (y.approx (2*n+1)).lo) := by ring
283 rw [hsum]
284 have hkey : (1 : ℚ) / (2 * n + 1 + 1) + 1 / (2 * n + 1 + 1) = 1 / (n + 1) := by
285 have hne : (n : ℚ) + 1 ≠ 0 := by positivity
286 field_simp; ring
287 calc ((x.approx (2*n+1)).hi - (x.approx (2*n+1)).lo)
288 + ((y.approx (2*n+1)).hi - (y.approx (2*n+1)).lo)
289 ≤ 1 / (2 * (n:ℚ) + 1 + 1) + 1 / (2 * (n:ℚ) + 1 + 1) := by
290 have hx' : ((x.approx (2*n+1)).hi - (x.approx (2*n+1)).lo) ≤ 1 / (2 * (n:ℚ) + 1 + 1) := by
291 have : ((2 * n + 1 : ℕ) : ℚ) + 1 = 2 * (n:ℚ) + 1 + 1 := by push_cast; ring
292 rw [← this]; exact hx
293 have hy' : ((y.approx (2*n+1)).hi - (y.approx (2*n+1)).lo) ≤ 1 / (2 * (n:ℚ) + 1 + 1) := by
294 have : ((2 * n + 1 : ℕ) : ℚ) + 1 = 2 * (n:ℚ) + 1 + 1 := by push_cast; ring
295 rw [← this]; exact hy
296 linarith
297 _ = 1 / (n + 1) := hkey
298
299theorem value_add (x y : Protocol) : (add x y).value = x.value + y.value := by
300 symm
301 apply value_unique
302 intro n
303 refine ⟨?_, ?_⟩
304 · show (add x y).lo n ≤ x.value + y.value
305 unfold Protocol.lo add
306 simp only
307 have hx := x.lo_le_value (2 * n + 1)
308 have hy := y.lo_le_value (2 * n + 1)
309 unfold Protocol.lo at hx hy
310 push_cast
311 linarith
312 · show x.value + y.value ≤ (add x y).hi n
313 unfold Protocol.hi add
314 simp only
315 have hx := x.value_le_hi (2 * n + 1)
316 have hy := y.value_le_hi (2 * n + 1)
317 unfold Protocol.hi at hx hy
318 push_cast
319 linarith
320
321/-- Negation of a protocol. -/
322def neg (x : Protocol) : Protocol where
323 approx := fun n => ⟨-(x.approx n).hi, -(x.approx n).lo, by have := (x.approx n).le; linarith⟩
324 nested := fun n => by
325 refine ⟨?_, ?_⟩
326 · have := (x.nested n).2; simp only; linarith
327 · have := (x.nested n).1; simp only; linarith
328 width_bound := fun n => by
329 have h := x.width_bound n
330 unfold RatInterval.width at h ⊢
331 simp only
332 linarith
333
334theorem value_neg (x : Protocol) : (neg x).value = -x.value := by
335 symm
336 apply value_unique
337 intro n
338 refine ⟨?_, ?_⟩
339 · show (neg x).lo n ≤ -x.value
340 unfold Protocol.lo neg
341 simp only
342 have := x.value_le_hi n
343 unfold Protocol.hi at this
344 push_cast; linarith
345 · show -x.value ≤ (neg x).hi n
346 unfold Protocol.hi neg
347 simp only
348 have := x.lo_le_value n
349 unfold Protocol.lo at this
350 push_cast; linarith
351
352/-- Subtraction. -/
353def sub (x y : Protocol) : Protocol := add x (neg y)
354
355theorem value_sub (x y : Protocol) : (sub x y).value = x.value - y.value := by
356 unfold sub
357 rw [value_add, value_neg]
358 ring
359
360/-! ## Surjectivity: every real is a protocol value -/
361
362/-- The doubling bound on dyadic floors: `⌊r·2ⁿ⁺¹⌋ ∈ {2⌊r·2ⁿ⌋, 2⌊r·2ⁿ⌋+1}`.
363This is exactly why the dyadic intervals are nested. -/
364theorem floor_double (r : ℝ) (n : ℕ) :
365 2 * ⌊r * 2 ^ n⌋ ≤ ⌊r * 2 ^ (n + 1)⌋ ∧ ⌊r * 2 ^ (n + 1)⌋ ≤ 2 * ⌊r * 2 ^ n⌋ + 1 := by
366 have hk : (⌊r * 2 ^ n⌋ : ℝ) ≤ r * 2 ^ n := Int.floor_le _
367 have hk1 : r * 2 ^ n < (⌊r * 2 ^ n⌋ : ℝ) + 1 := Int.lt_floor_add_one _
368 have hpow : r * 2 ^ (n + 1) = (r * 2 ^ n) * 2 := by rw [pow_succ]; ring
369 constructor
370 · apply Int.le_floor.mpr
371 push_cast
372 rw [hpow]; nlinarith [hk]
373 · have hlt : ⌊r * 2 ^ (n + 1)⌋ < 2 * ⌊r * 2 ^ n⌋ + 2 := by
374 apply Int.floor_lt.mpr
375 push_cast
376 rw [hpow]; nlinarith [hk1]
377 omega
378
379/-- The canonical dyadic protocol of a real: at precision `n` it returns the
380dyadic interval `[⌊r·2ⁿ⌋/2ⁿ, (⌊r·2ⁿ⌋+1)/2ⁿ]`. -/
381noncomputable def canonical (r : ℝ) : Protocol where
382 approx := fun n =>
383 ⟨(⌊r * 2 ^ n⌋ : ℚ) / 2 ^ n, ((⌊r * 2 ^ n⌋ : ℚ) + 1) / 2 ^ n, by
384 have h2 : (0 : ℚ) < 2 ^ n := by positivity
385 have hpos : (0 : ℚ) < 1 / 2 ^ n := by positivity
386 have heq : ((⌊r * 2 ^ n⌋ : ℚ) + 1) / 2 ^ n - (⌊r * 2 ^ n⌋ : ℚ) / 2 ^ n = 1 / 2 ^ n := by
387 rw [div_sub_div_same]; congr 1; ring
388 linarith⟩
389 nested := fun n => by
390 obtain ⟨hlow, hhigh⟩ := floor_double r n
391 have hq2 : (0 : ℚ) < 2 ^ n := by positivity
392 have hq2' : (0 : ℚ) < 2 ^ (n + 1) := by positivity
393 have hpowq : (2 : ℚ) ^ (n + 1) = 2 ^ n * 2 := by rw [pow_succ]
394 refine ⟨?_, ?_⟩
395 · -- (approx n).lo ≤ (approx (n+1)).lo
396 show (⌊r * 2 ^ n⌋ : ℚ) / 2 ^ n ≤ (⌊r * 2 ^ (n + 1)⌋ : ℚ) / 2 ^ (n + 1)
397 rw [div_le_div_iff₀ hq2 hq2', hpowq]
398 have hlowq : (2 * (⌊r * 2 ^ n⌋ : ℤ) : ℚ) ≤ ((⌊r * 2 ^ (n + 1)⌋ : ℤ) : ℚ) := by
399 exact_mod_cast hlow
400 push_cast at hlowq ⊢
401 nlinarith [hlowq, hq2]
402 · -- (approx (n+1)).hi ≤ (approx n).hi
403 show ((⌊r * 2 ^ (n + 1)⌋ : ℚ) + 1) / 2 ^ (n + 1) ≤ ((⌊r * 2 ^ n⌋ : ℚ) + 1) / 2 ^ n
404 rw [div_le_div_iff₀ hq2' hq2, hpowq]
405 have hhighq : ((⌊r * 2 ^ (n + 1)⌋ : ℤ) : ℚ) ≤ (2 * (⌊r * 2 ^ n⌋ : ℤ) + 1 : ℤ) := by
406 exact_mod_cast hhigh
407 push_cast at hhighq ⊢
408 nlinarith [hhighq, hq2]
409 width_bound := fun n => by
410 show ((⌊r * 2 ^ n⌋ : ℚ) + 1) / 2 ^ n - (⌊r * 2 ^ n⌋ : ℚ) / 2 ^ n ≤ 1 / (n + 1)
411 have hq2 : (0 : ℚ) < 2 ^ n := by positivity
412 have hw : ((⌊r * 2 ^ n⌋ : ℚ) + 1) / 2 ^ n - (⌊r * 2 ^ n⌋ : ℚ) / 2 ^ n = 1 / 2 ^ n := by
413 rw [div_sub_div_same]; congr 1; ring
414 rw [hw]
415 have hnat : ∀ m : ℕ, m + 1 ≤ 2 ^ m := by
416 intro m
417 induction m with
418 | zero => simp
419 | succ k ih =>
420 have h1 : (1 : ℕ) ≤ 2 ^ k := Nat.one_le_two_pow
421 have hpk : 2 ^ (k + 1) = 2 ^ k + 2 ^ k := by rw [pow_succ]; ring
422 omega
423 have hle : ((n : ℚ) + 1) ≤ 2 ^ n := by
424 have := hnat n
425 calc ((n : ℚ) + 1) = ((n + 1 : ℕ) : ℚ) := by push_cast; ring
426 _ ≤ ((2 ^ n : ℕ) : ℚ) := by exact_mod_cast this
427 _ = 2 ^ n := by push_cast; ring
428 have hnpos : (0 : ℚ) < (n : ℚ) + 1 := by positivity
429 rw [div_le_div_iff₀ hq2 hnpos]
430 linarith
431
432theorem value_canonical (r : ℝ) : (canonical r).value = r := by
433 symm
434 apply value_unique
435 intro n
436 have h2 : (0 : ℝ) < 2 ^ n := by positivity
437 have hflo : (⌊r * 2 ^ n⌋ : ℝ) ≤ r * 2 ^ n := Int.floor_le _
438 have hflo1 : r * 2 ^ n < (⌊r * 2 ^ n⌋ : ℝ) + 1 := Int.lt_floor_add_one _
439 constructor
440 · show (canonical r).lo n ≤ r
441 simp only [canonical, Protocol.lo]
442 push_cast
443 rw [div_le_iff₀ h2]
444 linarith
445 · show r ≤ (canonical r).hi n
446 simp only [canonical, Protocol.hi]
447 push_cast
448 rw [le_div_iff₀ h2]
449 linarith
450
451/-- `value` is surjective onto ℝ. -/
452theorem value_surjective : Function.Surjective Protocol.value :=
453 fun r => ⟨canonical r, value_canonical r⟩
454
455/-! ## The headline: classical ℝ is the forgetful display of ℝδ -/
456
457/-- **Phase 1 headline.** The classical real line is the forgetful value of a
458Delta-real protocol. Concretely:
459
4601. every real is the value of a protocol (`value_surjective`);
4612. the rational embedding `ofRat` has `value (ofRat q) = q`, so ℚ sits inside;
4623. observational equality of protocols is exactly equality of value
463 (`obsEq_iff_value`), so the presentation is faithful;
4644. the protocol operations are native interval rules whose value is a ring
465 homomorphism (`value_add`, `value_neg`, `value_sub`).
466
467So ℝ is not a primitive completed object here; it is recovered as the value
468display of refinement protocols, and nothing in analysis needs more than the
469protocol that produces rational data to any requested precision. -/
470theorem display_real_forgetful :
471 Function.Surjective Protocol.value
472 ∧ (∀ q : ℚ, (ofRat q).value = (q : ℝ))
473 ∧ (∀ x y : Protocol, ObsEq x y ↔ x.value = y.value)
474 ∧ (∀ x y : Protocol, (add x y).value = x.value + y.value)
475 ∧ (∀ x : Protocol, (neg x).value = -x.value)
476 ∧ (∀ x y : Protocol, (sub x y).value = x.value - y.value) :=
477 ⟨value_surjective, value_ofRat, obsEq_iff_value, value_add, value_neg, value_sub⟩
478
479end Protocol
480end DeltaReal
481end PrimitiveRecognitionCalculus
482end Foundation
483end IndisputableMonolith
484