LocalCocycleQueries.lean

1 import RealizationBoundaries.ComputableNormalCodes
2 
3 /-! # Denominator-local selector queries for the actual cocycle arithmetic -/
4 set_option autoImplicit false
5 set_option backward.isDefEq.respectTransparency false
6 noncomputable section
7 namespace RealizationBoundaries
8 
9 /-- The condition under which the cocycle cell can need a selector bit. -/
10 def localCocycleException (z : ℕ) : Prop :=
11   z.unpair.2.Prime ∧ z.unpair.2 ∣
12     RationalCode.normalDenominator (decodeNormalCode z.unpair.1.unpair.1).1 *
13       RationalCode.normalDenominator (decodeNormalCode z.unpair.1.unpair.2).1
14 
15 instance localCocycleException_decidable : DecidablePred localCocycleException := by
16   unfold localCocycleException
17   infer_instance
18 
19 theorem primrec_localCocycleException : PrimrecPred localCocycleException := by
20   let l : Primrec (fun z : ℕ => decodeNormalCode z.unpair.1.unpair.1) :=
21     primrec_decodeNormalCode.comp
22       ((Primrec.fst.comp Primrec.unpair).comp (Primrec.fst.comp Primrec.unpair))
23   let r : Primrec (fun z : ℕ => decodeNormalCode z.unpair.1.unpair.2) :=
24     primrec_decodeNormalCode.comp
25       ((Primrec.snd.comp Primrec.unpair).comp (Primrec.fst.comp Primrec.unpair))
26   let p : Primrec (fun z : ℕ => z.unpair.2) := Primrec.snd.comp Primrec.unpair
27   exact (primrec_prime_predicate.comp p).and (primrec_nat_dvd.comp p
28     (Primrec.nat_mul.comp
29       (RationalCode.primrec_normalDenominator.comp (Primrec.fst.comp l))
30       (RationalCode.primrec_normalDenominator.comp (Primrec.fst.comp r))))
31 
32 /-- The selector-independent sum of the two finite corrections. -/
33 def normalAddBaseCell (z : ℕ) : ℕ :=
34   ((decodeNormalCode z.unpair.1.unpair.1).2.getD z.unpair.2 0 +
35     (decodeNormalCode z.unpair.1.unpair.2).2.getD z.unpair.2 0) % z.unpair.2
36 
37 theorem primrec_normalAddBaseCell : Primrec normalAddBaseCell := by
38   let l : Primrec (fun z : ℕ => decodeNormalCode z.unpair.1.unpair.1) :=
39     primrec_decodeNormalCode.comp
40       ((Primrec.fst.comp Primrec.unpair).comp (Primrec.fst.comp Primrec.unpair))
41   let r : Primrec (fun z : ℕ => decodeNormalCode z.unpair.1.unpair.2) :=
42     primrec_decodeNormalCode.comp
43       ((Primrec.snd.comp Primrec.unpair).comp (Primrec.fst.comp Primrec.unpair))
44   let p : Primrec (fun z : ℕ => z.unpair.2) := Primrec.snd.comp Primrec.unpair
45   exact Primrec.nat_mod.comp
46     (Primrec.nat_add.comp ((Primrec.list_getD 0).comp (Primrec.snd.comp l) p)
47       ((Primrec.list_getD 0).comp (Primrec.snd.comp r) p)) p
48 
49 /-- The old arithmetic cell takes one supplied bit and makes no oracle calls. -/
50 def normalAddCellUsingBit (b : Bool) (z : ℕ) : ℕ :=
51   let c := decodeNormalCode z.unpair.1.unpair.1
52   let e := decodeNormalCode z.unpair.1.unpair.2
53   let p := z.unpair.2
54   let mask := if (if b then 1 else 0) = Nat.count Nat.Prime p % 2 then 1 else 0
55   (c.2.getD p 0 + e.2.getD p 0 + mask *
56     (RationalCode.primeResidue c.1 p + RationalCode.primeResidue e.1 p + p -
57       RationalCode.primeResidue (RationalCode.add c.1 e.1) p)) % p
58 
59 /-- Exactly one selector lookup is supplied to an exceptional prime's cell.
60 All other cells are independent of the selector. -/
61 def localNormalAddCell (a : ℕ → Bool) (z : ℕ) : ℕ :=
62   if localCocycleException z then
63     normalAddCellUsingBit (a (Nat.count Nat.Prime z.unpair.2 / 2)) z
64   else normalAddBaseCell z
65 
66 theorem localNormalAddCell_eq (a : ℕ → Bool) (z : ℕ) :
67     localNormalAddCell a z =
68       if localCocycleException z then normalAddCell a z else normalAddBaseCell z := by
69   rfl
70 
71 /-- The optimized cell agrees with the old cell at every actual prime coordinate. -/
72 theorem localNormalAddCell_same_prime_residue (a : ℕ → Bool)
73     (c e : NativeNormalCode) (p : Prime) :
74     (localNormalAddCell a
75       (Nat.pair (Nat.pair (Encodable.encode c) (Encodable.encode e)) p.val) : Coordinate p) =
76     (normalAddCell a
77       (Nat.pair (Nat.pair (Encodable.encode c) (Encodable.encode e)) p.val) : Coordinate p) := by
78   rw [localNormalAddCell_eq]
79   split_ifs with hx
80   · rfl
81   · have hn : ¬ p.val ∣ (RationalCode.value c.1).den * (RationalCode.value e.1).den := by
82       intro hd
83       apply hx
84       simp only [localCocycleException, Nat.unpair_pair, decodeNormalCode_encode,
85         ← (RationalCode.normal_fields c.1).2, ← (RationalCode.normal_fields e.1).2]
86       exact ⟨p.property, hd⟩
87     have hzero : sectionDefect (pairedSelector a) (RationalCode.value c.1)
88         (RationalCode.value e.1) p = 0 := by
89       by_contra hz
90       exact hn (sectionDefect_support (pairedSelector a) _ _ hz)
91     rw [normalAddCell_cast, hzero, add_zero]
92     simp only [normalAddBaseCell, Nat.unpair_pair, decodeNormalCode_encode,
93       ZMod.natCast_mod, Nat.cast_add, finiteCodeValue, ← List.getD_eq_getElem?_getD]
94 
95 namespace OracleComputable
96 variable {X : ℕ → Bool} {f g : ℕ → ℕ}
97 
98 /-- Primitive input predicates may choose between genuine oracle computations. -/
99 theorem localIte {P : ℕ → Prop} [DecidablePred P] (hP : PrimrecPred P)
100     (hf : OracleComputable X f) (hg : OracleComputable X g) :
101     OracleComputable X (fun n => if P n then f n else g n) := by
102   have hs : Computable (fun n : ℕ => if P n.unpair.1
103       then n.unpair.2.unpair.1 else n.unpair.2.unpair.2) :=
104     (Primrec.ite (hP.comp (Primrec.fst.comp Primrec.unpair))
105       ((Primrec.fst.comp Primrec.unpair).comp (Primrec.snd.comp Primrec.unpair))
106       ((Primrec.snd.comp Primrec.unpair).comp (Primrec.snd.comp Primrec.unpair))).to_comp
107   exact (of_computable hs).comp (id.pair (hf.pair hg)) |>.of_eq (fun n => by simp)
108 
109 end OracleComputable
110 
111 theorem localNormalAddCell_oracleComputable (a X : ℕ → Bool) (ha : SelectorReducible a X) :
112     OracleComputable X (localNormalAddCell a) :=
113   ((normalAddCell_oracleComputable a X ha).localIte primrec_localCocycleException
114     (OracleComputable.of_computable primrec_normalAddBaseCell.to_comp)).of_eq
115       (fun z => (localNormalAddCell_eq a z).symm)
116 
117 /-- Instrumented cell: the trace records the prime whose single bit was looked up.
118 A composite or a non-denominator prime has an empty trace. -/
119 def recordedLocalCell (a : ℕ → Bool) (z : ℕ) : ℕ × List ℕ :=
120   if localCocycleException z then
121     (normalAddCellUsingBit (a (Nat.count Nat.Prime z.unpair.2 / 2)) z, [z.unpair.2])
122   else (normalAddBaseCell z, [])
123 
124 theorem recordedLocalCell_value (a : ℕ → Bool) (z : ℕ) :
125     (recordedLocalCell a z).1 = localNormalAddCell a z := by
126   unfold recordedLocalCell localNormalAddCell
127   split <;> rfl
128 
129 theorem recordedLocalCell_query_count (a : ℕ → Bool) (z : ℕ) :
130     (recordedLocalCell a z).2.length = if localCocycleException z then 1 else 0 := by
131   unfold recordedLocalCell
132   split <;> rfl
133 
134 /-- The exact finite prime-labelled query schedule for the optimized correction. -/
135 def localCocycleQuerySchedule (input N : ℕ) : List ℕ :=
136   (List.range N).filter (fun p => decide (localCocycleException (Nat.pair input p)))
137 
138 theorem localCocycleQuerySchedule_nodup (input N : ℕ) :
139     (localCocycleQuerySchedule input N).Nodup :=
140   List.nodup_range.filter _
141 
142 theorem localCocycleQuerySchedule_length_le (input N : ℕ) :
143     (localCocycleQuerySchedule input N).length ≤ N := by
144   exact (List.length_filter_le _ _).trans_eq (List.length_range (n := N))
145 
146 /-- At the complete correction bound the schedule consists exactly of all prime
147 divisors of the denominator product, each once. -/
148 theorem localCocycleQuerySchedule_mem (c e : NativeNormalCode) (p : ℕ) :
149     p ∈ localCocycleQuerySchedule (Nat.pair (Encodable.encode c) (Encodable.encode e))
150       (normalAddBound c e) ↔
151       p.Prime ∧ p ∣ (RationalCode.value c.1).den * (RationalCode.value e.1).den := by
152   simp only [localCocycleQuerySchedule, List.mem_filter, List.mem_range, decide_eq_true_eq,
153     localCocycleException, Nat.unpair_pair, decodeNormalCode_encode,
154     ← (RationalCode.normal_fields c.1).2, ← (RationalCode.normal_fields e.1).2]
155   constructor
156   · exact fun h => h.2
157   · intro h
158     refine ⟨?_, h⟩
159     have hp := Nat.le_of_dvd
160       (Nat.mul_pos (RationalCode.value c.1).den_pos (RationalCode.value e.1).den_pos) h.2
161     change p < normalAddBound c e
162     unfold normalAddBound
163     rw [← (RationalCode.normal_fields c.1).2, ← (RationalCode.normal_fields e.1).2]
164     exact lt_of_le_of_lt hp (lt_of_lt_of_le (Nat.lt_succ_self _) (le_max_right _ _))
165 
166 /-- The complete optimized finite correction uses the checked finite native loop. -/
167 def localNormalAddResidues (a : ℕ → Bool) (c e : NativeNormalCode) : List ℕ :=
168   residueLoop (localNormalAddCell a) (Nat.pair (Encodable.encode c) (Encodable.encode e))
169     (normalAddBound c e)
170 
171 theorem localNormalAddResidues_same (a : ℕ → Bool) (c e : NativeNormalCode) :
172     finiteCodeValue (localNormalAddResidues a c e) = finiteCodeValue (normalAddResidues a c e) := by
173   funext p
174   by_cases hp : p.val < normalAddBound c e
175   · simp only [localNormalAddResidues, normalAddResidues, residueLoop_eq_ofFn,
176       finiteCodeValue, List.getElem?_ofFn, hp, dite_true, Option.getD_some]
177     exact localNormalAddCell_same_prime_residue a c e p
178   · have hl : (localNormalAddResidues a c e).length = normalAddBound c e := by
179       rw [localNormalAddResidues, residueLoop_eq_ofFn, List.length_ofFn]
180     have hr : (normalAddResidues a c e).length = normalAddBound c e := by
181       rw [normalAddResidues, residueLoop_eq_ofFn, List.length_ofFn]
182     rw [finiteCodeValue_eq_zero _ p (hl.symm ▸ Nat.le_of_not_gt hp),
183       finiteCodeValue_eq_zero _ p (hr.symm ▸ Nat.le_of_not_gt hp)]
184 
185 /-- The optimized finite normal form performs the identical actual group addition. -/
186 theorem localNormalAdd_correct (a : ℕ → Bool) (c e : NativeNormalCode) :
187     nativeNormalValue a (RationalCode.add c.1 e.1, localNormalAddResidues a c e) =
188       nativeNormalValue a c + nativeNormalValue a e := by
189   have h : nativeNormalValue a (RationalCode.add c.1 e.1, localNormalAddResidues a c e) =
190       nativeNormalValue a (nativeNormalAdd a c e) := by
191     apply Subtype.ext
192     change rationalSection _ _ + finiteCodeValue (localNormalAddResidues a c e) = _
193     rw [localNormalAddResidues_same]
194     rfl
195   exact h.trans (nativeNormalAdd_exact a c e)
196 
197 /-- The optimized full bounded loop has genuine native oracle semantics. -/
198 theorem localNormalAdd_loop_oracleComputable (a X : ℕ → Bool) (ha : SelectorReducible a X) :
199     OracleComputable X (fun z => Encodable.encode
200       (residueLoop (localNormalAddCell a) z.unpair.1 z.unpair.2)) :=
201   residueLoop_oracleComputable (localNormalAddCell_oracleComputable a X ha)
202 
203 end RealizationBoundaries

Back to source controls