IndisputableMonolith.Foundation.DeltaSpine.GoldenInt
IndisputableMonolith/Foundation/DeltaSpine/GoldenInt.lean · 413 lines · 43 declarations
show as:
view math explainer →
1import Mathlib
2
3/-!
4# GoldenInt: the delta-forced golden ring ℤ[φ]
5
6**The sigma0 (choice-free) re-derivation of the T6 golden-ratio forcing node.**
7
8The existing spine node `Foundation.PhiForcing` proves T6 over `ℝ` with
9`Real.sqrt 5`, and its axiom closure is `[propext, Classical.choice, Quot.sound]`:
10sigma1 (CHOICE) in the forcing-spectrum grading of `scripts/sigma_audit.py`.
11The choice dependency is pure carrier tax. Nothing in "x² = x + 1 has a unique
12positive solution and it is φ" needs the continuum.
13
14This module re-derives the same content over the ring ℤ[φ] = ℤ×ℤ with
15(a, b) ↦ a + b·φ and multiplication folded through φ² = φ + 1. Everything here
16is elementary integer arithmetic: the ring laws are `ring` over ℤ, the integral
17domain property reduces via the multiplicative norm N(a+bφ) = a² + ab − b² to
18the irrationality of √5, which is proved by strong-induction descent on ℕ.
19Positivity of a + b·φ is encoded as a decidable integer predicate on (2a+b, b)
20(the exact sign trichotomy of s + b√5), so "φ is the unique positive root" is
21stated and proved with no real numbers at all.
22
23**Tactic hygiene (measured, 2026-07-01).** The choice-free toolset was
24established by direct axiom probes: `ring` on ℤ, `decide`, `rcases`/`obtain`/
25`by_cases`, `Nat.strong_induction_on`, `Int.lt_trichotomy`, and `omega` *when
26the goal is a single atom or `False`* all close within `{propext, Quot.sound}`.
27Two tools are contaminated and are banned here: full `simp` (its default simp
28set reaches choice-tainted Mathlib lemmas; only `simp only [...]` over the
29component lemmas below is used) and `omega` on goals with logical structure
30(a disjunctive/implicative goal makes `omega` emit a `Classical.choice`-tainted
31proof term). Every case split below is therefore an explicit
32`Int.lt_trichotomy`/`rcases`, with `omega` used only to close atomic goals.
33
34**Verdict target: sigma0 DELTA_FORCED** — the axiom closure of every theorem
35here must be a subset of `{propext, Quot.sound}`. No `Classical.choice`.
36Audit with `scripts/sigma_audit.py` or `#print axioms t6_delta_forced`.
37
38The bridge back to the display continuum (`toReal`, `toReal phi = PhiForcing.φ`,
39`IsPos x ↔ 0 < toReal x`) lives in `DeltaSpine.GoldenIntReal`, which is honestly
40sigma1: the continuum tax is paid exactly once, at the display boundary, not in
41the derivation.
42
43Delta Forcing Spectrum program: `Delta_Forcing_Spectrum_20260626.tex`.
44-/
45
46namespace IndisputableMonolith
47namespace Foundation
48namespace DeltaSpine
49
50/-- The golden ring ℤ[φ]: pairs `(a, b)` representing `a + b·φ`, with the
51 multiplication law folded through `φ² = φ + 1`. -/
52@[ext]
53structure GoldenInt where
54 /-- integer part -/
55 a : ℤ
56 /-- φ-coefficient -/
57 b : ℤ
58deriving DecidableEq, Repr
59
60namespace GoldenInt
61
62instance : Zero GoldenInt := ⟨⟨0, 0⟩⟩
63instance : One GoldenInt := ⟨⟨1, 0⟩⟩
64
65/-- φ as an element of ℤ[φ]. -/
66def phi : GoldenInt := ⟨0, 1⟩
67
68/-- The conjugate root ψ = 1 − φ. -/
69def psi : GoldenInt := ⟨1, -1⟩
70
71instance : Add GoldenInt := ⟨fun x y => ⟨x.a + y.a, x.b + y.b⟩⟩
72instance : Neg GoldenInt := ⟨fun x => ⟨-x.a, -x.b⟩⟩
73
74/-- `(a₁ + b₁φ)(a₂ + b₂φ) = (a₁a₂ + b₁b₂) + (a₁b₂ + b₁a₂ + b₁b₂)φ`
75 using `φ² = φ + 1`. -/
76instance : Mul GoldenInt :=
77 ⟨fun x y => ⟨x.a * y.a + x.b * y.b, x.a * y.b + x.b * y.a + x.b * y.b⟩⟩
78
79@[simp] theorem zero_a : (0 : GoldenInt).a = 0 := rfl
80@[simp] theorem zero_b : (0 : GoldenInt).b = 0 := rfl
81@[simp] theorem one_a : (1 : GoldenInt).a = 1 := rfl
82@[simp] theorem one_b : (1 : GoldenInt).b = 0 := rfl
83@[simp] theorem phi_a : phi.a = 0 := rfl
84@[simp] theorem phi_b : phi.b = 1 := rfl
85@[simp] theorem psi_a : psi.a = 1 := rfl
86@[simp] theorem psi_b : psi.b = -1 := rfl
87@[simp] theorem add_a (x y : GoldenInt) : (x + y).a = x.a + y.a := rfl
88@[simp] theorem add_b (x y : GoldenInt) : (x + y).b = x.b + y.b := rfl
89@[simp] theorem neg_a (x : GoldenInt) : (-x).a = -x.a := rfl
90@[simp] theorem neg_b (x : GoldenInt) : (-x).b = -x.b := rfl
91@[simp] theorem mul_a (x y : GoldenInt) : (x * y).a = x.a * y.a + x.b * y.b := rfl
92@[simp] theorem mul_b (x y : GoldenInt) :
93 (x * y).b = x.a * y.b + x.b * y.a + x.b * y.b := rfl
94
95/-- The component-lemma simp set used everywhere below. Full `simp` is banned
96 in this module (choice contamination via the default simp set); every
97 rewrite goes through these `rfl`-lemmas plus `ring` over ℤ. -/
98macro "golden_simp" : tactic =>
99 `(tactic| simp only [zero_a, zero_b, one_a, one_b, phi_a, phi_b, psi_a, psi_b,
100 add_a, add_b, neg_a, neg_b, mul_a, mul_b])
101
102/-- ℤ[φ] is a commutative ring. Every law is componentwise `ring` over ℤ,
103 which is choice-free. -/
104instance : CommRing GoldenInt where
105 add_assoc x y z := by ext <;> golden_simp <;> ring
106 zero_add x := by ext <;> golden_simp <;> ring
107 add_zero x := by ext <;> golden_simp <;> ring
108 add_comm x y := by ext <;> golden_simp <;> ring
109 mul_assoc x y z := by ext <;> golden_simp <;> ring
110 one_mul x := by ext <;> golden_simp <;> ring
111 mul_one x := by ext <;> golden_simp <;> ring
112 left_distrib x y z := by ext <;> golden_simp <;> ring
113 right_distrib x y z := by ext <;> golden_simp <;> ring
114 mul_comm x y := by ext <;> golden_simp <;> ring
115 zero_mul x := by ext <;> golden_simp <;> ring
116 mul_zero x := by ext <;> golden_simp <;> ring
117 neg_add_cancel x := by ext <;> golden_simp <;> ring
118 nsmul := nsmulRec
119 zsmul := zsmulRec
120
121@[simp] theorem sub_a (x y : GoldenInt) : (x - y).a = x.a - y.a := by
122 show (x + -y).a = x.a - y.a
123 golden_simp
124 ring
125
126@[simp] theorem sub_b (x y : GoldenInt) : (x - y).b = x.b - y.b := by
127 show (x + -y).b = x.b - y.b
128 golden_simp
129 ring
130
131/-! ## The multiplicative norm and the integral-domain property -/
132
133/-- The field norm `N(a + bφ) = a² + ab − b²` (the product with the conjugate
134 `(a+b) − bφ`). -/
135def norm (x : GoldenInt) : ℤ := x.a * x.a + x.a * x.b - x.b * x.b
136
137@[simp] theorem norm_zero : norm 0 = 0 := by decide
138
139/-- The norm is multiplicative. Pure `ring` over ℤ. -/
140theorem norm_mul (x y : GoldenInt) : norm (x * y) = norm x * norm y := by
141 simp only [norm, mul_a, mul_b]
142 ring
143
144/-- 5 divides a square only through its root: five-way case split on `x % 5`
145 by `rcases` (not by an `omega` disjunction, which would be choice-tainted),
146 each residue killed by kernel `decide`. -/
147theorem five_dvd_of_five_dvd_sq (x : ℕ) (hx : 5 ∣ x * x) : 5 ∣ x := by
148 obtain ⟨c, hc⟩ := hx
149 have hmod : x % 5 * (x % 5) % 5 = 0 := by
150 rw [← Nat.mul_mod, hc]
151 omega
152 have hlt : x % 5 < 5 := Nat.mod_lt x (by decide)
153 rcases h5 : x % 5 with _ | _ | _ | _ | _ | r
154 · exact Nat.dvd_of_mod_eq_zero h5
155 · rw [h5] at hmod; exact absurd hmod (by decide)
156 · rw [h5] at hmod; exact absurd hmod (by decide)
157 · rw [h5] at hmod; exact absurd hmod (by decide)
158 · rw [h5] at hmod; exact absurd hmod (by decide)
159 · exfalso; rw [h5] at hlt; omega
160
161/-- **Irrationality of √5, ℕ-level, by descent**: no nonzero natural square is
162 five times a square. Strong induction; the only tools are `Nat.mul_mod`,
163 atomic `omega`, and `ring`-rearrangement, all choice-free. -/
164theorem sq_ne_five_sq : ∀ n m : ℕ, m * m = 5 * (n * n) → n = 0 := by
165 intro n
166 induction n using Nat.strong_induction_on with
167 | _ n ih =>
168 intro m h
169 by_cases hn : n = 0
170 · exact hn
171 · exfalso
172 have h5m : 5 ∣ m := five_dvd_of_five_dvd_sq m ⟨n * n, h⟩
173 obtain ⟨k, rfl⟩ := h5m
174 have h1 : n * n = 5 * (k * k) := by
175 have h' : 5 * (5 * (k * k)) = 5 * (n * n) := by
176 calc 5 * (5 * (k * k)) = 5 * k * (5 * k) := by ring
177 _ = 5 * (n * n) := h
178 omega
179 have h5n : 5 ∣ n := five_dvd_of_five_dvd_sq n ⟨k * k, h1⟩
180 obtain ⟨j, hj⟩ := h5n
181 have h2 : k * k = 5 * (j * j) := by
182 have h' : 5 * (5 * (j * j)) = 5 * (k * k) := by
183 calc 5 * (5 * (j * j)) = 5 * j * (5 * j) := by ring
184 _ = n * n := by rw [hj]
185 _ = 5 * (k * k) := h1
186 omega
187 have hjn : j < n := by omega
188 have hj0 : j = 0 := ih j hjn k h2
189 omega
190
191/-- Integer form: `s² = 5·b²` forces `b = 0`. -/
192theorem int_sq_eq_five_sq {s b : ℤ} (h : s * s = 5 * (b * b)) : b = 0 := by
193 have h1 : (s * s).natAbs = (5 * (b * b)).natAbs := by rw [h]
194 rw [Int.natAbs_mul, Int.natAbs_mul, Int.natAbs_mul] at h1
195 have h5 : (5 : ℤ).natAbs = 5 := rfl
196 rw [h5] at h1
197 exact Int.natAbs_eq_zero.mp (sq_ne_five_sq b.natAbs s.natAbs h1)
198
199/-- The norm vanishes only at 0. This is where the irrationality of √5 does
200 its work: `4·N(x) = (2a+b)² − 5b²`. -/
201theorem norm_eq_zero_iff {x : GoldenInt} : norm x = 0 ↔ x = 0 := by
202 constructor
203 · intro h
204 have key : (2 * x.a + x.b) * (2 * x.a + x.b) = 5 * (x.b * x.b) := by
205 have expand : (2 * x.a + x.b) * (2 * x.a + x.b)
206 = 4 * (x.a * x.a + x.a * x.b - x.b * x.b) + 5 * (x.b * x.b) := by ring
207 rw [expand, show x.a * x.a + x.a * x.b - x.b * x.b = norm x from rfl, h]
208 ring
209 have hb : x.b = 0 := int_sq_eq_five_sq key
210 have ha : x.a = 0 := by
211 have hx : x.a * x.a + x.a * x.b - x.b * x.b = 0 := h
212 rw [hb] at hx
213 -- hx : x.a * x.a + x.a * 0 - 0 * 0 = 0; `x.a * x.a` is an opaque atom,
214 -- the rest is linear, so `omega` stays in its choice-free atomic regime.
215 have hnorm : x.a * x.a = 0 := by omega
216 -- `Int.mul_eq_zero` is the choice-free route (the generic
217 -- `mul_self_eq_zero`/`mul_eq_zero` are Classical.choice-tainted).
218 rcases Int.mul_eq_zero.mp hnorm with h' | h' <;> exact h'
219 ext
220 · rw [ha]; rfl
221 · rw [hb]; rfl
222 · rintro rfl
223 exact norm_zero
224
225/-- **ℤ[φ] is an integral domain** (choice-free, via the multiplicative norm). -/
226theorem mul_eq_zero_iff {x y : GoldenInt} : x * y = 0 ↔ x = 0 ∨ y = 0 := by
227 constructor
228 · intro h
229 have hn : norm x * norm y = 0 := by rw [← norm_mul, h, norm_zero]
230 rcases Int.mul_eq_zero.mp hn with h' | h'
231 · exact Or.inl (norm_eq_zero_iff.mp h')
232 · exact Or.inr (norm_eq_zero_iff.mp h')
233 · rintro (rfl | rfl) <;> ext <;> golden_simp <;> ring
234
235/-! ## The golden equation and its exactly-two roots -/
236
237/-- φ satisfies the golden equation `x² = x + 1` — by kernel computation on
238 integer literals. -/
239theorem phi_sq : phi * phi = phi + 1 := by decide
240
241/-- ψ = 1 − φ also satisfies the golden equation. -/
242theorem psi_sq : psi * psi = psi + 1 := by decide
243
244/-- φ ≠ ψ. -/
245theorem phi_ne_psi : phi ≠ psi := by decide
246
247/-- The golden polynomial factors: `(x − φ)(x − ψ) = x² − x − 1`. -/
248theorem golden_factorization (x : GoldenInt) :
249 (x - phi) * (x - psi) = x * x - x - 1 := by
250 ext <;> simp only [sub_a, sub_b, mul_a, mul_b, phi_a, phi_b, psi_a, psi_b,
251 one_a, one_b] <;> ring
252
253/-- **The golden equation has exactly the two roots φ and ψ in ℤ[φ]**
254 (factorization + integral domain; no quadratic formula, no `Real.sqrt`). -/
255theorem golden_roots {x : GoldenInt} (h : x * x = x + 1) : x = phi ∨ x = psi := by
256 have hfac : (x - phi) * (x - psi) = 0 := by
257 rw [golden_factorization, h]
258 ring
259 rcases mul_eq_zero_iff.mp hfac with h' | h'
260 · exact Or.inl (sub_eq_zero.mp h')
261 · exact Or.inr (sub_eq_zero.mp h')
262
263/-! ## Decidable positivity
264
265`a + b·φ = (s + b·√5)/2` with `s = 2a + b`. The sign of `s + b·√5` is decided
266by integer comparisons alone, because `√5` is irrational (ties `s² = 5b²` are
267impossible for `b ≠ 0`). `IsPos` encodes the exact trichotomy. -/
268
269/-- Sign predicate for `s + t·√5 > 0`, stated entirely in ℤ. The three
270 disjuncts are: both components nonnegative and not both zero; `s < 0`
271 dominated by `t√5`; `t < 0` dominated by `s`. -/
272def PosPair (s t : ℤ) : Prop :=
273 (0 ≤ s ∧ 0 ≤ t ∧ (0 < s ∨ 0 < t)) ∨
274 (s < 0 ∧ 0 < t ∧ s * s < 5 * (t * t)) ∨
275 (0 < s ∧ t < 0 ∧ 5 * (t * t) < s * s)
276
277instance (s t : ℤ) : Decidable (PosPair s t) := by unfold PosPair; infer_instance
278
279/-- Constructive positivity of `a + b·φ = (s + b√5)/2` with `s = 2a + b`. -/
280def IsPos (x : GoldenInt) : Prop := PosPair (2 * x.a + x.b) x.b
281
282instance : DecidablePred IsPos := fun x => by unfold IsPos; infer_instance
283
284/-- φ is positive (kernel computation). -/
285theorem phi_isPos : IsPos phi := by decide
286
287/-- ψ = 1 − φ is not positive (kernel computation): its real value is
288 ≈ −0.618. -/
289theorem psi_not_isPos : ¬ IsPos psi := by decide
290
291/-- 0 is not positive (kernel computation). -/
292theorem zero_not_isPos : ¬ IsPos (0 : GoldenInt) := by decide
293
294/-- Trichotomy at the pair level: given that the tie `s² = 5t²` forces `t = 0`
295 (the irrationality of √5), one of `PosPair s t`, `(s,t) = 0`,
296 `PosPair (−s) (−t)` holds. The case split is explicit `Int.lt_trichotomy`
297 (choice-free); `omega` only ever closes atomic side goals. -/
298theorem posPair_trichotomy {s t : ℤ}
299 (hnotie : s * s = 5 * (t * t) → t = 0) :
300 PosPair s t ∨ (s = 0 ∧ t = 0) ∨ PosPair (-s) (-t) := by
301 unfold PosPair
302 have e1 : -s * -s = s * s := by ring
303 have e2 : -t * -t = t * t := by ring
304 rcases Int.lt_trichotomy s 0 with hs | hs | hs
305 · -- s < 0
306 rcases Int.lt_trichotomy t 0 with ht | ht | ht
307 · -- both negative: −x has both components positive
308 exact Or.inr (Or.inr (Or.inl ⟨by omega, by omega, Or.inl (by omega)⟩))
309 · -- t = 0, s < 0: −x nonneg with 0 < −s
310 exact Or.inr (Or.inr (Or.inl ⟨by omega, by omega, Or.inl (by omega)⟩))
311 · -- s < 0 < t: sign decided by s² vs 5t²
312 rcases Int.lt_trichotomy (s * s) (5 * (t * t)) with hq | hq | hq
313 · exact Or.inl (Or.inr (Or.inl ⟨hs, ht, hq⟩))
314 · exfalso; have ht0 := hnotie hq; omega
315 · refine Or.inr (Or.inr (Or.inr (Or.inr ⟨by omega, by omega, ?_⟩)))
316 rw [e1, e2]; exact hq
317 · -- s = 0
318 rcases Int.lt_trichotomy t 0 with ht | ht | ht
319 · exact Or.inr (Or.inr (Or.inl ⟨by omega, by omega, Or.inr (by omega)⟩))
320 · exact Or.inr (Or.inl ⟨hs, ht⟩)
321 · exact Or.inl (Or.inl ⟨by omega, by omega, Or.inr ht⟩)
322 · -- s > 0
323 rcases Int.lt_trichotomy t 0 with ht | ht | ht
324 · -- 0 < s, t < 0: sign decided by s² vs 5t²
325 rcases Int.lt_trichotomy (s * s) (5 * (t * t)) with hq | hq | hq
326 · refine Or.inr (Or.inr (Or.inr (Or.inl ⟨by omega, by omega, ?_⟩)))
327 rw [e1, e2]; exact hq
328 · exfalso; have ht0 := hnotie hq; omega
329 · exact Or.inl (Or.inr (Or.inr ⟨hs, ht, hq⟩))
330 · exact Or.inl (Or.inl ⟨by omega, by omega, Or.inl hs⟩)
331 · exact Or.inl (Or.inl ⟨by omega, by omega, Or.inl hs⟩)
332
333/-- Exclusivity at the pair level: `s + t√5` cannot be positive in both
334 directions. All nine hypothesis cases close with `omega` on `False`
335 (atomic; the products `s·s`, `t·t` are opaque atoms). -/
336theorem posPair_not_neg {s t : ℤ} (h : PosPair s t) : ¬ PosPair (-s) (-t) := by
337 intro hneg
338 unfold PosPair at h hneg
339 have e1 : -s * -s = s * s := by ring
340 have e2 : -t * -t = t * t := by ring
341 rw [e1, e2] at hneg
342 rcases h with ⟨h1, h2, h3 | h3⟩ | ⟨h1, h2, h3⟩ | ⟨h1, h2, h3⟩ <;>
343 rcases hneg with ⟨g1, g2, g3 | g3⟩ | ⟨g1, g2, g3⟩ | ⟨g1, g2, g3⟩ <;>
344 omega
345
346/-- Exactly one of `IsPos x`, `x = 0`, `IsPos (−x)` holds (the trichotomy
347 direction: at least one). The tie case `s² = 5b²` is excluded by the
348 descent lemma `int_sq_eq_five_sq`. -/
349theorem isPos_trichotomy (x : GoldenInt) : IsPos x ∨ x = 0 ∨ IsPos (-x) := by
350 have h := posPair_trichotomy (s := 2 * x.a + x.b) (t := x.b)
351 (fun htie => int_sq_eq_five_sq htie)
352 rcases h with h | h | h
353 · exact Or.inl h
354 · refine Or.inr (Or.inl ?_)
355 obtain ⟨h1, h2⟩ := h
356 have ha : x.a = 0 := by omega
357 ext
358 · rw [ha]; rfl
359 · rw [h2]; rfl
360 · refine Or.inr (Or.inr ?_)
361 show PosPair (2 * (-x).a + (-x).b) (-x).b
362 have harg : 2 * (-x).a + (-x).b = -(2 * x.a + x.b) := by
363 rw [neg_a, neg_b]; ring
364 rw [harg, show (-x).b = -x.b from rfl]
365 exact h
366
367/-- Positivity is exclusive with negativity: `IsPos x` and `IsPos (−x)` cannot
368 both hold. -/
369theorem isPos_not_neg {x : GoldenInt} (h : IsPos x) : ¬ IsPos (-x) := by
370 intro hneg
371 have hneg' : PosPair (-(2 * x.a + x.b)) (-x.b) := by
372 have harg : 2 * (-x).a + (-x).b = -(2 * x.a + x.b) := by
373 rw [neg_a, neg_b]; ring
374 have hh := hneg
375 unfold IsPos at hh
376 rwa [harg, show (-x).b = -x.b from rfl] at hh
377 exact posPair_not_neg h hneg'
378
379/-- A positive element is nonzero. -/
380theorem isPos_ne_zero {x : GoldenInt} (h : IsPos x) : x ≠ 0 := by
381 rintro rfl
382 exact zero_not_isPos h
383
384/-! ## The T6 forcing theorem, delta-forced -/
385
386/-- **T6, DELTA-FORCED (sigma0)**: in the golden ring ℤ[φ],
387
388 1. φ satisfies the golden self-similarity equation x² = x + 1;
389 2. φ is positive (in the decidable integer sign structure);
390 3. the golden equation has exactly the roots φ and ψ = 1 − φ;
391 4. φ is the *unique positive* root.
392
393 This is the content of `PhiForcing.phi_unique_self_similar` with the
394 continuum stripped away. Axiom closure target: `{propext, Quot.sound}` —
395 no `Classical.choice`, no `Real.sqrt`, no `nlinarith` over ℝ. The
396 irrationality of √5 (the actual mathematical content of "the golden ratio
397 is not rational") is carried by `sq_ne_five_sq`, a strong-induction
398 descent over ℕ. -/
399theorem t6_delta_forced :
400 (phi * phi = phi + 1) ∧
401 IsPos phi ∧
402 (∀ x : GoldenInt, x * x = x + 1 → x = phi ∨ x = psi) ∧
403 (∀ x : GoldenInt, x * x = x + 1 → IsPos x → x = phi) := by
404 refine ⟨phi_sq, phi_isPos, fun _ h => golden_roots h, fun x h hp => ?_⟩
405 rcases golden_roots h with rfl | rfl
406 · rfl
407 · exact absurd hp psi_not_isPos
408
409end GoldenInt
410end DeltaSpine
411end Foundation
412end IndisputableMonolith
413