CoupledFormal.lean

1 import Mathlib.Basic.Real.Basic
2 import Mathlib.Tactic.Ring
3 import Mathlib.Tactic.Linarith
4 import Mathlib.Tactic.Positivity
5 import Mathlib.Algebra.BigOperators.Fin
6 import Lean.Elab.Tactic.Omega
7 import Mathlib.Analysis.Complex.Basic
8 import Mathlib.Analysis.SpecificLimits.Normed
9 
10 /-!
11 # Coupled special functions: recurrence, local convergence, and parameter recovery
12 
13 Source: Special Functions, Appendix F (recurrence and local coefficient bounds)
14 and Appendix G (degree-seven parameter recovery and the exceptional surfaces).
15 The coordinate maps are linked to a recursively constructed infinite sequence.
16 All parameters in the inverse theorem are positive real numbers. The local
17 convergence theorem additionally assumes that every scale is at most one.
18 
19 This module does not assert entire continuation, the differential-equation
20 identification of the sums, or the Perron growth law. The precise claim map
21 and restart point are in `formalization/Block01/`.
22 -/
23 
24 set_option autoImplicit false
25 set_option maxHeartbeats 800000
26 
27 noncomputable section
28 
29 namespace Komorebi.SpecialFunctions.Coupled
30 
31 /-- Two weighted observations and the product recover a positive first coordinate,
32 provided the coefficient discriminant is nonzero. No root-selection oracle is used. -/
33 theorem positive_pair_recovery {p k u v x y X Y : ℝ}
34     (hk : k ≠ 0) (hx : 0 < x) (hX : 0 < X)
35     (hprod : x * y = X * Y)
36     (hlin : p * x + k * y = p * X + k * Y)
37     (hquad : u * x ^ 2 + v * y ^ 2 = u * X ^ 2 + v * Y ^ 2)
38     (hD : k ^ 2 * u - p ^ 2 * v ≠ 0) : x = X ∧ y = Y := by
39   have hfirst : x = X := by
40     by_contra hn
41     have hfactor : (x - X) * (p * X - k * y) = 0 := by
42       calc
43         _ = X * ((p * x + k * y) - (p * X + k * Y)) -
44             k * (x * y - X * Y) := by ring
45         _ = 0 := by rw [hlin, hprod]; ring
46     have hc1 : p * X = k * y :=
47       sub_eq_zero.mp ((mul_eq_zero.mp hfactor).resolve_left (sub_ne_zero.mpr hn))
48     have hc2 : p * x = k * Y := by linarith only [hlin, hc1]
49     have hc1sq := congrArg (fun t : ℝ => t ^ 2) hc1
50     have hc2sq := congrArg (fun t : ℝ => t ^ 2) hc2
51     have hs : k ^ 2 * (y ^ 2 - Y ^ 2) + p ^ 2 * (x ^ 2 - X ^ 2) = 0 := by
52       nlinarith only [hc1sq, hc2sq]
53     have hz : (k ^ 2 * u - p ^ 2 * v) * (x ^ 2 - X ^ 2) = 0 := by
54       calc
55         _ = k ^ 2 * ((u * x ^ 2 + v * y ^ 2) - (u * X ^ 2 + v * Y ^ 2)) -
56             v * (k ^ 2 * (y ^ 2 - Y ^ 2) + p ^ 2 * (x ^ 2 - X ^ 2)) := by ring
57         _ = 0 := by rw [hquad, hs]; ring
58     have hsq : x ^ 2 = X ^ 2 :=
59       sub_eq_zero.mp ((mul_eq_zero.mp hz).resolve_left hD)
60     have hdiff : (x - X) * (x + X) = 0 := by nlinarith only [hsq]
61     exact hn (sub_eq_zero.mp ((mul_eq_zero.mp hdiff).resolve_right (ne_of_gt (add_pos hx hX))))
62   refine ⟨hfirst, ?_⟩
63   apply mul_left_cancel₀ hk
64   rw [hfirst] at hlin
65   linarith only [hlin]
66 
67 structure Scales where
68   q : ℝ
69   r : ℝ
70   a : ℝ
71   b : ℝ
72 
73 namespace Scales
74 
75 def positive (s : Scales) : Prop := 0 < s.q ∧ 0 < s.r ∧ 0 < s.a ∧ 0 < s.b
76 
77 def p (s : Scales) : ℝ := s.q * s.r
78 
79 def k (s : Scales) : ℝ := s.a * s.b
80 
81 def u1 (s : Scales) : ℝ := s.p / 3
82 
83 def v1 (s : Scales) : ℝ := s.k / 3
84 
85 def u2 (s : Scales) : ℝ := s.p / 15 * (s.p * s.q ^ 2 + s.k * s.r ^ 2)
86 
87 def v2 (s : Scales) : ℝ := s.k / 15 * (s.p * s.a ^ 2 + s.k * s.b ^ 2)
88 
89 def u3 (s : Scales) : ℝ := s.p / 7 *
90   (s.q ^ 4 * s.u2 + s.p ^ 2 * s.u1 * s.v1 + s.r ^ 4 * s.v2)
91 
92 def v3 (s : Scales) : ℝ := s.k / 7 *
93   (s.a ^ 4 * s.u2 + s.k ^ 2 * s.u1 * s.v1 + s.b ^ 4 * s.v2)
94 
95 def defect (s : Scales) : ℝ := s.k ^ 2 * s.u2 - s.p ^ 2 * s.v2
96 
97 def sameJet (s t : Scales) : Prop :=
98   s.u1 = t.u1 ∧ s.v1 = t.v1 ∧ s.u2 = t.u2 ∧ s.v2 = t.v2 ∧ s.u3 = t.u3 ∧ s.v3 = t.v3
99 
100 theorem defect_factor (s : Scales) :
101     s.defect = (s.p * s.k * s.a * s.r / 15) *
102       (s.q ^ 2 - s.b ^ 2) * (s.q * s.b - s.a * s.r) := by
103   unfold defect u2 v2 p k
104   ring
105 
106 theorem defect_eq_zero_iff (s : Scales) (h : s.positive) :
107     s.defect = 0 ↔ s.q = s.b ∨ s.q * s.b = s.a * s.r := by
108   rcases h with ⟨hq, hr, ha, hb⟩
109   have hpk : s.p * s.k * s.a * s.r / 15 ≠ 0 := by
110     unfold p k
111     positivity
112   rw [defect_factor]
113   rw [mul_eq_zero, mul_eq_zero]
114   simp only [hpk, false_or, sub_eq_zero]
115   have heq : s.q ^ 2 = s.b ^ 2 ↔ s.q = s.b := by
116     constructor
117     · intro hs
118       have ht : (s.q - s.b) * (s.q + s.b) = 0 := by nlinarith only [hs]
119       exact sub_eq_zero.mp ((mul_eq_zero.mp ht).resolve_right (ne_of_gt (add_pos hq hb)))
120     · intro hs; rw [hs]
121   rw [heq]
122 
123 
124 /-- Equality of positive squares recovers the signed scale, not just its magnitude. -/
125 theorem positive_square_injective {x y : ℝ} (hx : 0 < x) (hy : 0 < y)
126     (h : x ^ 2 = y ^ 2) : x = y := by
127   have hf : (x - y) * (x + y) = 0 := by nlinarith only [h]
128   exact sub_eq_zero.mp ((mul_eq_zero.mp hf).resolve_right (ne_of_gt (add_pos hx hy)))
129 
130 /-- The algebraic inverse theorem corresponding to Appendix G.2.
131 This proves injectivity of the six-coefficient map on positive scales off D=0. -/
132 theorem seven_jet_injective {s t : Scales} (hs : s.positive) (ht : t.positive)
133     (hD : s.defect ≠ 0) (hj : s.sameJet t) : s = t := by
134   rcases hs with ⟨hq, hr, ha, hb⟩
135   rcases ht with ⟨tq, tr, ta, tb⟩
136   rcases hj with ⟨hu1, hv1, hu2, hv2, hu3, hv3⟩
137   have hp : s.p = t.p := by unfold u1 at hu1; linarith only [hu1]
138   have hk : s.k = t.k := by unfold v1 at hv1; linarith only [hv1]
139   have hp0 : s.p ≠ 0 := ne_of_gt (mul_pos hq hr)
140   have hk0 : s.k ≠ 0 := ne_of_gt (mul_pos ha hb)
141   have hl1 : s.p * s.q ^ 2 + s.k * s.r ^ 2 = s.p * t.q ^ 2 + s.k * t.r ^ 2 := by
142     have h := hu2
143     simp only [u2, ← hp, ← hk] at h
144     exact mul_left_cancel₀ (div_ne_zero hp0 (by norm_num)) h
145   have hl2 : s.p * s.a ^ 2 + s.k * s.b ^ 2 = s.p * t.a ^ 2 + s.k * t.b ^ 2 := by
146     have h := hv2
147     simp only [v2, ← hp, ← hk] at h
148     exact mul_left_cancel₀ (div_ne_zero hk0 (by norm_num)) h
149   have hquad1 : s.u2 * (s.q ^ 2) ^ 2 + s.v2 * (s.r ^ 2) ^ 2 =
150       s.u2 * (t.q ^ 2) ^ 2 + s.v2 * (t.r ^ 2) ^ 2 := by
151     have h := hu3
152     simp only [u3, ← hp, ← hu1, ← hv1, ← hu2, ← hv2] at h
153     have hc := mul_left_cancel₀ (div_ne_zero hp0 (by norm_num : (7 : ℝ) ≠ 0)) h
154     nlinarith only [hc]
155   have hquad2 : s.u2 * (s.a ^ 2) ^ 2 + s.v2 * (s.b ^ 2) ^ 2 =
156       s.u2 * (t.a ^ 2) ^ 2 + s.v2 * (t.b ^ 2) ^ 2 := by
157     have h := hv3
158     simp only [v3, ← hk, ← hu1, ← hv1, ← hu2, ← hv2] at h
159     have hc := mul_left_cancel₀ (div_ne_zero hk0 (by norm_num : (7 : ℝ) ≠ 0)) h
160     nlinarith only [hc]
161   have hprod1 : s.q ^ 2 * s.r ^ 2 = t.q ^ 2 * t.r ^ 2 := by
162     have h := congrArg (fun x : ℝ => x ^ 2) hp
163     unfold p at h
164     nlinarith only [h]
165   have hprod2 : s.a ^ 2 * s.b ^ 2 = t.a ^ 2 * t.b ^ 2 := by
166     have h := congrArg (fun x : ℝ => x ^ 2) hk
167     unfold k at h
168     nlinarith only [h]
169   have hrow1 := positive_pair_recovery hk0 (sq_pos_of_pos hq) (sq_pos_of_pos tq)
170     hprod1 hl1 hquad1 hD
171   have hrow2 := positive_pair_recovery hk0 (sq_pos_of_pos ha) (sq_pos_of_pos ta)
172     hprod2 hl2 hquad2 hD
173   have hqeq := positive_square_injective hq tq hrow1.1
174   have hreq := positive_square_injective hr tr hrow1.2
175   have haeq := positive_square_injective ha ta hrow2.1
176   have hbeq := positive_square_injective hb tb hrow2.2
177   cases s
178   cases t
179   simp_all
180 
181 
182 /-- The next odd coefficient: n indexes the previously available coefficients. -/
183 def nextCoefficient (x y : ℝ) (f : ℕ → ℝ × ℝ) (n : ℕ) : ℝ :=
184   (∑ i : Fin (n + 1), x ^ (2 * i.val + 1) * y ^ (2 * (n - i.val) + 1) *
185     (f i.val).1 * (f (n - i.val)).2) / (2 * (n : ℝ) + 3)
186 
187 /-- The simultaneous, uniquely determined infinite coefficient sequence.
188 The n-th pair multiplies z^(2*n+1). No convergence is included in this definition. -/
189 def coefficients (s : Scales) : ℕ → ℝ × ℝ
190   | 0 => (1, 1)
191   | n + 1 =>
192     ((∑ i : Fin (n + 1), s.q ^ (2 * i.val + 1) * s.r ^ (2 * (n - i.val) + 1) *
193       (coefficients s i.val).1 * (coefficients s (n - i.val)).2) / (2 * (n : ℝ) + 3),
194      (∑ i : Fin (n + 1), s.a ^ (2 * i.val + 1) * s.b ^ (2 * (n - i.val) + 1) *
195       (coefficients s i.val).1 * (coefficients s (n - i.val)).2) / (2 * (n : ℝ) + 3))
196 termination_by n => n
197 decreasing_by all_goals omega
198 
199 /-- Recurrence contract. It does not assume a particular formula for later coefficients. -/
200 def IsCoefficientSolution (s : Scales) (f : ℕ → ℝ × ℝ) : Prop :=
201   f 0 = (1, 1) ∧ ∀ n, f (n + 1) =
202     (nextCoefficient s.q s.r f n, nextCoefficient s.a s.b f n)
203 
204 theorem coefficients_solution (s : Scales) : s.IsCoefficientSolution s.coefficients := by
205   constructor
206   · rw [coefficients]
207   · intro n
208     rw [coefficients]
209     rfl
210 
211 theorem nextCoefficient_congr {x y : ℝ} {f g : ℕ → ℝ × ℝ} {n : ℕ}
212     (h : ∀ j, j ≤ n → f j = g j) : nextCoefficient x y f n = nextCoefficient x y g n := by
213   unfold nextCoefficient
214   congr 1
215   apply Finset.sum_congr rfl
216   intro i _
217   rw [h i.val (by omega), h (n - i.val) (Nat.sub_le _ _)]
218 
219 theorem coefficient_solution_unique {s : Scales} {f g : ℕ → ℝ × ℝ}
220     (hf : s.IsCoefficientSolution f) (hg : s.IsCoefficientSolution g) : f = g := by
221   funext n
222   induction n using Nat.strong_induction_on with
223   | h n ih =>
224     cases n with
225     | zero => exact hf.1.trans hg.1.symm
226     | succ n =>
227       rw [hf.2, hg.2]
228       have hl : ∀ j, j ≤ n → f j = g j := fun j hj => ih j (by omega)
229       rw [nextCoefficient_congr hl, nextCoefficient_congr hl]
230 
231 theorem coefficient_solution_exists_unique (s : Scales) : ∃! f, s.IsCoefficientSolution f := by
232   refine ⟨s.coefficients, s.coefficients_solution, ?_⟩
233   intro g hg
234   exact coefficient_solution_unique hg s.coefficients_solution
235 
236 theorem coefficients_zero (s : Scales) : s.coefficients 0 = (1, 1) := by rw [coefficients]
237 
238 theorem coefficients_one (s : Scales) : s.coefficients 1 = (s.u1, s.v1) := by
239   simp [coefficients, u1, v1, p, k]
240 
241 theorem coefficients_two (s : Scales) : s.coefficients 2 = (s.u2, s.v2) := by
242   rw [s.coefficients_solution.2]
243   simp [nextCoefficient, Fin.sum_univ_succ, coefficients_zero, coefficients_one,
244     u1, v1, u2, v2, p, k]
245   constructor <;> ring
246 
247 theorem coefficients_three (s : Scales) : s.coefficients 3 = (s.u3, s.v3) := by
248   rw [s.coefficients_solution.2]
249   simp [nextCoefficient, Fin.sum_univ_succ, coefficients_zero, coefficients_one, coefficients_two,
250     u1, v1, u2, v2, u3, v3, p, k]
251   constructor <;> ring
252 
253 theorem nextCoefficient_positive {x y : ℝ} {f : ℕ → ℝ × ℝ} {n : ℕ}
254     (hx : 0 < x) (hy : 0 < y)
255     (hf : ∀ j, j ≤ n → 0 < (f j).1 ∧ 0 < (f j).2) :
256     0 < nextCoefficient x y f n := by
257   unfold nextCoefficient
258   apply div_pos
259   · apply Finset.sum_pos
260     · intro i _
261       have hfi := (hf i.val (by omega)).1
262       have hfj := (hf (n - i.val) (Nat.sub_le _ _)).2
263       positivity
264     · exact Finset.univ_nonempty
265   · positivity
266 
267 theorem coefficients_positive (s : Scales) (hs : s.positive) (n : ℕ) :
268     0 < (s.coefficients n).1 ∧ 0 < (s.coefficients n).2 := by
269   induction n using Nat.strong_induction_on with
270   | h n ih =>
271     cases n with
272     | zero => rw [coefficients_zero]; norm_num
273     | succ n =>
274       rw [s.coefficients_solution.2]
275       have hl : ∀ j, j ≤ n → 0 < (s.coefficients j).1 ∧ 0 < (s.coefficients j).2 :=
276         fun j hj => ih j (by omega)
277       exact ⟨nextCoefficient_positive hs.1 hs.2.1 hl,
278         nextCoefficient_positive hs.2.2.1 hs.2.2.2 hl⟩
279 
280 
281 /-- Uniform coefficient bound for one recurrence step. -/
282 theorem nextCoefficient_le_geometric {x y : ℝ} {f : ℕ → ℝ × ℝ} {n : ℕ}
283     (hx : 0 < x) (hy : 0 < y) (hx1 : x ≤ 1) (hy1 : y ≤ 1)
284     (hf : ∀ j, j ≤ n → 0 ≤ (f j).1 ∧ (f j).1 ≤ (1 / 2 : ℝ) ^ j ∧
285       0 ≤ (f j).2 ∧ (f j).2 ≤ (1 / 2 : ℝ) ^ j) :
286     nextCoefficient x y f n ≤ (1 / 2 : ℝ) ^ (n + 1) := by
287   have hterm (i : Fin (n + 1)) :
288       x ^ (2 * i.val + 1) * y ^ (2 * (n - i.val) + 1) *
289         (f i.val).1 * (f (n - i.val)).2 ≤ (1 / 2 : ℝ) ^ n := by
290     have hi : i.val ≤ n := by omega
291     have hj : n - i.val ≤ n := Nat.sub_le _ _
292     have hp : x ^ (2 * i.val + 1) * y ^ (2 * (n - i.val) + 1) ≤ 1 := by
293       calc
294         _ ≤ (1 : ℝ) * 1 := mul_le_mul (pow_le_one₀ hx.le hx1)
295           (pow_le_one₀ hy.le hy1) (by positivity) (by norm_num)
296         _ = 1 := by norm_num
297     have hc : (f i.val).1 * (f (n - i.val)).2 ≤
298         (1 / 2 : ℝ) ^ i.val * (1 / 2 : ℝ) ^ (n - i.val) :=
299       mul_le_mul (hf i.val hi).2.1 (hf (n - i.val) hj).2.2.2
300         (hf (n - i.val) hj).2.2.1 (by positivity)
301     calc
302       _ = (x ^ (2 * i.val + 1) * y ^ (2 * (n - i.val) + 1)) *
303           ((f i.val).1 * (f (n - i.val)).2) := by ring
304       _ ≤ 1 * ((1 / 2 : ℝ) ^ i.val * (1 / 2 : ℝ) ^ (n - i.val)) :=
305         mul_le_mul hp hc (mul_nonneg (hf i.val hi).1 (hf (n - i.val) hj).2.2.1)
306           (by norm_num)
307       _ = (1 / 2 : ℝ) ^ n := by rw [one_mul, ← pow_add, Nat.add_sub_of_le hi]
308   have hsum : (∑ i : Fin (n + 1), x ^ (2 * i.val + 1) * y ^ (2 * (n - i.val) + 1) *
309       (f i.val).1 * (f (n - i.val)).2) ≤ ((n : ℝ) + 1) * (1 / 2 : ℝ) ^ n := by
310     calc
311       _ ≤ ∑ _i : Fin (n + 1), (1 / 2 : ℝ) ^ n :=
312         Finset.sum_le_sum (fun i _ => hterm i)
313       _ = ((n : ℝ) + 1) * (1 / 2 : ℝ) ^ n := by simp
314   unfold nextCoefficient
315   apply (div_le_iff₀ (by positivity : (0 : ℝ) < 2 * (n : ℝ) + 3)).2
316   rw [pow_succ]
317   have hnonneg : 0 ≤ (1 / 2 : ℝ) ^ n := by positivity
318   nlinarith only [hsum, hnonneg]
319 
320 /-- Both coefficient sequences have the common geometric majorant 2^(-n).
321 This is a coefficient estimate, not an entire-function assertion. -/
322 theorem coefficients_le_geometric (s : Scales) (hs : s.positive)
323     (hsmall : s.q ≤ 1 ∧ s.r ≤ 1 ∧ s.a ≤ 1 ∧ s.b ≤ 1) (n : ℕ) :
324     (s.coefficients n).1 ≤ (1 / 2 : ℝ) ^ n ∧
325       (s.coefficients n).2 ≤ (1 / 2 : ℝ) ^ n := by
326   induction n using Nat.strong_induction_on with
327   | h n ih =>
328     cases n with
329     | zero => rw [coefficients_zero]; norm_num
330     | succ n =>
331       have hl : ∀ j, j ≤ n → 0 ≤ (s.coefficients j).1 ∧
332           (s.coefficients j).1 ≤ (1 / 2 : ℝ) ^ j ∧
333           0 ≤ (s.coefficients j).2 ∧ (s.coefficients j).2 ≤ (1 / 2 : ℝ) ^ j := by
334         intro j hj
335         exact ⟨(s.coefficients_positive hs j).1.le, (ih j (by omega)).1,
336           (s.coefficients_positive hs j).2.le, (ih j (by omega)).2⟩
337       rw [s.coefficients_solution.2]
338       exact ⟨nextCoefficient_le_geometric hs.1 hs.2.1 hsmall.1 hsmall.2.1 hl,
339         nextCoefficient_le_geometric hs.2.2.1 hs.2.2.2 hsmall.2.2.1 hsmall.2.2.2 hl⟩
340 
341 
342 /-- The geometric bound controls the actual complex odd-series terms. -/
343 theorem odd_series_norm_bound {c : ℕ → ℝ}
344     (hc : ∀ n, 0 ≤ c n ∧ c n ≤ (1 / 2 : ℝ) ^ n) (z : ℂ) (n : ℕ) :
345     ‖(c n : ℂ) * z ^ (2 * n + 1)‖ ≤ ‖z‖ * (‖z‖ ^ 2 / 2) ^ n := by
346   rw [norm_mul, Complex.norm_of_nonneg (hc n).1, norm_pow]
347   calc
348     _ ≤ (1 / 2 : ℝ) ^ n * ‖z‖ ^ (2 * n + 1) :=
349       mul_le_mul_of_nonneg_right (hc n).2 (by positivity)
350     _ = ‖z‖ * (‖z‖ ^ 2 / 2) ^ n := by
351       simp only [pow_add, pow_one, pow_mul, div_pow, one_pow]
352       ring
353 
354 /-- Absolute convergence on the open disk norm(z)^2 < 2. -/
355 theorem odd_series_norm_summable {c : ℕ → ℝ}
356     (hc : ∀ n, 0 ≤ c n ∧ c n ≤ (1 / 2 : ℝ) ^ n)
357     (z : ℂ) (hz : ‖z‖ ^ 2 < 2) :
358     Summable (fun n => ‖(c n : ℂ) * z ^ (2 * n + 1)‖) := by
359   have hr0 : 0 ≤ ‖z‖ ^ 2 / 2 := by positivity
360   have hr1 : ‖z‖ ^ 2 / 2 < 1 := by linarith only [hz]
361   have hg := (summable_geometric_of_lt_one hr0 hr1).mul_left ‖z‖
362   exact Summable.of_nonneg_of_le (fun n => norm_nonneg _) (odd_series_norm_bound hc z) hg
363 
364 theorem odd_series_summable {c : ℕ → ℝ}
365     (hc : ∀ n, 0 ≤ c n ∧ c n ≤ (1 / 2 : ℝ) ^ n)
366     (z : ℂ) (hz : ‖z‖ ^ 2 < 2) :
367     Summable (fun n => (c n : ℂ) * z ^ (2 * n + 1)) :=
368   (odd_series_norm_summable hc z hz).of_norm
369 
370 /-- Both recurrence series converge absolutely on the stated disk.
371 This does not yet assert differentiability or continuation to the entire plane. -/
372 theorem coefficient_series_absolutely_convergent (s : Scales) (hs : s.positive)
373     (hsmall : s.q ≤ 1 ∧ s.r ≤ 1 ∧ s.a ≤ 1 ∧ s.b ≤ 1)
374     (z : ℂ) (hz : ‖z‖ ^ 2 < 2) :
375     Summable (fun n => ‖((s.coefficients n).1 : ℂ) * z ^ (2 * n + 1)‖) ∧
376     Summable (fun n => ‖((s.coefficients n).2 : ℂ) * z ^ (2 * n + 1)‖) := by
377   constructor
378   · apply odd_series_norm_summable _ z hz
379     intro n
380     exact ⟨(s.coefficients_positive hs n).1.le, (s.coefficients_le_geometric hs hsmall n).1⟩
381   · apply odd_series_norm_summable _ z hz
382     intro n
383     exact ⟨(s.coefficients_positive hs n).2.le, (s.coefficients_le_geometric hs hsmall n).2⟩
384 
385 
386 /-- An explicit certified truncation bound, beginning at coefficient index N. -/
387 theorem odd_series_tail_bound {c : ℕ → ℝ}
388     (hc : ∀ n, 0 ≤ c n ∧ c n ≤ (1 / 2 : ℝ) ^ n)
389     (z : ℂ) (hz : ‖z‖ ^ 2 < 2) (N : ℕ) :
390     ‖∑' n, (c (n + N) : ℂ) * z ^ (2 * (n + N) + 1)‖ ≤
391       ‖z‖ * (‖z‖ ^ 2 / 2) ^ N / (1 - ‖z‖ ^ 2 / 2) := by
392   let r : ℝ := ‖z‖ ^ 2 / 2
393   have hr0 : 0 ≤ r := by dsimp [r]; positivity
394   have hr1 : r < 1 := by dsimp [r]; linarith only [hz]
395   have hg : HasSum (fun n : ℕ => (‖z‖ * r ^ N) * r ^ n)
396       (‖z‖ * r ^ N / (1 - r)) := by
397     simpa only [div_eq_mul_inv] using
398       (hasSum_geometric_of_lt_one hr0 hr1).mul_left (‖z‖ * r ^ N)
399   have hbound (n : ℕ) : ‖(c (n + N) : ℂ) * z ^ (2 * (n + N) + 1)‖ ≤
400       (‖z‖ * r ^ N) * r ^ n := by
401     calc
402       _ ≤ ‖z‖ * r ^ (n + N) := odd_series_norm_bound hc z (n + N)
403       _ = _ := by rw [pow_add]; ring
404   have hf := Summable.of_norm_bounded hg.summable hbound
405   exact hf.hasSum.norm_le_of_bounded hg hbound
406 
407 /-- The explicit six-coordinate map is the actual jet of the infinite recurrence. -/
408 theorem sameJet_of_coefficients_eq {s t : Scales}
409     (h : ∀ n, 1 ≤ n → n ≤ 3 → s.coefficients n = t.coefficients n) : s.sameJet t := by
410   have h1 := h 1 (by omega) (by omega)
411   have h2 := h 2 (by omega) (by omega)
412   have h3 := h 3 (by omega) (by omega)
413   rw [coefficients_one, coefficients_one, Prod.mk.injEq] at h1
414   rw [coefficients_two, coefficients_two, Prod.mk.injEq] at h2
415   rw [coefficients_three, coefficients_three, Prod.mk.injEq] at h3
416   exact ⟨h1.1, h1.2, h2.1, h2.2, h3.1, h3.2⟩
417 
418 /-- Parameter recovery directly from finite observations of the recurrence. -/
419 theorem parameters_of_jet_through_degree_seven {s t : Scales} (hs : s.positive) (ht : t.positive)
420     (hD : s.defect ≠ 0)
421     (h : ∀ n, 1 ≤ n → n ≤ 3 → s.coefficients n = t.coefficients n) : s = t :=
422   seven_jet_injective hs ht hD (sameJet_of_coefficients_eq h)
423 
424 /-- Generic injectivity of the full formal coefficient sequence. -/
425 theorem parameters_of_formal_pair_eq {s t : Scales} (hs : s.positive) (ht : t.positive)
426     (hD : s.defect ≠ 0) (h : s.coefficients = t.coefficients) : s = t := by
427   apply parameters_of_jet_through_degree_seven hs ht hD
428   intro n _ _
429   exact congrFun h n
430 
431 
432 /-- The nondegenerate rational example used in Appendix G. -/
433 def workedScales : Scales := ⟨1/5, 2/5, 3/5, 7/10⟩
434 
435 theorem workedScales_positive : workedScales.positive := by
436   norm_num [workedScales, positive]
437 
438 theorem workedScales_defect : workedScales.defect = 189 / 7812500 := by
439   norm_num [workedScales, defect, u2, v2, p, k]
440 
441 theorem workedScales_recoverable {s : Scales} (hs : s.positive)
442     (h : workedScales.sameJet s) : s = workedScales := by
443   have hD : workedScales.defect ≠ 0 := by rw [workedScales_defect]; norm_num
444   exact (seven_jet_injective workedScales_positive hs hD h).symm
445 
446 /-- A genuine boundary collision demonstrates why the nonzero-defect guard matters. -/
447 def boundaryLeft : Scales := ⟨1/4, 1/2, 1/4, 1/2⟩
448 
449 def boundaryRight : Scales := ⟨1/2, 1/4, 1/2, 1/4⟩
450 
451 theorem boundary_collision : boundaryLeft.positive ∧ boundaryRight.positive ∧
452     boundaryLeft.defect = 0 ∧ boundaryLeft.sameJet boundaryRight ∧ boundaryLeft ≠ boundaryRight := by
453   constructor
454   · norm_num [boundaryLeft, positive]
455   constructor
456   · norm_num [boundaryRight, positive]
457   constructor
458   · norm_num [boundaryLeft, defect, u2, v2, p, k]
459   constructor
460   · norm_num [sameJet, boundaryLeft, boundaryRight, u1, v1, u2, v2, u3, v3, p, k]
461   · intro h
462     have hq := congrArg Scales.q h
463     norm_num [boundaryLeft, boundaryRight] at hq
464 
465 end Scales
466 end Komorebi.SpecialFunctions.Coupled

Back to source controls