IndisputableMonolith.Foundation.DeltaSpine.GoldenIntReal
IndisputableMonolith/Foundation/DeltaSpine/GoldenIntReal.lean · 347 lines · 26 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Foundation.DeltaSpine.GoldenInt
3import IndisputableMonolith.Foundation.DeltaSpine.CostUniqueness
4import IndisputableMonolith.Foundation.DeltaSpine.LadderRatioBounds
5import IndisputableMonolith.Foundation.PhiForcing
6import IndisputableMonolith.Cost
7
8/-!
9# GoldenIntReal: the display bridge from ℤ[φ] to ℝ
10
11**The sigma1 boundary module.** `DeltaSpine.GoldenInt` derives T6 (φ forced as
12the unique positive golden root) entirely inside ℤ[φ], with axiom closure
13`{propext, Quot.sound}` (sigma0 DELTA_FORCED). This module pays the continuum
14tax exactly once, at the display boundary: it evaluates ℤ[φ] into ℝ and shows
15the sigma0 structure maps onto the classical `PhiForcing` presentation.
16
17Contents:
18* `toReal : GoldenInt → ℝ`, the evaluation `a + b·φ ↦ a + b·φℝ`;
19* `toReal` is a ring embedding (additive, multiplicative via `φ² = φ + 1`,
20 injective via the irrationality descent `int_sq_eq_five_sq`);
21* `toReal phi = PhiForcing.φ`: the sigma0 φ is the classical φ;
22* `isPos_iff_toReal_pos`: the decidable integer sign predicate `IsPos` is
23 exactly real positivity — so the sigma0 trichotomy/uniqueness theorems are
24 about the real order, not a private surrogate;
25* `t6_bridge`: the unique positive golden root of the sigma0 derivation
26 evaluates to `(1 + √5)/2`.
27
28This module is honestly **sigma1 CHOICE** (`Real.sqrt`, `nlinarith` over ℝ).
29That is the point: the *derivation* is delta-forced; only the *display* into
30the continuum costs `Classical.choice`.
31-/
32
33namespace IndisputableMonolith
34namespace Foundation
35namespace DeltaSpine
36
37open GoldenInt
38
39/-- Evaluation of ℤ[φ] into ℝ: `⟨a, b⟩ ↦ a + b·φ`. -/
40noncomputable def toReal (x : GoldenInt) : ℝ :=
41 (x.a : ℝ) + (x.b : ℝ) * PhiForcing.φ
42
43@[simp] theorem toReal_zero : toReal 0 = 0 := by simp [toReal]
44
45@[simp] theorem toReal_one : toReal 1 = 1 := by simp [toReal]
46
47/-- The sigma0 φ evaluates to the classical golden ratio. -/
48@[simp] theorem toReal_phi : toReal GoldenInt.phi = PhiForcing.φ := by
49 simp [toReal, GoldenInt.phi]
50
51/-- The sigma0 conjugate root evaluates to `1 − φ = (1 − √5)/2`. -/
52@[simp] theorem toReal_psi : toReal GoldenInt.psi = 1 - PhiForcing.φ := by
53 simp [toReal, GoldenInt.psi]; ring
54
55theorem toReal_add (x y : GoldenInt) : toReal (x + y) = toReal x + toReal y := by
56 simp only [toReal, add_a, add_b]
57 push_cast
58 ring
59
60theorem toReal_neg (x : GoldenInt) : toReal (-x) = -toReal x := by
61 simp only [toReal, neg_a, neg_b]
62 push_cast
63 ring
64
65/-- Multiplicativity: the ℤ[φ] product law *is* multiplication in ℝ, because
66 `φ² = φ + 1` (`PhiForcing.phi_equation`). -/
67theorem toReal_mul (x y : GoldenInt) : toReal (x * y) = toReal x * toReal y := by
68 simp only [toReal, mul_a, mul_b]
69 push_cast
70 -- the ℤ[φ] product law is exactly multiplication in ℝ because φ² = φ + 1
71 linear_combination (-(x.b : ℝ) * (y.b : ℝ)) * PhiForcing.phi_equation
72
73/-- `toReal` kills only 0 — the irrationality of √5 again, imported from the
74 sigma0 descent lemma `int_sq_eq_five_sq`. -/
75theorem toReal_eq_zero_iff {x : GoldenInt} : toReal x = 0 ↔ x = 0 := by
76 constructor
77 · intro h
78 have hss : Real.sqrt 5 * Real.sqrt 5 = 5 := Real.mul_self_sqrt (by norm_num)
79 -- 2·toReal x = (2a + b) + b·√5
80 have h2 : ((2 * x.a + x.b : ℤ) : ℝ) + (x.b : ℝ) * Real.sqrt 5 = 0 := by
81 have hφ : PhiForcing.φ = (1 + Real.sqrt 5) / 2 := rfl
82 rw [toReal, hφ] at h
83 push_cast
84 linarith
85 have hs : ((2 * x.a + x.b : ℤ) : ℝ) = -(x.b : ℝ) * Real.sqrt 5 := by linarith
86 have hsqR : ((2 * x.a + x.b : ℤ) : ℝ) * ((2 * x.a + x.b : ℤ) : ℝ)
87 = 5 * ((x.b : ℝ) * (x.b : ℝ)) := by
88 rw [hs]
89 nlinarith [hss]
90 have hsqZ : (2 * x.a + x.b) * (2 * x.a + x.b) = 5 * (x.b * x.b) := by
91 exact_mod_cast hsqR
92 have hb : x.b = 0 := GoldenInt.int_sq_eq_five_sq hsqZ
93 have ha : x.a = 0 := by
94 have h2' := h2
95 rw [hb] at h2'
96 push_cast at h2'
97 have : (x.a : ℝ) = 0 := by linarith
98 exact_mod_cast this
99 ext
100 · rw [ha]; rfl
101 · rw [hb]; rfl
102 · rintro rfl
103 exact toReal_zero
104
105theorem toReal_injective : Function.Injective toReal := by
106 intro x y h
107 have hz : toReal (x + -y) = 0 := by
108 rw [toReal_add, toReal_neg, h]
109 ring
110 have hxy : x + -y = 0 := toReal_eq_zero_iff.mp hz
111 have : x = y := by
112 have := congrArg (· + y) hxy
113 simpa [add_assoc, add_comm, add_left_comm] using this
114 exact this
115
116/-- The pair predicate `PosPair s t` says exactly `0 < s + t·√5`. Forward
117 direction of the sign bridge. -/
118theorem posPair_real_pos {s t : ℤ} (h : PosPair s t) :
119 0 < (s : ℝ) + (t : ℝ) * Real.sqrt 5 := by
120 have hss : Real.sqrt 5 * Real.sqrt 5 = 5 := Real.mul_self_sqrt (by norm_num)
121 have hpos : 0 < Real.sqrt 5 := Real.sqrt_pos.mpr (by norm_num)
122 rcases h with ⟨hs, ht, hst⟩ | ⟨hs, ht, hq⟩ | ⟨hs, ht, hq⟩
123 · -- both nonnegative, one strictly positive
124 have hs' : (0 : ℝ) ≤ (s : ℝ) := by exact_mod_cast hs
125 have ht' : (0 : ℝ) ≤ (t : ℝ) := by exact_mod_cast ht
126 rcases hst with h' | h'
127 · have : (0 : ℝ) < (s : ℝ) := by exact_mod_cast h'
128 nlinarith
129 · have : (0 : ℝ) < (t : ℝ) := by exact_mod_cast h'
130 nlinarith
131 · -- s < 0 < t, dominated: s² < 5t²
132 have hs' : (s : ℝ) < 0 := by exact_mod_cast hs
133 have ht' : (0 : ℝ) < (t : ℝ) := by exact_mod_cast ht
134 have hq' : (s : ℝ) * (s : ℝ) < 5 * ((t : ℝ) * (t : ℝ)) := by exact_mod_cast hq
135 by_contra hle
136 push_neg at hle
137 have h1 : (t : ℝ) * Real.sqrt 5 ≤ -(s : ℝ) := by linarith
138 have h2 : (0 : ℝ) < (t : ℝ) * Real.sqrt 5 := mul_pos ht' hpos
139 nlinarith
140 · -- t < 0 < s, dominated: 5t² < s²
141 have hs' : (0 : ℝ) < (s : ℝ) := by exact_mod_cast hs
142 have ht' : (t : ℝ) < 0 := by exact_mod_cast ht
143 have hq' : 5 * ((t : ℝ) * (t : ℝ)) < (s : ℝ) * (s : ℝ) := by exact_mod_cast hq
144 by_contra hle
145 push_neg at hle
146 have h1 : (s : ℝ) ≤ -(t : ℝ) * Real.sqrt 5 := by linarith
147 have h2 : (0 : ℝ) < -(t : ℝ) * Real.sqrt 5 := by
148 apply mul_pos _ hpos
149 linarith
150 nlinarith
151
152/-- **The sign bridge**: the sigma0 decidable predicate `IsPos` is exactly real
153 positivity of the evaluation. Proved via the sigma0 trichotomy — the
154 forward direction is `posPair_real_pos`; the reverse uses exclusivity
155 (`isPos_not_neg`) so no real-side case analysis is ever needed. -/
156theorem isPos_iff_toReal_pos (x : GoldenInt) : IsPos x ↔ 0 < toReal x := by
157 have key : ∀ y : GoldenInt, IsPos y → 0 < toReal y := by
158 intro y hy
159 have h := posPair_real_pos hy
160 have hφ : PhiForcing.φ = (1 + Real.sqrt 5) / 2 := rfl
161 rw [toReal, hφ]
162 push_cast at h ⊢
163 linarith
164 constructor
165 · exact key x
166 · intro h
167 rcases isPos_trichotomy x with hp | hz | hn
168 · exact hp
169 · exfalso
170 rw [hz, toReal_zero] at h
171 exact lt_irrefl 0 h
172 · exfalso
173 have hneg := key (-x) hn
174 rw [toReal_neg] at hneg
175 linarith
176
177/-- **T6 display bridge**: the unique positive golden root delivered by the
178 sigma0 derivation is, under evaluation, the classical `(1 + √5)/2`. The
179 mathematical work (uniqueness, positivity, the two roots) was all done at
180 sigma0; this theorem only translates it. -/
181theorem t6_bridge :
182 toReal GoldenInt.phi = (1 + Real.sqrt 5) / 2 ∧
183 0 < toReal GoldenInt.phi ∧
184 toReal GoldenInt.phi * toReal GoldenInt.phi = toReal GoldenInt.phi + 1 := by
185 refine ⟨?_, ?_, ?_⟩
186 · rw [toReal_phi]; rfl
187 · exact (isPos_iff_toReal_pos GoldenInt.phi).mp GoldenInt.phi_isPos
188 · rw [← toReal_mul, GoldenInt.phi_sq, toReal_add, toReal_one]
189
190/-! ## T5 display bridge
191
192`DeltaSpine.CostUniqueness` derives the T5 cost-uniqueness content at sigma0:
193the trace sequence `traceZ n = φⁿ + φ⁻ⁿ` is the unique solution of the
194d'Alembert law with the forced initial conditions, and `Jdouble n = traceZ n − 2`
195is the unique solution of the discrete Recognition Composition Law. This
196section evaluates those objects into ℝ and shows they are exactly the
197classical presentation: `traceZ` is `2·cosh(n·log φ)` and `Jdouble` is
198`2·Jcost(φⁿ)` for the canonical cost `Jcost x = (x + x⁻¹)/2 − 1` of
199`Cost.FunctionalEquation`. Again: the forcing was done at sigma0; this is
200display only. -/
201
202theorem toReal_sub (x y : GoldenInt) : toReal (x - y) = toReal x - toReal y := by
203 rw [sub_eq_add_neg, toReal_add, toReal_neg]
204 ring
205
206theorem toReal_two : toReal 2 = 2 := by
207 have h : (2 : GoldenInt) = ⟨2, 0⟩ := by decide
208 rw [h]
209 show ((2 : ℤ) : ℝ) + ((0 : ℤ) : ℝ) * PhiForcing.φ = 2
210 push_cast
211 ring
212
213/-- The sigma0 inverse `phiInv = φ − 1` evaluates to the real `φ⁻¹`. -/
214theorem toReal_phiInv : toReal GoldenInt.phiInv = PhiForcing.φ⁻¹ := by
215 have h := toReal_mul GoldenInt.phi GoldenInt.phiInv
216 rw [GoldenInt.phi_mul_phiInv, toReal_one, toReal_phi] at h
217 exact eq_inv_of_mul_eq_one_right h.symm
218
219/-- The unit-group power ladder evaluates to real integer powers of φ. -/
220theorem toReal_phiZpow (n : ℤ) : toReal (phiZpow n) = PhiForcing.φ ^ n := by
221 have hφne : PhiForcing.φ ≠ 0 := ne_of_gt PhiForcing.phi_pos
222 induction n using Int.induction_on with
223 | zero => rw [phiZpow_zero, toReal_one, zpow_zero]
224 | succ k ih =>
225 have hstep : phiZpow ((k : ℤ) + 1) = phiZpow (k : ℤ) * GoldenInt.phi := by
226 rw [phiZpow_add, phiZpow_one]
227 rw [hstep, toReal_mul, ih, toReal_phi, ← zpow_add_one₀ hφne]
228 | pred k ih =>
229 have hstep : phiZpow (-(k : ℤ) - 1) = phiZpow (-(k : ℤ)) * GoldenInt.phiInv := by
230 have e : -(k : ℤ) - 1 = -(k : ℤ) + (-1) := by ring
231 rw [e, phiZpow_add, phiZpow_neg_one]
232 rw [hstep, toReal_mul, ih, toReal_phiInv, ← zpow_sub_one₀ hφne]
233
234/-- The sigma0 trace sequence is the classical two-sided power sum. -/
235theorem toReal_traceZ (n : ℤ) :
236 toReal (traceZ n) = PhiForcing.φ ^ n + PhiForcing.φ ^ (-n) := by
237 show toReal (phiZpow n + phiZpow (-n)) = _
238 rw [toReal_add, toReal_phiZpow, toReal_phiZpow]
239
240/-- **The cosh display**: `traceZ n` is `2·cosh(n·log φ)`. The d'Alembert
241 functional equation proved at sigma0 is the addition law of cosh. -/
242theorem traceZ_cosh (n : ℤ) :
243 toReal (traceZ n) = 2 * Real.cosh ((n : ℝ) * Real.log PhiForcing.φ) := by
244 have hzpow : ∀ m : ℤ, PhiForcing.φ ^ m
245 = Real.exp ((m : ℝ) * Real.log PhiForcing.φ) := by
246 intro m
247 rw [← Real.rpow_intCast PhiForcing.φ m,
248 Real.rpow_def_of_pos PhiForcing.phi_pos, mul_comm]
249 have e : ((-n : ℤ) : ℝ) * Real.log PhiForcing.φ
250 = -((n : ℝ) * Real.log PhiForcing.φ) := by
251 push_cast
252 ring
253 rw [toReal_traceZ, hzpow n, hzpow (-n), e, Real.cosh_eq]
254 ring
255
256/-- **The Jcost display**: the sigma0 doubled cost `Jdouble n` evaluates to
257 `2·Jcost(φⁿ)` for the canonical cost `Jcost x = (x + x⁻¹)/2 − 1`. The
258 discrete RCL proved at sigma0 is the composition law that forces `Jcost`
259 in `Cost.FunctionalEquation`. -/
260theorem jdouble_eq_jcost (n : ℤ) :
261 toReal (Jdouble n) = 2 * Cost.Jcost (PhiForcing.φ ^ n) := by
262 have hφne : PhiForcing.φ ≠ 0 := ne_of_gt PhiForcing.phi_pos
263 show toReal (traceZ n - 2) = _
264 rw [toReal_sub, toReal_traceZ, toReal_two, Cost.Jcost, zpow_neg]
265 ring
266
267/-- **T5 display bridge**, the capstone: the sigma0-forced cost ladder is,
268 under evaluation, exactly the classical J-cost on the φ-ladder together
269 with its cosh form. Everything with mathematical content (existence,
270 uniqueness, the composition law) was proved at sigma0 in
271 `DeltaSpine.CostUniqueness`; this theorem is pure translation. -/
272theorem t5_bridge :
273 (∀ n : ℤ, toReal (Jdouble n) = 2 * Cost.Jcost (PhiForcing.φ ^ n)) ∧
274 (∀ n : ℤ, toReal (traceZ n)
275 = 2 * Real.cosh ((n : ℝ) * Real.log PhiForcing.φ)) :=
276 ⟨jdouble_eq_jcost, traceZ_cosh⟩
277
278/-! ## Ladder-ratio bracket bridge
279
280`DeltaSpine.LadderRatioBounds` pins φ and the ladder rungs φ⁵, φ⁸ inside
281explicit rational intervals entirely at sigma0: the predicates `RatLt`/`RatGt`
282are decidable integer sign questions on ℤ[φ] and every bracket closes by
283kernel `decide`. This section is the sigma1 reading: those integer predicates
284mean exactly the real inequalities they claim (`RatLt p q x` with `q > 0` is
285`p/q < toReal x`, dually for `RatGt`), so the sigma0 brackets are genuine
286bounds on the classical golden ratio and its powers. -/
287
288/-- The bracket witness `q·x − p` evaluates to the real affine form. -/
289theorem toReal_ratWitness (p q : ℤ) (x : GoldenInt) :
290 toReal (ratWitness p q x) = (q : ℝ) * toReal x - (p : ℝ) := by
291 show ((q * x.a - p : ℤ) : ℝ) + ((q * x.b : ℤ) : ℝ) * PhiForcing.φ = _
292 rw [toReal]
293 push_cast
294 ring
295
296/-- The sigma0 predicate `RatLt p q x` (for `q > 0`) is the real inequality
297 `p/q < toReal x`. -/
298theorem ratLt_toReal {p q : ℤ} {x : GoldenInt} (hq : 0 < q) (h : RatLt p q x) :
299 (p : ℝ) / (q : ℝ) < toReal x := by
300 have hpos := (isPos_iff_toReal_pos _).mp h
301 rw [toReal_ratWitness] at hpos
302 have hq' : (0 : ℝ) < (q : ℝ) := by exact_mod_cast hq
303 rw [div_lt_iff₀ hq']
304 nlinarith
305
306/-- The sigma0 predicate `RatGt p q x` (for `q > 0`) is the real inequality
307 `toReal x < p/q`. -/
308theorem ratGt_toReal {p q : ℤ} {x : GoldenInt} (hq : 0 < q) (h : RatGt p q x) :
309 toReal x < (p : ℝ) / (q : ℝ) := by
310 have hpos := (isPos_iff_toReal_pos _).mp h
311 rw [toReal_ratWitness, toReal_neg] at hpos
312 have hq' : (0 : ℝ) < (q : ℝ) := by exact_mod_cast hq
313 rw [lt_div_iff₀ hq']
314 push_cast at hpos
315 nlinarith
316
317/-- The computable ℕ-ladder `phiPow` evaluates to real powers of φ. -/
318theorem toReal_phiPow (n : ℕ) : toReal (phiPow n) = PhiForcing.φ ^ n := by
319 rw [phiPow_eq_phiZpow, toReal_phiZpow, zpow_natCast]
320
321/-- **Ladder-ratio display bridge**: the sigma0 rational brackets on the
322 primitive forced ratio φ and the ladder rungs φ⁵, φ⁸ read, under
323 evaluation, as genuine real inequalities on the classical golden ratio.
324 The arithmetic was decided at sigma0 (`ladder_ratio_brackets`); this
325 theorem only translates it into ℝ. -/
326theorem ladder_ratio_real_brackets :
327 ((1618033 : ℝ) / 1000000 < PhiForcing.φ ∧
328 PhiForcing.φ < (1618034 : ℝ) / 1000000) ∧
329 ((1109 : ℝ) / 100 < PhiForcing.φ ^ (5 : ℕ) ∧
330 PhiForcing.φ ^ (5 : ℕ) < (1110 : ℝ) / 100) ∧
331 ((46978 : ℝ) / 1000 < PhiForcing.φ ^ (8 : ℕ) ∧
332 PhiForcing.φ ^ (8 : ℕ) < (46979 : ℝ) / 1000) := by
333 have h1 := ratLt_toReal (by norm_num) phi_lower
334 have h2 := ratGt_toReal (by norm_num) phi_upper
335 have h3 := ratLt_toReal (by norm_num) phi5_lower
336 have h4 := ratGt_toReal (by norm_num) phi5_upper
337 have h5 := ratLt_toReal (by norm_num) phi8_lower
338 have h6 := ratGt_toReal (by norm_num) phi8_upper
339 rw [toReal_phi] at h1 h2
340 rw [toReal_phiPow] at h3 h4 h5 h6
341 push_cast at h1 h2 h3 h4 h5 h6
342 exact ⟨⟨h1, h2⟩, ⟨h3, h4⟩, ⟨h5, h6⟩⟩
343
344end DeltaSpine
345end Foundation
346end IndisputableMonolith
347