CoupledGuardedMajorant.lean

1 import CoupledNormalization
2 
3 /-!
4 # Bounded contraction ladders and guarded reverse folds
5 
6 An exact rational algorithm specification for the valid-input arithmetic
7 core of `disk_majorant`. Step exhaustion and post-update size failures are
8 explicit errors. The first small-radius seed is not size-checked. Successful
9 returns refine the proved fuel majorant and hence certify actual functions.
10 This does not assert Python interpreter or library implementation correctness.
11 -/
12 
13 set_option autoImplicit false
14 set_option maxHeartbeats 2500000
15 noncomputable section
16 
17 namespace Komorebi.SpecialFunctions.Coupled.Scales
18 
19 inductive MajorantError where
20   | steps
21   | bits
22   deriving DecidableEq, Repr
23 
24 def majorantSeed (R : ℚ) : ℚ := R/(1-R^2)
25 def majorantStep (R B : ℚ) : ℚ := R*(1+B^2)
26 
27 inductive LadderTrace (Q : ℚ) : ℚ → List ℚ → ℚ → Prop where
28   | stop {R : ℚ} (small : R < 1) : LadderTrace Q R [] R
29   | step {R t : ℚ} {xs : List ℚ} (large : 1 ≤ R)
30       (child : LadderTrace Q (Q*R) xs t) : LadderTrace Q R (R::xs) t
31 
32 def buildLadder (Q : ℚ) : ℕ → ℚ → Except MajorantError (List ℚ × ℚ)
33   | 0, R => if R < 1 then .ok ([],R) else .error .steps
34   | n+1, R => if R < 1 then .ok ([],R) else
35       match buildLadder Q n (Q*R) with
36       | .error e => .error e
37       | .ok (xs,t) => .ok (R::xs,t)
38 
39 theorem ladder_terminal (Q R t : ℚ) (xs : List ℚ) (h : LadderTrace Q R xs t) :
40     t = Q^xs.length * R := by
41   induction h with
42   | stop => simp
43   | @step R t xs hlarge hchild ih =>
44     rw [ih, List.length_cons, pow_succ]
45     ring
46 
47 theorem ladder_terminal_small (Q R t : ℚ) (xs : List ℚ) (h : LadderTrace Q R xs t) : t < 1 := by
48   induction h with
49   | stop hs => exact hs
50   | step _ _ ih => exact ih
51 
52 theorem ladder_adequate (Q R t : ℚ) (xs : List ℚ) (h : LadderTrace Q R xs t) :
53     Q^xs.length * R < 1 := by
54   rw [← ladder_terminal Q R t xs h]
55   exact ladder_terminal_small Q R t xs h
56 
57 theorem ladder_fold_eq (Q R t : ℚ) (xs : List ℚ) (h : LadderTrace Q R xs t) :
58     xs.foldr majorantStep (majorantSeed t) = rationalDiskMajorant Q xs.length R := by
59   induction h with
60   | stop hs => rfl
61   | @step R t xs hlarge hchild ih =>
62     simp only [List.foldr_cons, List.length_cons, rationalDiskMajorant,
63       ite_eq_right (not_lt.mpr hlarge)]
64     rw [ih]
65     rfl
66 
67 theorem build_ladder_ok (Q R : ℚ) (fuel : ℕ) (xs : List ℚ) (t : ℚ)
68     (h : buildLadder Q fuel R = .ok (xs,t)) :
69     LadderTrace Q R xs t ∧ xs.length ≤ fuel := by
70   induction fuel generalizing R xs t with
71   | zero =>
72     by_cases hs : R < 1
73     · simp only [buildLadder, ite_eq_left hs, Except.ok.injEq, Prod.mk.injEq] at h
74       rcases h with ⟨rfl,rfl⟩
75       exact ⟨.stop hs, by simp⟩
76     · simp only [buildLadder, ite_eq_right hs] at h
77       cases h
78   | succ n ih =>
79     by_cases hs : R < 1
80     · simp only [buildLadder, ite_eq_left hs, Except.ok.injEq, Prod.mk.injEq] at h
81       rcases h with ⟨rfl,rfl⟩
82       exact ⟨.stop hs, by simp⟩
83     · simp only [buildLadder, ite_eq_right hs] at h
84       cases he : buildLadder Q n (Q*R) with
85       | error e => rw [he] at h; cases h
86       | ok pair =>
87         rcases pair with ⟨ys,u⟩
88         rw [he] at h
89         obtain ⟨ht,hl⟩ := ih (Q*R) ys u he
90         cases h
91         exact ⟨.step (le_of_not_gt hs) ht, by simpa using Nat.succ_le_succ hl⟩
92 
93 theorem build_ladder_of_trace (Q R t : ℚ) (xs : List ℚ) (h : LadderTrace Q R xs t)
94     (fuel : ℕ) (hl : xs.length ≤ fuel) : buildLadder Q fuel R = .ok (xs,t) := by
95   induction h generalizing fuel with
96   | stop hs => cases fuel <;> simp only [buildLadder, ite_eq_left hs]
97   | @step R t xs hlarge hchild ih =>
98     cases fuel with
99     | zero => simp at hl
100     | succ n =>
101       have hn : xs.length ≤ n := by simpa using hl
102       simp only [buildLadder, ite_eq_right (not_lt.mpr hlarge), ih n hn]
103 
104 theorem build_ladder_ok_iff (Q R : ℚ) (fuel : ℕ) (xs : List ℚ) (t : ℚ) :
105     buildLadder Q fuel R = .ok (xs,t) ↔ LadderTrace Q R xs t ∧ xs.length ≤ fuel :=
106   ⟨build_ladder_ok Q R fuel xs t, fun h => build_ladder_of_trace Q R t xs h.1 fuel h.2⟩
107 
108 theorem build_ladder_not_bits (Q R : ℚ) (fuel : ℕ) : buildLadder Q fuel R ≠ .error .bits := by
109   induction fuel generalizing R with
110   | zero => simp only [buildLadder]; split <;> simp
111   | succ n ih =>
112     simp only [buildLadder]
113     split
114     · simp
115     · cases he : buildLadder Q n (Q*R) with
116       | ok pair => simp
117       | error e =>
118         have hn := ih (Q*R)
119         rw [he] at hn
120         exact hn
121 
122 theorem build_ladder_exists_of_adequate (Q R : ℚ) (fuel : ℕ) (ht : Q^fuel*R < 1) :
123     ∃ xs t, buildLadder Q fuel R = .ok (xs,t) := by
124   induction fuel generalizing R with
125   | zero =>
126     have hR : R < 1 := by simpa using ht
127     exact ⟨[],R,by simp only [buildLadder,ite_eq_left hR]⟩
128   | succ n ih =>
129     by_cases hs : R < 1
130     · exact ⟨[],R,by simp [buildLadder,hs]⟩
131     · have hc : Q^n*(Q*R) < 1 := by simpa only [pow_succ, mul_assoc] using ht
132       obtain ⟨xs,t,he⟩ := ih (Q*R) hc
133       exact ⟨R::xs,t,by simp only [buildLadder,ite_eq_right hs,he]⟩
134 
135 def guardedFold (fits : ℚ → Bool) (seed : ℚ) : List ℚ → Except MajorantError ℚ
136   | [] => .ok seed
137   | R::xs => match guardedFold fits seed xs with
138       | .error e => .error e
139       | .ok B => if fits (majorantStep R B) then .ok (majorantStep R B) else .error .bits
140 
141 def FoldFits (fits : ℚ → Bool) (seed : ℚ) : List ℚ → Prop
142   | [] => True
143   | R::xs => FoldFits fits seed xs ∧ fits (majorantStep R (xs.foldr majorantStep seed)) = true
144 
145 theorem guarded_fold_not_steps (fits : ℚ → Bool) (seed : ℚ) (xs : List ℚ) :
146     guardedFold fits seed xs ≠ .error .steps := by
147   induction xs with
148   | nil => simp [guardedFold]
149   | cons R xs ih =>
150     simp only [guardedFold]
151     cases he : guardedFold fits seed xs with
152     | error e => rw [he] at ih; exact ih
153     | ok B => simp only; split <;> simp
154 
155 theorem guarded_fold_ok_iff (fits : ℚ → Bool) (seed B : ℚ) (xs : List ℚ) :
156     guardedFold fits seed xs = .ok B ↔ B = xs.foldr majorantStep seed ∧ FoldFits fits seed xs := by
157   induction xs generalizing B with
158   | nil => simp [guardedFold, FoldFits, eq_comm]
159   | cons R xs ih =>
160     cases he : guardedFold fits seed xs with
161     | error e =>
162       have hf : ¬FoldFits fits seed xs := by
163         intro hf
164         have hc := (ih (xs.foldr majorantStep seed)).mpr ⟨rfl,hf⟩
165         rw [he] at hc
166         cases hc
167       simp [guardedFold, he, FoldFits, hf]
168     | ok C =>
169       have hc := (ih C).mp he
170       rcases hc with ⟨rfl,hf⟩
171       simp only [guardedFold,he,List.foldr_cons,FoldFits]
172       cases hb : fits (majorantStep R (xs.foldr majorantStep seed)) <;> simp_all
173       exact eq_comm
174 
175 theorem guarded_fold_bits_iff (fits : ℚ → Bool) (seed : ℚ) (xs : List ℚ) :
176     guardedFold fits seed xs = .error .bits ↔ ¬FoldFits fits seed xs := by
177   constructor
178   · intro he hf
179     have ho := (guarded_fold_ok_iff fits seed (xs.foldr majorantStep seed) xs).mpr ⟨rfl,hf⟩
180     rw [he] at ho
181     cases ho
182   · intro hf
183     cases he : guardedFold fits seed xs with
184     | ok B => exact False.elim (hf ((guarded_fold_ok_iff fits seed B xs).mp he).2)
185     | error e =>
186       cases e with
187       | bits => rfl
188       | steps => exact False.elim (guarded_fold_not_steps fits seed xs he)
189 
190 def guardedMajorant (Q : ℚ) (maxSteps : ℕ) (fits : ℚ → Bool) (R : ℚ) : Except MajorantError ℚ :=
191   match buildLadder Q maxSteps R with
192   | .error e => .error e
193   | .ok (xs,t) => guardedFold fits (majorantSeed t) xs
194 
195 theorem guarded_majorant_success (Q R B : ℚ) (budget : ℕ) (fits : ℚ → Bool)
196     (h : guardedMajorant Q budget fits R = .ok B) :
197     ∃ xs t, LadderTrace Q R xs t ∧ xs.length ≤ budget ∧
198       FoldFits fits (majorantSeed t) xs ∧ B = rationalDiskMajorant Q xs.length R := by
199   cases he : buildLadder Q budget R with
200   | error e => simp only [guardedMajorant,he] at h; cases h
201   | ok pair =>
202     rcases pair with ⟨xs,t⟩
203     have ht := build_ladder_ok Q R budget xs t he
204     have hf := (guarded_fold_ok_iff fits (majorantSeed t) B xs).mp (by simpa [guardedMajorant,he] using h)
205     exact ⟨xs,t,ht.1,ht.2,hf.2,hf.1.trans (ladder_fold_eq Q R t xs ht.1)⟩
206 
207 theorem guarded_majorant_small (Q R : ℚ) (budget : ℕ) (fits : ℚ → Bool) (hs : R < 1) :
208     guardedMajorant Q budget fits R = .ok (majorantSeed R) := by
209   cases budget <;> simp [guardedMajorant,buildLadder,hs,guardedFold]
210 
211 theorem guarded_majorant_zero (Q : ℚ) (budget : ℕ) (fits : ℚ → Bool) :
212     guardedMajorant Q budget fits 0 = .ok 0 := by
213   simpa [majorantSeed] using guarded_majorant_small Q 0 budget fits (by norm_num)
214 
215 theorem guarded_majorant_no_steps (Q R : ℚ) (fits : ℚ → Bool) (hR : 1 ≤ R) :
216     guardedMajorant Q 0 fits R = .error .steps := by
217   simp only [guardedMajorant,buildLadder,ite_eq_right (not_lt.mpr hR)]
218 
219 theorem guarded_majorant_disk_bound (p : RationalScales) (hs : p.toReal.positive)
220     (hc : p.toReal.q < 1 ∧ p.toReal.r < 1 ∧ p.toReal.a < 1 ∧ p.toReal.b < 1)
221     (R B : ℚ) (hR : 0 ≤ R) (budget : ℕ) (fits : ℚ → Bool)
222     (h : guardedMajorant p.maxScale budget fits R = .ok B) (i : Fin 2)
223     (z : ℂ) (hz : ‖z‖ ≤ (R : ℝ)) : ‖p.toReal.complexComponent i z‖ ≤ (B : ℝ) := by
224   obtain ⟨xs,t,ht,_,_,hB⟩ := guarded_majorant_success p.maxScale R B budget fits h
225   rw [hB]
226   exact p.toReal.rational_disk_majorant_sound hs hc p.maxScale R
227     (rational_maxScale_cast p) hR xs.length (ladder_adequate _ _ _ _ ht) i hz
228 
229 theorem guarded_majorant_endpoint_enclosure (p : RationalScales) (hs : p.toReal.positive)
230     (hc : p.toReal.q < 1 ∧ p.toReal.r < 1 ∧ p.toReal.a < 1 ∧ p.toReal.b < 1)
231     (x S B : ℚ) (hx : 0 ≤ x) (hxS : x < S) (budget : ℕ) (fits : ℚ → Bool)
232     (h : guardedMajorant p.maxScale budget fits S = .ok B) (N : ℕ) (i : Fin 2) :
233     (p.arrayPolynomial i N x : ℝ) ≤ p.toReal.realComponent i (x : ℝ) ∧
234       p.toReal.realComponent i (x : ℝ) ≤ ((p.arrayPolynomial i N x+B*(x/S)^(2*N+3) : ℚ) : ℝ) := by
235   obtain ⟨xs,t,ht,_,_,hB⟩ := guarded_majorant_success p.maxScale S B budget fits h
236   rw [hB]
237   exact array_endpoint_enclosure p hs hc x S hx hxS xs.length (ladder_adequate _ _ _ _ ht) N i
238 
239 theorem guarded_majorant_step_failure (Q R : ℚ) (budget : ℕ) (fits : ℚ → Bool)
240     (h : buildLadder Q budget R = .error .steps) :
241     guardedMajorant Q budget fits R = .error .steps := by
242   simp only [guardedMajorant,h]
243 
244 theorem guarded_majorant_bit_failure (Q R t : ℚ) (budget : ℕ) (fits : ℚ → Bool)
245     (xs : List ℚ) (h : buildLadder Q budget R = .ok (xs,t))
246     (hf : ¬FoldFits fits (majorantSeed t) xs) :
247     guardedMajorant Q budget fits R = .error .bits := by
248   simp only [guardedMajorant,h]
249   exact (guarded_fold_bits_iff fits (majorantSeed t) xs).mpr hf
250 
251 /-- Mathematical binary width, including width zero for integer zero. -/
252 def integerWidth (n : ℕ) : ℕ := if n = 0 then 0 else n.log2+1
253 def rationalBitSize (B : ℚ) : ℕ := max (integerWidth B.num.natAbs) (integerWidth B.den)
254 def sizeFits (maxBits : ℕ) (B : ℚ) : Bool := decide (rationalBitSize B ≤ maxBits)
255 
256 theorem size_fits_iff (maxBits : ℕ) (B : ℚ) :
257     sizeFits maxBits B = true ↔ rationalBitSize B ≤ maxBits := by simp [sizeFits]
258 
259 inductive CheckedMajorantError where
260   | scales
261   | radius
262   | stepsInput
263   | bitsInput
264   | resource (e : MajorantError)
265   deriving DecidableEq, Repr
266 
267 def RationalScales.strictRational (p : RationalScales) : Prop :=
268   0 < p.q ∧ p.q < 1 ∧ 0 < p.r ∧ p.r < 1 ∧ 0 < p.a ∧ p.a < 1 ∧ 0 < p.b ∧ p.b < 1
269 
270 instance (p : RationalScales) : Decidable p.strictRational := by
271   unfold RationalScales.strictRational
272   infer_instance
273 
274 /-- None represents an invalid nonnegative exact-integer resource input.
275 This is an input abstraction, not a Python runtime type checker. -/
276 def checkedMajorant (p : RationalScales) (R : ℚ) (steps bits : Option ℕ) :
277     Except CheckedMajorantError ℚ :=
278   if ¬p.strictRational then .error .scales else
279   if R < 0 then .error .radius else
280   if R = 0 then .ok 0 else
281   match steps with
282   | none => .error .stepsInput
283   | some n => match bits with
284       | none => .error .bitsInput
285       | some 0 => .error .bitsInput
286       | some (m+1) => match guardedMajorant p.maxScale n (sizeFits (m+1)) R with
287           | .ok B => .ok B
288           | .error e => .error (.resource e)
289 
290 theorem checked_invalid_scales (p : RationalScales) (R : ℚ) (steps bits : Option ℕ)
291     (hp : ¬p.strictRational) : checkedMajorant p R steps bits = .error .scales := by
292   simp only [checkedMajorant,ite_eq_left hp]
293 
294 theorem checked_negative_radius (p : RationalScales) (R : ℚ) (steps bits : Option ℕ)
295     (hp : p.strictRational) (hR : R < 0) : checkedMajorant p R steps bits = .error .radius := by
296   simp only [checkedMajorant,ite_eq_right (not_not.mpr hp),ite_eq_left hR]
297 
298 theorem checked_zero_before_resources (p : RationalScales) (steps bits : Option ℕ)
299     (hp : p.strictRational) : checkedMajorant p 0 steps bits = .ok 0 := by
300   simp [checkedMajorant,hp]
301 
302 theorem checked_invalid_steps (p : RationalScales) (R : ℚ) (bits : Option ℕ)
303     (hp : p.strictRational) (hR : 0 < R) : checkedMajorant p R none bits = .error .stepsInput := by
304   simp [checkedMajorant,hp,not_lt.mpr hR.le,ne_of_gt hR]
305 
306 theorem checked_invalid_bits (p : RationalScales) (R : ℚ) (n : ℕ)
307     (hp : p.strictRational) (hR : 0 < R) :
308     checkedMajorant p R (some n) none = .error .bitsInput ∧
309       checkedMajorant p R (some n) (some 0) = .error .bitsInput := by
310   simp [checkedMajorant,hp,not_lt.mpr hR.le,ne_of_gt hR]
311 
312 theorem checked_valid_inputs (p : RationalScales) (R : ℚ) (n m : ℕ)
313     (hp : p.strictRational) (hR : 0 < R) :
314     checkedMajorant p R (some n) (some (m+1)) =
315       match guardedMajorant p.maxScale n (sizeFits (m+1)) R with
316       | .ok B => .ok B
317       | .error e => .error (.resource e) := by
318   simp only [checkedMajorant,ite_eq_right (not_not.mpr hp),
319     ite_eq_right (not_lt.mpr hR.le),ite_eq_right (ne_of_gt hR)]
320 
321 theorem checked_small_seed_unchecked (p : RationalScales) (R : ℚ) (n m : ℕ)
322     (hp : p.strictRational) (hR : 0 < R) (hs : R < 1) :
323     checkedMajorant p R (some n) (some (m+1)) = .ok (majorantSeed R) := by
324   rw [checked_valid_inputs p R n m hp hR,guarded_majorant_small p.maxScale R n (sizeFits (m+1)) hs]
325 
326 theorem checked_success_core (p : RationalScales) (R B : ℚ) (n m : ℕ)
327     (hp : p.strictRational) (hR : 0 < R)
328     (h : checkedMajorant p R (some n) (some (m+1)) = .ok B) :
329     guardedMajorant p.maxScale n (sizeFits (m+1)) R = .ok B := by
330   rw [checked_valid_inputs p R n m hp hR] at h
331   cases he : guardedMajorant p.maxScale n (sizeFits (m+1)) R with
332   | ok C => rw [he] at h; cases h; rfl
333   | error e => rw [he] at h; cases h
334 
335 theorem checked_endpoint_enclosure (p : RationalScales) (hs : p.toReal.positive)
336     (hc : p.toReal.q < 1 ∧ p.toReal.r < 1 ∧ p.toReal.a < 1 ∧ p.toReal.b < 1)
337     (hp : p.strictRational) (x S B : ℚ) (hx : 0 ≤ x) (hxS : x < S) (n m : ℕ)
338     (h : checkedMajorant p S (some n) (some (m+1)) = .ok B) (N : ℕ) (i : Fin 2) :
339     (p.arrayPolynomial i N x : ℝ) ≤ p.toReal.realComponent i (x : ℝ) ∧
340       p.toReal.realComponent i (x : ℝ) ≤ ((p.arrayPolynomial i N x+B*(x/S)^(2*N+3) : ℚ) : ℝ) := by
341   have hS : 0 < S := hx.trans_lt hxS
342   exact guarded_majorant_endpoint_enclosure p hs hc x S B hx hxS n (sizeFits (m+1))
343     (checked_success_core p S B n m hp hS h) N i
344 
345 end Komorebi.SpecialFunctions.Coupled.Scales

Back to source controls