RootAlgorithmCost.lean

1 import RealizationBoundaries.RootAlgorithm
2 
3 /-!
4 # Oracle traces for the executable finite root solver
5 
6 Every oracle read appends its prime to a finite trace. Erasing the traces gives
7 the original finite arithmetic routines. The bounds count oracle requests and
8 loop candidates, and do not assign unit bit-cost to rational arithmetic,
9 primality testing, integer division or modular inversion.
10 -/
11 set_option autoImplicit false
12 namespace RealizationBoundaries
13 
14 /-- One explicit oracle operation, recording its queried coordinate. -/
15 def tracedSelectorRead (a : Prime → Bool) (p : Prime) : Bool × List Prime :=
16   (a p, [p])
17 
18 def tracedOracleSection (a : Prime → Bool) (r : ℚ) (p : Prime) :
19     Coordinate p × List Prime :=
20   let q := tracedSelectorRead a p
21   (if q.1 then (r : Coordinate p) else 0, q.2)
22 
23 @[simp] theorem tracedOracleSection_erase (a : Prime → Bool) (r : ℚ) (p : Prime) :
24     (tracedOracleSection a r p).1 = oracleSection a r p := rfl
25 
26 @[simp] theorem tracedOracleSection_trace (a : Prime → Bool) (r : ℚ) (p : Prime) :
27     (tracedOracleSection a r p).2 = [p] := rfl
28 
29 /-- The two section evaluations in the original correction, with their actual reads. -/
30 def tracedRootCorrectionValue (a : Prime → Bool) (r : ℚ) (d : List ℕ)
31     (m : ℕ) (p : Prime) : Coordinate p × List Prime :=
32   let sr := tracedOracleSection a r p
33   let st := tracedOracleSection a (r / m) p
34   ((m : Coordinate p)⁻¹ * (sr.1 + finiteCodeValue d p - (m : Coordinate p) * st.1),
35     sr.2 ++ st.2)
36 
37 @[simp] theorem tracedRootCorrectionValue_erase (a : Prime → Bool) (r : ℚ)
38     (d : List ℕ) (m : ℕ) (p : Prime) :
39     (tracedRootCorrectionValue a r d m p).1 = rootCorrectionValue a r d m p := rfl
40 
41 @[simp] theorem tracedRootCorrectionValue_trace (a : Prime → Bool) (r : ℚ)
42     (d : List ℕ) (m : ℕ) (p : Prime) :
43     (tracedRootCorrectionValue a r d m p).2 = [p, p] := rfl
44 
45 /-- Single-pass sequencing: preserve each computed value and concatenate its trace. -/
46 def sequenceRootTrace {α : Type*} : List (α × List Prime) → List α × List Prime
47   | [] => ([], [])
48   | (x, t) :: xs =>
49     let tail := sequenceRootTrace xs
50     (x :: tail.1, t ++ tail.2)
51 
52 @[simp] theorem sequenceRootTrace_erase {α : Type*} (xs : List (α × List Prime)) :
53     (sequenceRootTrace xs).1 = xs.map Prod.fst := by
54   induction xs with
55   | nil => rfl
56   | cons x xs ih => cases x; simp [sequenceRootTrace, ih]
57 
58 theorem sequenceRootTrace_bound {α : Type*} (xs : List (α × List Prime))
59     (c : ℕ) (h : ∀ x ∈ xs, x.2.length ≤ c) :
60     (sequenceRootTrace xs).2.length ≤ c * xs.length := by
61   induction xs with
62   | nil => simp [sequenceRootTrace]
63   | cons x xs ih =>
64     have hx := h x (List.mem_cons_self)
65     have ht := ih (fun y hy => h y (List.mem_cons_of_mem _ hy))
66     cases x with
67     | mk v t =>
68       simp only [sequenceRootTrace, List.length_append, List.length_cons]
69       dsimp only at hx
70       rw [Nat.mul_add, Nat.mul_one]
71       omega
72 
73 def tracedRootCorrectionStep (a : Prime → Bool) (r : ℚ) (d : List ℕ)
74     (m n : ℕ) : ℕ × List Prime :=
75   if h : n.Prime then
76     let q := tracedRootCorrectionValue a r d m ⟨n, h⟩
77     (q.1.val, q.2)
78   else (0, [])
79 
80 def tracedRootCorrectionCode (a : Prime → Bool) (r : ℚ) (d : List ℕ) (m : ℕ) :
81     List ℕ × List Prime :=
82   sequenceRootTrace (List.ofFn fun i : Fin (rootCorrectionBound r d m) =>
83     tracedRootCorrectionStep a r d m i.val)
84 
85 theorem tracedRootCorrectionCode_erase (a : Prime → Bool) (r : ℚ)
86     (d : List ℕ) (m : ℕ) :
87     (tracedRootCorrectionCode a r d m).1 = rootCorrectionCode a r d m := by
88   simp only [tracedRootCorrectionCode, sequenceRootTrace_erase, List.map_ofFn]
89   congr 1
90   funext i
91   simp only [Function.comp_apply, tracedRootCorrectionStep]
92   split <;> rfl
93 
94 theorem tracedRootCorrectionCode_query_bound (a : Prime → Bool) (r : ℚ)
95     (d : List ℕ) (m : ℕ) :
96     (tracedRootCorrectionCode a r d m).2.length ≤ 2 * rootCorrectionBound r d m := by
97   have hb := sequenceRootTrace_bound
98     (List.ofFn fun i : Fin (rootCorrectionBound r d m) =>
99       tracedRootCorrectionStep a r d m i.val) 2 (by
100         intro x hx
101         obtain ⟨i, rfl⟩ := List.mem_ofFn.mp hx
102         simp only [tracedRootCorrectionStep]
103         split
104         · change ([_, _] : List Prime).length ≤ 2
105           exact Nat.le_refl 2
106         · exact Nat.zero_le 2)
107   simpa only [tracedRootCorrectionCode, List.length_ofFn] using hb
108 
109 /-- Search predicate evaluates the section only at prime divisors of the multiplier. -/
110 def tracedRootObstructs (a : Prime → Bool) (r : ℚ) (d : List ℕ)
111     (m n : ℕ) : Bool × List Prime :=
112   if h : n.Prime then
113     if n ∣ m then
114       let q := tracedOracleSection a r ⟨n, h⟩
115       (decide (q.1 + finiteCodeValue d ⟨n, h⟩ ≠ 0), q.2)
116     else (false, [])
117   else (false, [])
118 
119 @[simp] theorem tracedRootObstructs_erase (a : Prime → Bool) (r : ℚ)
120     (d : List ℕ) (m n : ℕ) :
121     (tracedRootObstructs a r d m n).1 = rootObstructs a r d m n := by
122   by_cases hp : n.Prime <;> by_cases hd : n ∣ m <;>
123     simp [tracedRootObstructs, rootObstructs, hp, hd, codedNormalValue,
124       tracedOracleSection, tracedSelectorRead, oracleSection]
125   exact decide_not
126 
127 @[simp] theorem tracedRootObstructs_query_bound (a : Prime → Bool) (r : ℚ)
128     (d : List ℕ) (m n : ℕ) :
129     (tracedRootObstructs a r d m n).2.length ≤ 1 := by
130   by_cases hp : n.Prime <;> by_cases hd : n ∣ m <;>
131     simp [tracedRootObstructs, hp, hd, tracedOracleSection, tracedSelectorRead]
132   exact Nat.le_refl 1
133 
134 /-- Short-circuit search: stop after the first successful predicate, retaining all reads. -/
135 def findRootTrace {α : Type*} (test : α → Bool × List Prime) :
136     List α → Option α × List Prime
137   | [] => (none, [])
138   | x :: xs =>
139     let q := test x
140     if q.1 then (some x, q.2)
141     else
142       let tail := findRootTrace test xs
143       (tail.1, q.2 ++ tail.2)
144 
145 @[simp] theorem findRootTrace_erase {α : Type*} (test : α → Bool × List Prime)
146     (xs : List α) :
147     (findRootTrace test xs).1 = xs.find? (fun x => (test x).1) := by
148   induction xs with
149   | nil => rfl
150   | cons x xs ih => simp only [findRootTrace, List.find?_cons]; split <;> simp_all
151 
152 theorem findRootTrace_bound {α : Type*} (test : α → Bool × List Prime)
153     (xs : List α) (c : ℕ) (h : ∀ x ∈ xs, (test x).2.length ≤ c) :
154     (findRootTrace test xs).2.length ≤ c * xs.length := by
155   induction xs with
156   | nil => simp [findRootTrace]
157   | cons x xs ih =>
158     have hx := h x (List.mem_cons_self)
159     have ht := ih (fun y hy => h y (List.mem_cons_of_mem _ hy))
160     simp only [findRootTrace, List.length_cons]
161     split
162     · change (test x).2.length ≤ c * (xs.length + 1)
163       rw [Nat.mul_add, Nat.mul_one]
164       omega
165     · simp only [List.length_append]
166       rw [Nat.mul_add, Nat.mul_one]
167       omega
168 
169 def tracedFirstRootObstruction (a : Prime → Bool) (r : ℚ) (d : List ℕ) (m : ℕ) :
170     Option ℕ × List Prime :=
171   findRootTrace (tracedRootObstructs a r d m) (List.range (m + 1))
172 
173 @[simp] theorem tracedFirstRootObstruction_erase (a : Prime → Bool) (r : ℚ)
174     (d : List ℕ) (m : ℕ) :
175     (tracedFirstRootObstruction a r d m).1 = firstRootObstruction a r d m := by
176   simp only [tracedFirstRootObstruction, findRootTrace_erase,
177     tracedRootObstructs_erase, firstRootObstruction]
178 
179 theorem tracedFirstRootObstruction_query_bound (a : Prime → Bool) (r : ℚ)
180     (d : List ℕ) (m : ℕ) :
181     (tracedFirstRootObstruction a r d m).2.length ≤ m + 1 := by
182   simpa only [tracedFirstRootObstruction, List.length_range, one_mul] using
183     findRootTrace_bound (tracedRootObstructs a r d m) (List.range (m + 1)) 1
184       (fun n _ => tracedRootObstructs_query_bound a r d m n)
185 
186 def tracedCertifiedRootSolver (a : Prime → Bool) (r : ℚ) (d : List ℕ) (m : ℕ) :
187     Except ℕ (ℚ × List ℕ) × List Prime :=
188   let search := tracedFirstRootObstruction a r d m
189   match search.1 with
190   | some p => (.error p, search.2)
191   | none =>
192     let correction := tracedRootCorrectionCode a r d m
193     (.ok (r / m, correction.1), search.2 ++ correction.2)
194 
195 theorem tracedCertifiedRootSolver_erase (a : Prime → Bool) (r : ℚ)
196     (d : List ℕ) (m : ℕ) :
197     (tracedCertifiedRootSolver a r d m).1 = certifiedRootSolver a r d m := by
198   simp only [tracedCertifiedRootSolver, certifiedRootSolver,
199     tracedFirstRootObstruction_erase]
200   split <;> simp_all [tracedRootCorrectionCode_erase]
201 
202 /-- Certified finite oracle-query bound, without any unit bit-cost claim. -/
203 theorem tracedCertifiedRootSolver_query_bound (a : Prime → Bool) (r : ℚ)
204     (d : List ℕ) (m : ℕ) :
205     (tracedCertifiedRootSolver a r d m).2.length ≤
206       m + 1 + 2 * rootCorrectionBound r d m := by
207   have hs := tracedFirstRootObstruction_query_bound a r d m
208   have hc := tracedRootCorrectionCode_query_bound a r d m
209   simp only [tracedCertifiedRootSolver]
210   split
211   · exact hs.trans (Nat.le_add_right _ _)
212   · simpa only [List.length_append] using Nat.add_le_add hs hc
213 
214 /-- The same short-circuit search with an explicit counter of predicate-candidate
215 visits, including candidates discarded without making an oracle request. -/
216 def countedFindRootTrace {α : Type*} (test : α → Bool × List Prime) :
217     List α → (Option α × List Prime) × ℕ
218   | [] => ((none, []), 0)
219   | x :: xs =>
220     let q := test x
221     if q.1 then ((some x, q.2), 1)
222     else
223       let tail := countedFindRootTrace test xs
224       ((tail.1.1, q.2 ++ tail.1.2), tail.2 + 1)
225 
226 @[simp] theorem countedFindRootTrace_erase {α : Type*} (test : α → Bool × List Prime)
227     (xs : List α) : (countedFindRootTrace test xs).1 = findRootTrace test xs := by
228   induction xs with
229   | nil => rfl
230   | cons x xs ih =>
231     simp only [countedFindRootTrace, findRootTrace]
232     split <;> simp_all
233 
234 theorem countedFindRootTrace_step_bound {α : Type*} (test : α → Bool × List Prime)
235     (xs : List α) : (countedFindRootTrace test xs).2 ≤ xs.length := by
236   induction xs with
237   | nil => exact Nat.le_refl 0
238   | cons x xs ih =>
239     simp only [countedFindRootTrace, List.length_cons]
240     split
241     · change 1 ≤ xs.length + 1
242       omega
243     · change (countedFindRootTrace test xs).2 + 1 ≤ xs.length + 1
244       omega
245 
246 /-- A counted certified execution: one visit per searched integer, and on success
247 one correction candidate for each integer below the proved finite bound. -/
248 def countedCertifiedRootSolver (a : Prime → Bool) (r : ℚ) (d : List ℕ) (m : ℕ) :
249     (Except ℕ (ℚ × List ℕ) × List Prime) × ℕ :=
250   let search := countedFindRootTrace (tracedRootObstructs a r d m) (List.range (m + 1))
251   match search.1.1 with
252   | some p => ((.error p, search.1.2), search.2)
253   | none =>
254     let correction := tracedRootCorrectionCode a r d m
255     ((.ok (r / m, correction.1), search.1.2 ++ correction.2),
256       search.2 + rootCorrectionBound r d m)
257 
258 theorem countedCertifiedRootSolver_erase (a : Prime → Bool) (r : ℚ)
259     (d : List ℕ) (m : ℕ) :
260     (countedCertifiedRootSolver a r d m).1 = tracedCertifiedRootSolver a r d m := by
261   simp only [countedCertifiedRootSolver, countedFindRootTrace_erase,
262     tracedCertifiedRootSolver, tracedFirstRootObstruction]
263   split <;> rfl
264 
265 theorem countedCertifiedRootSolver_step_bound (a : Prime → Bool) (r : ℚ)
266     (d : List ℕ) (m : ℕ) :
267     (countedCertifiedRootSolver a r d m).2 ≤ m + 1 + rootCorrectionBound r d m := by
268   have hs := countedFindRootTrace_step_bound (tracedRootObstructs a r d m)
269     (List.range (m + 1))
270   simp only [List.length_range] at hs
271   simp only [countedCertifiedRootSolver]
272   split
273   · exact hs.trans (Nat.le_add_right _ _)
274   · exact Nat.add_le_add_right hs _
275 
276 theorem countedCertifiedRootSolver_query_bound (a : Prime → Bool) (r : ℚ)
277     (d : List ℕ) (m : ℕ) :
278     (countedCertifiedRootSolver a r d m).1.2.length ≤
279       m + 1 + 2 * rootCorrectionBound r d m := by
280   rw [countedCertifiedRootSolver_erase]
281   exact tracedCertifiedRootSolver_query_bound a r d m
282 
283 /-- Semantic extraction correspondence composes the trace erasure with the
284 all-prime ambient correctness theorem for positive multipliers. -/
285 theorem tracedCertifiedRootSolver_sound (a : Prime → Bool) (r : ℚ) (d : List ℕ)
286     {m : ℕ} (hm : 0 < m) (t : ℚ) (e : List ℕ)
287     (h : (tracedCertifiedRootSolver a r d m).1 = .ok (t, e)) :
288     m • codedNormalValue a t e = codedNormalValue a r d := by
289   rw [tracedCertifiedRootSolver_erase] at h
290   exact certifiedRootSolver_ok a r d hm t e h
291 
292 end RealizationBoundaries

Back to source controls