RootAlgorithm.lean

1 import RealizationBoundaries.RootConsequences
2 import Mathlib.Data.List.OfFn
3 
4 /-! # A finite arithmetic implementation of the normal-form root correction
5 
6 The executable input is a rational, a finite list of natural residue codes,
7 and an explicit Boolean selector oracle. List position n names prime VALUE n,
8 not the nth prime. Unused and nonprime positions carry no mathematical data.
9 The proof connects the finite implementation to the original ambient group.
10 -/
11 set_option autoImplicit false
12 namespace RealizationBoundaries
13 
14 def finiteCodeValue (d : List ℕ) (p : Prime) : Coordinate p :=
15   (d[p.val]?.getD 0 : Coordinate p)
16 
17 def oracleSection (a : Prime → Bool) (r : ℚ) (p : Prime) : Coordinate p :=
18   if a p then (r : Coordinate p) else 0
19 
20 def codedNormalValue (a : Prime → Bool) (r : ℚ) (d : List ℕ) : Ambient :=
21   fun p => oracleSection a r p + finiteCodeValue d p
22 
23 def rootCorrectionBound (r : ℚ) (d : List ℕ) (m : ℕ) : ℕ :=
24   max d.length (r.den * (r / m).den + 1)
25 
26 def rootCorrectionValue (a : Prime → Bool) (r : ℚ) (d : List ℕ)
27     (m : ℕ) (p : Prime) : Coordinate p :=
28   (m : Coordinate p)⁻¹ *
29     (codedNormalValue a r d p - (m : Coordinate p) * oracleSection a (r / m) p)
30 
31 /-- A finite loop. ZMod inversion is its computable extended-Euclidean implementation. -/
32 def rootCorrectionCode (a : Prime → Bool) (r : ℚ) (d : List ℕ) (m : ℕ) : List ℕ :=
33   List.ofFn fun i : Fin (rootCorrectionBound r d m) =>
34     if h : i.val.Prime then (rootCorrectionValue a r d m ⟨i.val, h⟩).val else 0
35 
36 @[simp] theorem rootCorrectionCode_length (a : Prime → Bool) (r : ℚ)
37     (d : List ℕ) (m : ℕ) :
38     (rootCorrectionCode a r d m).length = rootCorrectionBound r d m := by
39   simp [rootCorrectionCode]
40 
41 theorem finiteCodeValue_eq_zero (d : List ℕ) (p : Prime) (h : d.length ≤ p.val) :
42     finiteCodeValue d p = 0 := by
43   simp [finiteCodeValue, List.getElem?_eq_none h]
44 
45 theorem oracleSection_eq (a : Prime → Bool) (r : ℚ) :
46     oracleSection a r = rationalSection {p | a p = true} r := by
47   funext p
48   cases h : a p <;> simp [oracleSection, rationalSection, h]
49 
50 theorem codedNormalValue_mem (a : Prime → Bool) (r : ℚ) (d : List ℕ) :
51     codedNormalValue a r d ∈ selectorGroup {p | a p = true} := by
52   apply (selectorGroup _).add_mem
53   · exact (oracleSection_eq a r).symm ▸ rationalSection_mem _ r
54   · apply finiteSupport_le_preimage
55     apply (Set.finite_Iio d.length).preimage Subtype.val_injective.injOn |>.subset
56     intro p hp
57     by_contra hn
58     exact hp (finiteCodeValue_eq_zero d p (Nat.le_of_not_gt hn))
59 
60 /-- Outside the input support and the two denominator-prime sets the defect is zero. -/
61 theorem root_defect_zero_outside (a : Prime → Bool) (r : ℚ) (d : List ℕ)
62     {m : ℕ} (hm : 0 < m) (p : Prime)
63     (hd : d.length ≤ p.val) (hp : ¬ p.val ∣ r.den * (r / m).den) :
64     codedNormalValue a r d p - (m : Coordinate p) * oracleSection a (r / m) p = 0 := by
65   have ht : ((r / m).den : Coordinate p) ≠ 0 :=
66     (coordinate_cast_eq_zero _ p).not.mpr (fun h => hp (dvd_mul_of_dvd_right h _))
67   have he : (m : ℚ) * (r / m) = r := mul_div_cancel₀ r (Nat.cast_ne_zero.mpr hm.ne')
68   have hc : (r : Coordinate p) = (m : Coordinate p) * ((r / m : ℚ) : Coordinate p) := by
69     calc
70       _ = (((m : ℚ) * (r / m) : ℚ) : Coordinate p) := congrArg (fun q : ℚ => (q : Coordinate p)) he.symm
71       _ = _ := by rw [Rat.cast_mul_of_ne_zero (by simp) ht]; simp
72   cases hs : a p <;> simp [codedNormalValue, oracleSection, hs,
73     finiteCodeValue_eq_zero d p hd, hc]
74 
75 theorem rootCorrectionValue_zero_outside (a : Prime → Bool) (r : ℚ) (d : List ℕ)
76     {m : ℕ} (hm : 0 < m) (p : Prime) (hp : rootCorrectionBound r d m ≤ p.val) :
77     rootCorrectionValue a r d m p = 0 := by
78   have hd : d.length ≤ p.val := (le_max_left _ _).trans hp
79   have hden : ¬ p.val ∣ r.den * (r / m).den := by
80     intro h
81     have hle := Nat.le_of_dvd (Nat.mul_pos r.den_pos (r / m).den_pos) h
82     have hbound := (le_max_right d.length (r.den * (r / m).den + 1)).trans hp
83     omega
84   simp [rootCorrectionValue, root_defect_zero_outside a r d hm p hd hden]
85 
86 /-- Extraction correspondence for every prime of the infinite ambient product. -/
87 theorem rootCorrectionCode_exact (a : Prime → Bool) (r : ℚ) (d : List ℕ)
88     {m : ℕ} (hm : 0 < m) :
89     finiteCodeValue (rootCorrectionCode a r d m) = rootCorrectionValue a r d m := by
90   funext p
91   by_cases hp : p.val < rootCorrectionBound r d m
92   · simp [finiteCodeValue, rootCorrectionCode, hp, p.property]
93     rfl
94   · rw [finiteCodeValue_eq_zero _ p (by simpa using Nat.le_of_not_gt hp),
95       rootCorrectionValue_zero_outside a r d hm p (Nat.le_of_not_gt hp)]
96 
97 /-- The printed finite procedure produces a root of the original ambient value. -/
98 theorem finite_root_algorithm_correct (a : Prime → Bool) (r : ℚ) (d : List ℕ)
99     {m : ℕ} (hm : 0 < m)
100     (h : ∀ p : Prime, p.val ∣ m → codedNormalValue a r d p = 0) :
101     m • codedNormalValue a (r / m) (rootCorrectionCode a r d m) =
102       codedNormalValue a r d := by
103   funext p
104   rw [coordinate_nsmul]
105   change (m : Coordinate p) * (oracleSection a (r / m) p +
106     finiteCodeValue (rootCorrectionCode a r d m) p) = _
107   rw [congrFun (rootCorrectionCode_exact a r d hm) p]
108   by_cases hp : p.val ∣ m
109   · simp [(coordinate_cast_eq_zero m p).mpr hp, h p hp]
110   · have hn := (coordinate_cast_eq_zero m p).not.mpr hp
111     simp only [rootCorrectionValue, mul_add, mul_inv_cancel_left₀ hn]
112     exact add_sub_cancel _ _
113 
114 /-- Trial division and finitely many residue tests implement the obstruction test. -/
115 def finiteRootTest (a : Prime → Bool) (r : ℚ) (d : List ℕ) (m : ℕ) : Bool :=
116   (List.range (m + 1)).all fun n =>
117     if h : n.Prime then
118       if n ∣ m then decide (codedNormalValue a r d ⟨n, h⟩ = 0) else true
119     else true
120 
121 theorem finiteRootTest_exact (a : Prime → Bool) (r : ℚ) (d : List ℕ)
122     {m : ℕ} (hm : 0 < m) :
123     finiteRootTest a r d m = true ↔
124       ∀ p : Prime, p.val ∣ m → codedNormalValue a r d p = 0 := by
125   simp only [finiteRootTest, List.all_eq_true, List.mem_range]
126   constructor
127   · intro h p hp
128     rcases p with ⟨n, hn⟩
129     change n ∣ m at hp
130     have ht : (if h : n.Prime then if n ∣ m then decide (codedNormalValue a r d ⟨n, h⟩ = 0) else true else true) = true := h n (by have := Nat.le_of_dvd hm hp; omega)
131     simpa [hn, hp] using ht
132   · intro h n _
133     split_ifs with hn hd
134     · exact decide_eq_true (h ⟨n, hn⟩ hd)
135     · rfl
136     · rfl
137 
138 /-- None is a rejected root request; Some contains the rational and finite output. -/
139 def finiteRootSolver (a : Prime → Bool) (r : ℚ) (d : List ℕ) (m : ℕ) :
140     Option (ℚ × List ℕ) :=
141   if 0 < m ∧ finiteRootTest a r d m = true then
142     some (r / m, rootCorrectionCode a r d m)
143   else none
144 
145 theorem finiteRootSolver_some_iff (a : Prime → Bool) (r : ℚ) (d : List ℕ)
146     (m : ℕ) (t : ℚ) (e : List ℕ) :
147     finiteRootSolver a r d m = some (t, e) ↔
148       0 < m ∧ finiteRootTest a r d m = true ∧
149       t = r / m ∧ e = rootCorrectionCode a r d m := by
150   simp only [finiteRootSolver]
151   split_ifs with h
152   · simp only [Option.some.injEq, Prod.mk.injEq]
153     exact ⟨fun he => ⟨h.1, h.2, he.1.symm, he.2.symm⟩,
154       fun he => ⟨he.2.2.1.symm, he.2.2.2.symm⟩⟩
155   · simp only [false_iff]
156     rintro ⟨hm, ht, _, _⟩
157     exact h ⟨hm, ht⟩
158 
159 theorem finiteRootSolver_sound (a : Prime → Bool) (r : ℚ) (d : List ℕ)
160     (m : ℕ) (t : ℚ) (e : List ℕ) (h : finiteRootSolver a r d m = some (t, e)) :
161     m • codedNormalValue a t e = codedNormalValue a r d := by
162   obtain ⟨hm, ht, rfl, rfl⟩ := (finiteRootSolver_some_iff a r d m t e).mp h
163   exact finite_root_algorithm_correct a r d hm ((finiteRootTest_exact a r d hm).mp ht)
164 
165 /-- Rejection has a single prime coordinate as a mathematical certificate. -/
166 theorem finiteRootSolver_rejection_certificate (a : Prime → Bool) (r : ℚ)
167     (d : List ℕ) {m : ℕ} (hm : 0 < m)
168     (h : finiteRootSolver a r d m = none) :
169     ∃ p : Prime, p.val ∣ m ∧ codedNormalValue a r d p ≠ 0 := by
170   by_contra hn
171   have ht : finiteRootTest a r d m = true := (finiteRootTest_exact a r d hm).mpr (by
172     intro p hp
173     by_contra hnz
174     exact hn ⟨p, hp, hnz⟩)
175   simp [finiteRootSolver, hm, ht] at h
176 
177 /-- For positive multipliers rejection is equivalent to no root in the original group. -/
178 theorem finiteRootSolver_complete (a : Prime → Bool) (r : ℚ) (d : List ℕ)
179     {m : ℕ} (hm : 0 < m) :
180     (∃ t e, finiteRootSolver a r d m = some (t, e)) ↔
181       ∃ y : selectorGroup {p | a p = true},
182         m • y = ⟨codedNormalValue a r d, codedNormalValue_mem a r d⟩ := by
183   constructor
184   · rintro ⟨t, e, he⟩
185     exact ⟨⟨codedNormalValue a t e, codedNormalValue_mem a t e⟩,
186       Subtype.ext (finiteRootSolver_sound a r d m t e he)⟩
187   · intro hy
188     have hr := (preimage_root_iff _ hm _).mp hy
189     have ht := (finiteRootTest_exact a r d hm).mpr hr
190     exact ⟨r / m, rootCorrectionCode a r d m, by simp [finiteRootSolver, hm, ht]⟩
191 
192 /-- The finite output has no nonzero correction outside the printed support set. -/
193 theorem finiteRootSolver_support_bound (a : Prime → Bool) (r : ℚ) (d : List ℕ)
194     {m : ℕ} (hm : 0 < m) (p : Prime)
195     (hd : finiteCodeValue d p = 0) (hp : ¬ p.val ∣ r.den * (r / m).den) :
196     finiteCodeValue (rootCorrectionCode a r d m) p = 0 := by
197   rw [congrFun (rootCorrectionCode_exact a r d hm) p]
198   have he : (m : ℚ) * (r / m) = r := mul_div_cancel₀ r (Nat.cast_ne_zero.mpr hm.ne')
199   have ht : ((r / m).den : Coordinate p) ≠ 0 :=
200     (coordinate_cast_eq_zero _ p).not.mpr (fun h => hp (dvd_mul_of_dvd_right h _))
201   have hc : (r : Coordinate p) = (m : Coordinate p) * ((r / m : ℚ) : Coordinate p) := by
202     calc
203       _ = (((m : ℚ) * (r / m) : ℚ) : Coordinate p) := congrArg (fun q : ℚ => (q : Coordinate p)) he.symm
204       _ = _ := by rw [Rat.cast_mul_of_ne_zero (by simp) ht]; simp
205   cases hs : a p <;> simp [rootCorrectionValue, codedNormalValue, oracleSection, hs, hd, hc]
206 
207 /-- Every actual finite-support input admits a finite residue list. The existence
208 proof does not claim to extract a list from an arbitrary infinite function. -/
209 theorem finiteCodeValue_represents (x : finiteSupport) :
210     ∃ d : List ℕ, finiteCodeValue d = x.val := by
211   classical
212   let hf := x.property
213   let s := hf.toFinset
214   let N := s.sup Subtype.val + 1
215   let d : List ℕ := List.ofFn fun i : Fin N =>
216     if h : i.val.Prime then (x.val ⟨i.val, h⟩).val else 0
217   refine ⟨d, ?_⟩
218   funext p
219   by_cases hp : p.val < N
220   · simp only [finiteCodeValue, d, List.getElem?_ofFn, hp, dite_true, dite_eq_left p.property,
221       Option.getD_some, ZMod.natCast_zmod_val]
222     rfl
223   · have hx : x.val p = 0 := by
224       by_contra hn
225       have hmem : p ∈ s := (Set.Finite.mem_toFinset hf).mpr hn
226       have hle : p.val ≤ s.sup Subtype.val := Finset.le_sup hmem
227       have hlt : p.val < N := Nat.lt_succ_of_le hle
228       exact hp hlt
229     have hlen : d.length = N := by simp only [d, List.length_ofFn]
230     rw [finiteCodeValue_eq_zero d p (hlen.symm ▸ Nat.le_of_not_gt hp), hx]
231 
232 /-- Thus the finite engine covers every original selector-group normal form. -/
233 theorem codedNormalValue_represents (a : Prime → Bool)
234     (x : selectorGroup {p | a p = true}) :
235     ∃ r : ℚ, ∃ d : List ℕ, codedNormalValue a r d = x.val := by
236   obtain ⟨r, d, hd⟩ := normalForm_exists _ x
237   obtain ⟨code, hc⟩ := finiteCodeValue_represents d
238   refine ⟨r, code, ?_⟩
239   change oracleSection a r + finiteCodeValue code = x.val
240   rw [oracleSection_eq, hc, ← hd]
241 
242 def rootObstructs (a : Prime → Bool) (r : ℚ) (d : List ℕ) (m n : ℕ) : Bool :=
243   if h : n.Prime then decide (n ∣ m ∧ codedNormalValue a r d ⟨n, h⟩ ≠ 0)
244   else false
245 
246 /-- The implementation returns the first obstructing prime, not just a rejection flag. -/
247 def firstRootObstruction (a : Prime → Bool) (r : ℚ) (d : List ℕ) (m : ℕ) : Option ℕ :=
248   (List.range (m + 1)).find? (rootObstructs a r d m)
249 
250 theorem firstRootObstruction_spec (a : Prime → Bool) (r : ℚ) (d : List ℕ)
251     (m n : ℕ) (h : firstRootObstruction a r d m = some n) :
252     ∃ hp : n.Prime, n ∣ m ∧ codedNormalValue a r d ⟨n, hp⟩ ≠ 0 := by
253   have ht := List.find?_some h
254   by_cases hp : n.Prime
255   · exact ⟨hp, by simpa [rootObstructs, hp] using ht⟩
256   · simp [rootObstructs, hp] at ht
257 
258 theorem firstRootObstruction_none_iff (a : Prime → Bool) (r : ℚ) (d : List ℕ)
259     {m : ℕ} (hm : 0 < m) :
260     firstRootObstruction a r d m = none ↔
261       ∀ p : Prime, p.val ∣ m → codedNormalValue a r d p = 0 := by
262   rw [firstRootObstruction, List.find?_eq_none]
263   constructor
264   · intro h p hp
265     rcases p with ⟨n, hn⟩
266     change n ∣ m at hp
267     have hle := Nat.le_of_dvd hm hp
268     have ht := h n (List.mem_range.mpr (Nat.lt_succ_of_le hle))
269     simpa [rootObstructs, hn, hp] using ht
270   · intro h n _
271     by_cases hn : n.Prime
272     · by_cases hd : n ∣ m
273       · simpa [rootObstructs, hn, hd] using h ⟨n, hn⟩ hd
274       · simp [rootObstructs, hn, hd]
275     · simp [rootObstructs, hn]
276 
277 /-- The positive-multiplier certified routine: error p, or a rational/finite root. -/
278 def certifiedRootSolver (a : Prime → Bool) (r : ℚ) (d : List ℕ) (m : ℕ) :
279     Except ℕ (ℚ × List ℕ) :=
280   match firstRootObstruction a r d m with
281   | some p => .error p
282   | none => .ok (r / m, rootCorrectionCode a r d m)
283 
284 theorem certifiedRootSolver_error (a : Prime → Bool) (r : ℚ) (d : List ℕ)
285     (m n : ℕ) (h : certifiedRootSolver a r d m = .error n) :
286     ∃ hp : n.Prime, n ∣ m ∧ codedNormalValue a r d ⟨n, hp⟩ ≠ 0 := by
287   unfold certifiedRootSolver at h
288   split at h
289   next p hp =>
290     cases h
291     exact firstRootObstruction_spec a r d m n hp
292   next => cases h
293 
294 theorem certifiedRootSolver_ok (a : Prime → Bool) (r : ℚ) (d : List ℕ)
295     {m : ℕ} (hm : 0 < m) (t : ℚ) (e : List ℕ)
296     (h : certifiedRootSolver a r d m = .ok (t, e)) :
297     m • codedNormalValue a t e = codedNormalValue a r d := by
298   unfold certifiedRootSolver at h
299   split at h
300   next => cases h
301   next hn =>
302     cases h
303     exact finite_root_algorithm_correct a r d hm
304       ((firstRootObstruction_none_iff a r d hm).mp hn)
305 
306 end RealizationBoundaries

Back to source controls