1(* ------------------------------------------------------------------------- *) 2(* Mappings for Introspective Sets *) 3(* ------------------------------------------------------------------------- *) 4 5(*===========================================================================*) 6 7(* add all dependent libraries for script *) 8open HolKernel boolLib bossLib Parse; 9 10(* declare new theory at start *) 11val _ = new_theory "AKSmaps"; 12 13(* ------------------------------------------------------------------------- *) 14 15 16 17(* val _ = load "jcLib"; *) 18open jcLib; 19 20(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *) 21 22(* Get dependent theories local *) 23(* val _ = load "AKSsetsTheory"; *) 24open AKSsetsTheory; 25open AKSintroTheory; 26 27(* For SQRT n and LOG2 n *) 28(* val _ = load "logPowerTheory"; *) 29open logPowerTheory; 30 31(* (* val _ = load "monoidTheory"; *) *) 32(* (* val _ = load "groupTheory"; *) *) 33(* (* val _ = load "ringTheory"; *) *) 34(* (* val _ = load "ringUnitTheory"; *) *) 35open monoidTheory groupTheory ringTheory ringUnitTheory; 36 37(* (* val _ = load "fieldTheory"; *) *) 38open fieldTheory; 39 40(* Get polynomial theory of Ring *) 41(* (* val _ = load "polyWeakTheory"; *) *) 42(* (* val _ = load "polyRingTheory"; *) *) 43(* (* val _ = load "polyDivisionTheory"; *) *) 44(* (* val _ = load "polyBinomialTheory"; *) *) 45open polynomialTheory polyWeakTheory polyRingTheory polyDivisionTheory; 46open polyBinomialTheory polyEvalTheory; 47 48(* (* val _ = load "polyDividesTheory"; *) *) 49open polyDividesTheory; 50open polyMonicTheory; 51 52(* (* val _ = load "polyRootTheory"; *) *) 53open polyRootTheory; 54 55(* (* val _ = load "polyProductTheory"; *) *) 56open polyProductTheory; 57 58(* (* val _ = load "polyFieldTheory"; *) *) 59(* (* val _ = load "polyFieldDivisionTheory"; *) *) 60(* (* val _ = load "polyFieldModuloTheory"; *) *) 61open polyFieldTheory; 62open polyFieldDivisionTheory; 63open polyFieldModuloTheory; 64open polyRingModuloTheory; 65open polyModuloRingTheory; 66open polyIrreducibleTheory; 67 68open subgroupTheory; 69open groupOrderTheory; 70 71(* open dependent theories *) 72open pred_setTheory listTheory arithmeticTheory; 73 74(* Get dependent theories in lib *) 75(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *) 76(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *) 77(* (* val _ = load "helperFunctionTheory"; -- in ringTheory *) *) 78open helperNumTheory helperSetTheory helperFunctionTheory; 79 80(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *) 81(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *) 82open dividesTheory gcdTheory; 83 84open GaussTheory; (* for phi_eq_0 *) 85 86(* (* val _ = load "ringBinomialTheory"; *) *) 87open binomialTheory; 88open ringBinomialTheory; 89 90(* (* val _ = load "fieldInstancesTheory"; *) *) 91open monoidInstancesTheory; 92open groupInstancesTheory; 93open ringInstancesTheory; 94open fieldInstancesTheory; 95 96(* (* val _ = load "ffUnityTheory"; *) *) 97open ffBasicTheory; 98open ffAdvancedTheory; 99open ffPolyTheory; 100open ffUnityTheory; 101 102 103(* ------------------------------------------------------------------------- *) 104(* Mappings for Introspective Sets Documentation *) 105(* ------------------------------------------------------------------------- *) 106(* Overloading: 107*) 108(* Definitions and Theorems (# are exported): 109 110 Injective Map into (Q z): 111 setP_poly_mod_eq |- !r k s. Ring r /\ 0 < k ==> 112 !p q. p IN P /\ q IN P /\ (p == q) (pm (unity k)) ==> 113 !m. m IN N ==> (peval (p - q) (X ** m) == |0|) (pm (unity k)) 114 setP_poly_mod_divisor_eq |- !r k s z. Ring r /\ 0 < k /\ ulead z /\ (unity k % z = |0|) ==> 115 !p q. p IN P /\ q IN P /\ (p == q) (pm z) ==> 116 !m. m IN N ==> (peval (p - q) (X ** m) == |0|) (pm z) 117 setP_poly_modN_eq |- !r k s. Ring r /\ 0 < k ==> 118 !p q. p IN P /\ q IN P /\ (p == q) (pm (unity k)) ==> 119 !n. n IN M ==> (peval (p - q) (X ** n) == |0|) (pm (unity k)) 120 setP_poly_modN_divisor_eq |- !r k s z. Ring r /\ 0 < k /\ ulead z /\ (unity k % z = |0|) ==> 121 !p q. p IN P /\ q IN P /\ (p == q) (pm z) ==> 122 !n. n IN M ==> (peval (p - q) (X ** n) == |0|) (pm z) 123 setP_mod_eq_gives_modN_roots 124 |- !r k s z. Field r /\ 0 < k /\ mifactor z (unity k) ==> 125 !p q. p IN P /\ q IN P /\ (p == q) (pm z) ==> 126 !n. n IN M ==> rootz (lift (p - q)) (X ** n % z) 127 reduceP_mod_modP_inj_0 |- !r k s z. FiniteField r /\ mifactor z (unity k) /\ 1 < deg z /\ 128 (forderz X = k) ==> INJ (\p. p % z) PM (Q z) 129 reduceP_mod_modP_inj_1 |- !r k s z. Field r /\ 0 < k /\ mifactor z (unity k) /\ 130 (forderz X = k) ==> INJ (\p. p % z) PM (Q z) 131 132 Elements of Reduced Set P as roots: 133 setP_element_as_root_mod_unity |- !r k s. Ring r /\ 0 < k ==> 134 !n m. n IN N /\ m IN N /\ (n MOD k = m MOD k) ==> 135 !p. p IN P ==> (peval (X ** n - X ** m) p == |0|) (pm (unity k)) 136 setP_element_as_root_mod_unity_factor 137 |- !r k s z. Field r /\ 0 < k /\ mifactor z (unity k) ==> 138 !n m. n IN N /\ m IN N /\ (n MOD k = m MOD k) ==> 139 !p. p IN P ==> (peval (X ** n - X ** m) p == |0|) (pm z) 140 setN_mod_eq_gives_modP_roots_0 |- !r k s z. Ring r /\ 0 < k /\ mifactor z (unity k) /\ 1 < deg z ==> 141 !n m. n IN N /\ m IN N /\ (n MOD k = m MOD k) ==> 142 !p. p IN Q z ==> rootz (lift (X ** n - X ** m)) p 143 setN_mod_eq_gives_modP_roots_1 |- !r k s z. Field r /\ 0 < k /\ mifactor z (unity k) ==> 144 !n m. n IN N /\ m IN N /\ (n MOD k = m MOD k) ==> 145 !p. p IN Q z ==> rootz (lift (X ** n - X ** m)) p 146 setN_mod_eq_gives_modP_roots_2 |- !r k s z. Field r /\ 0 < k /\ mifactor z (unity k) ==> 147 !n m. n IN N /\ m IN N /\ (n MOD k = m MOD k) ==> 148 Q z SUBSET rootsz (lift (X ** n - X ** m)) 149 setN_mod_eq_gives_modP_roots |- !r k s z. Field r /\ 0 < k /\ mifactor z (unity k) ==> 150 !n m. n IN N /\ m IN N /\ (n MOD k = m MOD k) ==> 151 !p. p IN Q z ==> (peval (X ** n - X ** m) p == |0|) (pm z) 152 153 Injective Map into M: 154 reduceN_mod_modN_inj_0 |- !r k s z. Field r /\ mifactor z (unity k) /\ 1 < deg z ==> 155 !p q. 1 < p /\ 1 < q /\ p IN N /\ q IN N /\ 156 MAX p q ** TWICE (SQRT (CARD M)) < CARD (Q z) ==> 157 INJ (\m. m MOD k) (NM p q (SQRT (CARD M))) M 158 reduceN_mod_modN_inj_1 |- !r k s z. Field r /\ mifactor z (unity k) ==> 159 !p q. 1 < p /\ 1 < q /\ p IN N /\ q IN N /\ 160 MAX p q ** TWICE (SQRT (CARD M)) < CARD (Q z) ==> 161 INJ (\m. m MOD k) (NM p q (SQRT (CARD M))) M 162 reduceN_mod_modN_inj_2 |- !r k s z. Field r /\ mifactor z (unity k) ==> 163 !p q. 1 < p /\ 1 < q /\ p IN N /\ q IN N /\ 164 (p * q) ** SQRT (CARD M) < CARD (Q z) ==> 165 INJ (\m. m MOD k) (NM p q (SQRT (CARD M))) M 166 167 Polynomial Product map to Power set of Monomials: 168 set_of_X_add_c_subset_setP_0 |- !r k s. Ring r ==> 169 !t. t SUBSET IMAGE SUC (count s) ==> 170 IMAGE (\c. X + |c|) t SUBSET P 171 set_of_X_add_c_subset_setP |- !r k s. Ring r ==> 172 !h t. t SUBSET IMAGE SUC (count (MIN s h)) ==> 173 IMAGE (\c. X + |c|) t SUBSET P 174 poly_prod_set_in_setP |- !r k s. Ring r /\ 0 < k ==> 175 !t. FINITE t /\ t SUBSET P ==> PPROD t IN P 176 reduceP_poly_subset_reduceP_0 |- !r k s. Ring r /\ 0 < k /\ s < CARD M /\ CARD M < char r ==> 177 PPM s SUBSET PM 178 reduceP_poly_subset_reduceP |- !r k s. Ring r /\ 0 < k /\ 0 < s /\ s < char r ==> 179 PPM (MIN s (CARD M)) SUBSET PM 180 181 Lower Bound for (Q z) by Combinatorics: 182 modP_card_lower_0 |- !r k s z. FiniteField r /\ mifactor z (unity k) /\ 1 < deg z /\ 183 (forderz X = k) /\ 0 < s /\ s < char r ==> 184 2 ** MIN s (CARD M) <= CARD (Q z) 185 modP_card_lower_1 |- !r k s z. FiniteField r /\ mifactor z (unity k) /\ 186 (forderz X = k) /\ 1 < k /\ 0 < s /\ s < char r ==> 187 2 ** MIN s (CARD M) <= CARD (Q z) 188 189 Improvements for Version 2: 190 poly_order_prime_condition_0 |- !r. Field r ==> !z. monic z /\ ipoly z ==> 191 !p. poly p /\ deg p < deg z /\ p <> |0| /\ p <> |1| ==> 192 !k. prime k /\ (p ** k == |1|) (pm z) ==> (forderz p = k) 193 poly_order_prime_condition |- !r. Field r ==> !z. monic z /\ ipoly z ==> 194 !p. poly p /\ p % z <> |0| /\ p % z <> |1| ==> 195 !k. prime k /\ (p ** k == |1|) (pm z) ==> (forderz p = k) 196 poly_X_order_prime_condition |- !r. Field r ==> !z. monic z /\ ipoly z /\ z <> unity 1 ==> 197 !k. prime k /\ (X ** k == |1|) (pm z) ==> (forderz X = k) 198 reduceP_mod_modP_inj_2 |- !r k s z. Field r /\ prime k /\ mifactor z (unity k) /\ z <> unity 1 ==> 199 INJ (\p. p % z) PM (Q z) 200 modP_card_lower_2 |- !r k s z. FiniteField r /\ prime k /\ 0 < s /\ s < char r /\ 201 mifactor z (unity k) /\ z <> unity 1 ==> 202 2 ** MIN s (CARD M) <= CARD (Q z) 203 204 Upper Bound for (Q z) by Roots: 205 modP_card_upper_better |- !r k n s z. FiniteField r /\ coprime k (CARD R) /\ 1 < ordz k (CARD R) /\ 206 char r divides n /\ n IN N /\ ~perfect_power n (char r) /\ mifactor z (unity k) ==> 207 CARD (Q z) <= n ** SQRT (CARD M) 208 modP_card_upper_better_1 |- !r k n s z. FiniteField r /\ coprime k (CARD R) /\ 1 < ordz k (CARD R) /\ 209 char r divides n /\ n IN N /\ ~perfect_power n (char r) /\ mifactor z (unity k) ==> 210 CARD (Q z) <= 2 ** (SQRT (CARD M) * ulog n) 211 modP_card_upper_better_2 |- !r k n s z. FiniteField r /\ coprime k (CARD R) /\ 1 < ordz k (CARD R) /\ 212 char r divides n /\ n IN N /\ ~perfect_power n (char r) /\ mifactor z (unity k) ==> 213 CARD (Q z) <= 2 ** (SQRT (phi k) * ulog n) 214 215 Better Lower Bound for (Q z): 216 modP_card_lower_better |- !r k s z. FiniteField r /\ mifactor z (unity k) /\ 1 < deg z /\ 217 (forderz X = k) /\ 1 < CARD M /\ 0 < s /\ s < char r ==> 218 2 ** MIN s (CARD M) < CARD (Q z) 219 modP_card_range |- !r k n s z. FiniteField r /\ coprime k (CARD R) /\ 220 1 < ordz k (CARD R) /\ char r divides n /\ 221 n IN N /\ ~perfect_power n (char r) /\ 222 0 < s /\ s < char r /\ mifactor z (unity k) /\ 1 < deg z /\ 223 (forderz X = k) /\ 1 < CARD M ==> 224 2 ** MIN s (CARD M) < CARD (Q z) /\ CARD (Q z) <= n ** SQRT (CARD M) 225 226 Exponent bounds for (CARD M): 227 modN_card_with_ulog_le_min_1 228 |- !r. Ring r ==> 229 !k n s. 1 < k /\ n IN N /\ ulog n ** 2 <= ordz k n ==> 230 SQRT (CARD M) * ulog n <= MIN (SQRT (phi k) * ulog n) (CARD M) 231 modN_card_with_ulog_le_min_2 232 |- !r. Ring r ==> 233 !k n s. 1 < k /\ n IN N /\ TWICE (ulog n) ** 2 <= ordz k n ==> 234 TWICE (SQRT (CARD M)) * ulog n <= MIN (TWICE (SQRT (phi k)) * ulog n) (CARD M) 235 modN_card_in_exp_lt_bound_0 236 |- !r. Ring r ==> 237 !k n s. 1 < k /\ 1 < n /\ n IN N /\ 238 TWICE (SUC (LOG2 n)) ** 2 <= ordz k n ==> 239 n ** TWICE (SQRT (CARD M)) < 2 ** MIN (TWICE (SQRT (phi k)) * SUC (LOG2 n)) (CARD M) 240 modN_card_in_exp_lt_bound_1 241 |- !r. Ring r ==> 242 !k n s. 1 < k /\ 1 < n /\ n IN N /\ (SUC (LOG2 n)) ** 2 <= ordz k n ==> 243 n ** (SQRT (CARD M)) < 2 ** MIN (SQRT (phi k) * SUC (LOG2 n)) (CARD M) 244 modN_card_in_exp_lt_bound_2 245 |- !r. Ring r ==> 246 !k n s. 1 < k /\ 1 < n /\ n IN N ==> 247 !h. 0 < h /\ n < 2 ** h /\ h ** 2 <= ordz k n ==> 248 n ** SQRT (CARD M) < 2 ** MIN (SQRT (phi k) * h) (CARD M) 249 modN_card_in_exp_lt_bound_3 250 |- !r. Ring r ==> 251 !k n s. 1 < k /\ 1 < n /\ 252 ~perfect_power n 2 /\ n IN N /\ ulog n ** 2 <= ordz k n ==> 253 n ** SQRT (CARD M) < 2 ** MIN (SQRT (phi k) * ulog n) (CARD M) 254 modN_card_in_exp_lt_bound_3_alt 255 |- !r. Ring r ==> 256 !n a k s. 1 < k /\ 1 < n /\ ~perfect_power n 2 /\ 257 (a = ulog n ** 2) /\ (s = SQRT (phi k) * ulog n) /\ 258 a <= ordz k n /\ n IN N ==> 259 n ** SQRT (CARD M) < 2 ** MIN s (CARD M) 260 modN_card_in_exp_lt_bound_4 261 |- !r. Ring r ==> 262 !k n s. 1 < k /\ 1 < n /\ ~perfect_power n 2 /\ n IN N /\ 263 TWICE (ulog n) ** 2 <= ordz k n ==> 264 n ** TWICE (SQRT (CARD M)) < 2 ** MIN (TWICE (SQRT (phi k)) * ulog n) (CARD M) 265 modN_card_in_exp_le_bound_0 266 |- !r. Ring r ==> 267 !k n s. 1 < k /\ 1 < n /\ n IN N /\ TWICE (ulog n) ** 2 <= ordz k n ==> 268 n ** TWICE (SQRT (CARD M)) <= 2 ** MIN (TWICE (SQRT (phi k)) * ulog n) (CARD M) 269 modN_card_in_exp_le_bound_1 270 |- !r. Ring r ==> 271 !k n s. 1 < k /\ n IN N ==> 272 !h. 0 < h /\ n <= 2 ** h /\ h ** 2 <= ordz k n ==> 273 n ** SQRT (CARD M) <= 2 ** MIN (SQRT (phi k) * h) (CARD M) 274 modN_card_in_exp_le_bound_2 275 |- !r. Ring r ==> 276 !k n s. 1 < k /\ 1 < n /\ n IN N /\ ulog n ** 2 <= ordz k n ==> 277 n ** SQRT (CARD M) <= 2 ** MIN (SQRT (phi k) * ulog n) (CARD M) 278 modP_card_upper_better_3 279 |- !r k n s z. FiniteField r /\ coprime k (CARD R) /\ 1 < ordz k (CARD R) /\ 280 char r divides n /\ n IN N /\ ~perfect_power n (char r) /\ 281 mifactor z (unity k) /\ ulog n ** 2 <= ordz k n ==> 282 CARD (Q z) <= 2 ** MIN (SQRT (phi k) * ulog n) (CARD M) 283 modP_card_lower_better_3 284 |- !r k n s z. FiniteField r /\ mifactor z (unity k) /\ 1 < deg z /\ 285 (forderz X = k) /\ 1 < n /\ n IN N /\ ulog n ** 2 <= ordz k n /\ 286 (s = SQRT (phi k) * ulog n) /\ s < char r ==> 287 n ** SQRT (CARD M) < CARD (Q z) 288*) 289 290(* ------------------------------------------------------------------------- *) 291(* Helper Theorems *) 292(* ------------------------------------------------------------------------- *) 293 294(* ------------------------------------------------------------------------- *) 295(* Injective Map into (Q z) *) 296(* ------------------------------------------------------------------------- *) 297 298(* 299p IN PM /\ q IN PM /\ p % h = q % h ==> peval p X = peval q X 300p IN PM /\ q IN PM /\ p % h = q % h ==> p = q by above, poly_peval_by_X 301*) 302 303(* Theorem: !p q. p IN P /\ q IN P /\ (p == q) (pm (unity k)) ==> 304 !m. m IN N ==> (peval (p - q) (X ** m) == |0|) (pm (unity k)) *) 305(* Proof: 306 We have: 307 p IN P ==> poly p /\ m intro p by setP_element 308 q IN P ==> poly q /\ m intro q by setP_element 309 Let u = unity k, 310 Then ulead u by poly_unity_ulead, 0 < k 311 Now (p == q) (pm u) ==> (p ** m == q ** m) (pm u) by pmod_exp_eq 312 LHS: (p ** m == peval p (X ** m)) (pm u) by poly_intro_def 313 RHS: (q ** m == peval q (X ** m)) (pm u) by poly_intro_def 314 Hence (peval p (X ** m) == peval q (X ** m)) (pm u) by poly_mod_eq_eq 315 and (peval (p - q) (X ** m) == |0|) (pm u) by poly_mod_peval_eq 316*) 317val setP_poly_mod_eq = store_thm( 318 "setP_poly_mod_eq", 319 ``!(r:'a ring) k s:num. Ring r /\ 0 < k ==> 320 !p q. p IN P /\ q IN P /\ (p == q) (pm (unity k)) ==> 321 !m. m IN N ==> (peval (p - q) (X ** m) == |0|) (pm (unity k))``, 322 rpt strip_tac >> 323 `poly p /\ m intro p` by metis_tac[setP_element] >> 324 `poly q /\ m intro q` by metis_tac[setP_element] >> 325 qabbrev_tac `u = unity k` >> 326 `poly X /\ ulead u` by rw[poly_unity_ulead, Abbr`u`] >> 327 `(p ** m == q ** m) (pm u)` by rw[pmod_exp_eq] >> 328 `(p ** m == peval p (X ** m)) (pm u)` by metis_tac[poly_intro_def] >> 329 `(q ** m == peval q (X ** m)) (pm u)` by metis_tac[poly_intro_def] >> 330 `!h n. poly h ==> poly (h ** n)` by rw[] >> 331 `(peval p (X ** m) == peval q (X ** m)) (pm u)` by prove_tac[poly_mod_eq_eq, poly_peval_poly] >> 332 rw[GSYM poly_mod_peval_eq]); 333 334(* Theorem: 0 < k /\ ulead z /\ ((unity k) % h = |0|) ==> 335 !p q. p IN P /\ q IN P /\ (p == q) (pm h) ==> 336 !m. m IN N ==> (peval (p - q) (X ** m) == |0|) (pm h) *) 337(* Proof: 338 We have: 339 p IN P ==> poly p /\ m intro p by setP_element 340 q IN P ==> poly q /\ m intro q by setP_element 341 and #1 <> #0 by poly_deg_pos_ring_one_ne_zero 342 Let u = unity k, and pmonic u by poly_unity_pmonic, #1 <> #0 343 Now (p == q) (pm z) ==> (p ** m == q ** m) (pm z) by pmod_exp_eq 344 LHS: (p ** m == peval p (X ** m)) (pm u) by poly_intro_def 345 i.e. (p ** m == peval p (X ** m)) (pm z) by poly_mod_eq_divisor 346 RHS: (q ** m == peval q (X ** m)) (pm u) by poly_intro_def 347 i.e. (q ** m == peval q (X ** m)) (pm z) by poly_mod_eq_divisor 348 Hence (peval p (X ** m) == peval q (X ** m)) (pm z) by poly_mod_eq_eq 349 and (peval (p - q) (X ** m) == |0|) (pm z) by poly_mod_peval_eq 350*) 351val setP_poly_mod_divisor_eq = store_thm( 352 "setP_poly_mod_divisor_eq", 353 ``!(r:'a ring) k s:num z. Ring r /\ 0 < k /\ ulead z /\ ((unity k) % z = |0|) ==> 354 !p q. p IN P /\ q IN P /\ (p == q) (pm z) ==> 355 !m. m IN N ==> (peval (p - q) (X ** m) == |0|) (pm z)``, 356 rpt strip_tac >> 357 `poly p /\ m intro p` by metis_tac[setP_element] >> 358 `poly q /\ m intro q` by metis_tac[setP_element] >> 359 qabbrev_tac `u = unity k` >> 360 `poly X /\ ulead u` by rw[poly_unity_ulead, Abbr`u`] >> 361 `(p ** m == q ** m) (pm z)` by rw[pmod_exp_eq] >> 362 `(p ** m == peval p (X ** m)) (pm u)` by metis_tac[poly_intro_def] >> 363 `(q ** m == peval q (X ** m)) (pm u)` by metis_tac[poly_intro_def] >> 364 `!z n. poly z ==> poly (z ** n)` by rw[] >> 365 `!u v. poly u /\ poly v ==> poly (peval u v)` by rw[] >> 366 `(p ** m == peval p (X ** m)) (pm z)` by metis_tac[poly_mod_eq_divisor] >> 367 `(q ** m == peval q (X ** m)) (pm z)` by metis_tac[poly_mod_eq_divisor] >> 368 `(peval p (X ** m) == peval q (X ** m)) (pm z)` by prove_tac[poly_mod_eq_eq] >> 369 rw[GSYM poly_mod_peval_eq]); 370 371(* Theorem: 0 < k ==> !p q. p IN P /\ q IN P /\ (p == q) (pm (unity k)) ==> 372 !n. n IN M ==> (peval (p - q) (X ** n) == |0|) (pm (unity k)) *) 373(* Proof: 374 For n in M, there is m IN N such that n = m MOD k, by modN_element 375 We have: 376 p IN P ==> poly p /\ m intro p by setP_element 377 q IN P ==> poly q /\ m intro q by setP_element 378 Let u = unity k, 379 Then ulead u by poly_unity_ulead, 0 < k 380 Now (p == q) (pm u) ==> (p ** m == q ** m) (pm u) by pmod_exp_eq 381 LHS: (p ** m == peval p (X ** m)) (pm u) by poly_intro_def 382 RHS: (q ** m == peval q (X ** m)) (pm u) by poly_intro_def 383 Hence (peval p (X ** m) == peval q (X ** m)) (pm u) by poly_mod_eq_eq 384 But (X ** m == X ** n) (pm u) by poly_unity_exp_mod, 0 < k 385 so (peval p (X ** m) == peval p (X ** n)) (pm u) by poly_peval_mod_eq 386 and (peval q (X ** m) == peval q (X ** n)) (pm u) by poly_peval_mod_eq 387 Hence (peval p (X ** n) == peval q (X ** n)) (pm u) by poly_mod_eq_eq 388 or (peval (p - q) (X ** n) == |0|) (pm u) by poly_mod_peval_eq 389*) 390val setP_poly_modN_eq = store_thm( 391 "setP_poly_modN_eq", 392 ``!(r:'a ring) k s:num. Ring r /\ 0 < k ==> 393 !p q. p IN P /\ q IN P /\ (p == q) (pm (unity k)) ==> 394 !n. n IN M ==> (peval (p - q) (X ** n) == |0|) (pm (unity k))``, 395 rpt strip_tac >> 396 `?m. m IN N /\ (n = m MOD k)` by metis_tac[modN_element] >> 397 `poly p /\ m intro p` by metis_tac[setP_element] >> 398 `poly q /\ m intro q` by metis_tac[setP_element] >> 399 qabbrev_tac `u = unity k` >> 400 `poly X /\ ulead u` by rw[poly_unity_ulead, Abbr`u`] >> 401 `(p ** m == q ** m) (pm u)` by rw[pmod_exp_eq] >> 402 `(p ** m == peval p (X ** m)) (pm u)` by metis_tac[poly_intro_def] >> 403 `(q ** m == peval q (X ** m)) (pm u)` by metis_tac[poly_intro_def] >> 404 `poly (p ** m) /\ poly (q ** m) /\ poly (peval p (X ** m)) /\ poly (peval p (X ** n)) /\ poly (peval q (X ** m)) /\ poly (peval q (X ** n))` by rw[] >> 405 `(peval p (X ** m) == peval q (X ** m)) (pm u)` by prove_tac[poly_mod_eq_eq] >> 406 `(X ** m == X ** n) (pm u)` by rw[poly_unity_exp_mod, Abbr`u`] >> 407 `(peval p (X ** m) == peval p (X ** n)) (pm u)` by rw[poly_peval_mod_eq] >> 408 `(peval q (X ** m) == peval q (X ** n)) (pm u)` by rw[poly_peval_mod_eq] >> 409 `(peval p (X ** n) == peval q (X ** n)) (pm u)` by prove_tac[poly_mod_eq_eq] >> 410 rw[GSYM poly_mod_peval_eq]); 411 412(* Theorem: ((unity k) % z = |0|) /\ p IN P /\ q IN P /\ (p == q) (pm z) ==> 413 !n. n IN M ==> (peval (p - q) (X ** n) == |0|) (pm z) *) 414(* Proof: 415 For n in M, there is m IN N such that n = m MOD k, by modN_element 416 We have: 417 p IN P ==> poly p /\ m intro p by setP_element 418 q IN P ==> poly q /\ m intro q by setP_element 419 Let u = unity k, 420 Then ulead u by poly_unity_ulead, 0 < k 421 Also (X ** m == X ** n) (pm u) since n = m MOD k by poly_unity_exp_mod, 0 < k [1] 422 423 By m intro p: 424 (p ** m == peval p (X ** m)) (pm u) by poly_intro_def 425 and (peval p (X ** m) == peval p (X ** n)) (pm u) by poly_peval_mod_eq from [1] 426 ==> (p ** m == peval p (X ** n)) (pm u) by poly_mod_transitive 427 ==> (p ** m == peval p (X ** n)) (pm z) by poly_mod_eq_divisor [2] 428 Similarly, by m intro q: 429 (q ** m == peval q (X ** m)) (pm u) by poly_intro_def 430 and (peval q (X ** m) == peval q (X ** n)) (pm u) by poly_peval_mod_eq from [1] 431 ==> (q ** m == peval q (X ** n)) (pm u) by poly_mod_transitive 432 ==> (q ** m == peval q (X ** n)) (pm z) by poly_mod_eq_divisor [3] 433 Now, 434 (p == q) (pm z) 435 ==> (p ** m == q ** m) (pm z) by pmod_exp_eq 436 Hence (peval p (X ** n) == peval q (X ** n)) (pm z) by poly_mod_eq_eq from [2], [3] 437 or (peval (p - q) (X ** n) == |0|) (pm z) by poly_mod_peval_eq 438*) 439val setP_poly_modN_divisor_eq = store_thm( 440 "setP_poly_modN_divisor_eq", 441 ``!(r:'a ring) k s:num z. Ring r /\ 0 < k /\ ulead z /\ ((unity k) % z = |0|) ==> 442 !p q. p IN P /\ q IN P /\ (p == q) (pm z) ==> 443 !n. n IN M ==> (peval (p - q) (X ** n) == |0|) (pm z)``, 444 rpt strip_tac >> 445 `?m. m IN N /\ (n = m MOD k)` by metis_tac[modN_element] >> 446 `poly p /\ m intro p` by metis_tac[setP_element] >> 447 `poly q /\ m intro q` by metis_tac[setP_element] >> 448 qabbrev_tac `u = unity k` >> 449 `poly X /\ ulead u` by rw[poly_unity_ulead, Abbr`u`] >> 450 `!x. poly x ==> !n. poly (x ** n)` by rw[] >> 451 `!x. poly x ==> poly (peval p x) /\ poly (peval q x)` by rw[] >> 452 `(X ** m == X ** n) (pm u)` by rw[poly_unity_exp_mod, Abbr`u`] >> 453 `(p ** m == peval p (X ** m)) (pm u)` by metis_tac[poly_intro_def] >> 454 `(peval p (X ** m) == peval p (X ** n)) (pm u)` by rw[poly_peval_mod_eq] >> 455 `(p ** m == peval p (X ** n)) (pm z)` by metis_tac[poly_mod_transitive, poly_mod_eq_divisor] >> 456 `(q ** m == peval q (X ** m)) (pm u)` by metis_tac[poly_intro_def] >> 457 `(peval q (X ** m) == peval q (X ** n)) (pm u)` by rw[poly_peval_mod_eq] >> 458 `(q ** m == peval q (X ** n)) (pm z)` by metis_tac[poly_mod_transitive, poly_mod_eq_divisor] >> 459 `(p ** m == q ** m) (pm z)` by rw[pmod_exp_eq] >> 460 `(peval p (X ** n) == peval q (X ** n)) (pm z)` by prove_tac[poly_mod_eq_eq] >> 461 rw[GSYM poly_mod_peval_eq]); 462 463(* 464Given: 465setP_poly_mod_eq 466|- !r k s. Ring r /\ #1 <> #0 ==> 467 !p q. p IN P /\ q IN P /\ (p == q) (pm (unity k)) ==> 468 !m. m IN N ==> (peval (p - q) (X ** m) == |0|) (pm (unity k)): thm 469 470To prove: 471not setP_poly_mod_divisor_eq 472|- !r k s z. Ring r /\ #1 <> #0 /\ pmonic z /\ (unity k % z = |0|) ==> 473 !p q. p IN P /\ q IN P /\ (p == q) (pm z) ==> 474 !m. m IN N ==> (peval (p - q) (X ** m) == |0|) (pm z): thm 475 476but setP_poly_modN_divisor_eq 477|- !r k s z. Ring r /\ #1 <> #0 /\ pmonic z /\ (unity k % z = |0|) ==> 478 !p q. p IN P /\ q IN P /\ (p == q) (pm z) ==> 479 !n. n IN M ==> (peval (p - q) (X ** n) == |0|) (pm z): thm 480*) 481 482(* Theorem: 0 < k /\ mifactor z (unity k) ==> !p q. p IN P /\ q IN P /\ (p == q) (pm z) ==> 483 !n. n IN M ==> rootz (lift (p - q)) (X ** n % z) *) 484(* Proof: 485 p IN P ==> poly p by setP_element_poly 486 q IN P ==> poly q by setP_element_poly 487 Let d = p - q. 488 Now, n IN M and (p == q) (pm z) 489 ==> (peval d (X ** n) == |0|) (pm z) by setP_poly_modN_divisor_eq 490 ==> ((peval d (X ** n)) % z = |0|) by pmod_zero 491 ==> rootz (lift (p - q)) (X ** n % z) by poly_mod_lift_root_X_exp 492*) 493val setP_mod_eq_gives_modN_roots = store_thm( 494 "setP_mod_eq_gives_modN_roots", 495 ``!(r:'a field) k s:num z. Field r /\ 0 < k /\ mifactor z (unity k) ==> 496 !p q. p IN P /\ q IN P /\ (p == q) (pm z) ==> 497 !n. n IN M ==> rootz (lift (p - q)) (X ** n % z)``, 498 rpt strip_tac >> 499 `Ring r` by rw[] >> 500 `pmonic z` by metis_tac[poly_monic_irreducible_factor] >> 501 qabbrev_tac `d = p - q` >> 502 `poly p /\ poly q /\ poly d` by metis_tac[setP_element_poly, poly_sub_poly] >> 503 metis_tac[setP_poly_modN_divisor_eq, pmod_zero, poly_mod_lift_root_X_exp]); 504 505(* Theorem: mifactor z (unity k) /\ 1 < deg z /\ (forderz X = k) ==> INJ (\p. p % z) PM (Q z) *) 506(* Proof: 507 Since 1 < deg z ==> 0 < deg z, 508 monic z ==> pmonic z by notation 509 and 0 < k by poly_X_order_nonzero 510 Let u = unity k, 511 (X ** k == |1|) (pm u) by poly_unity_pmod_eqn, 0 < k 512 By INJ_DEF, this is to show: 513 (1) p IN PM ==> p % z IN Q z 514 True by reduceP_element_mod. 515 (2) p IN PM /\ p' IN PM /\ p % z = p' % z ==> p = p' 516 Let d = p - p'. 517 We have poly p and poly p' by reduceP_element_poly 518 poly d by poly_sub_poly 519 If d = |0|, 520 |0| = p - p' ==> p = p' by poly_sub_eq_zero 521 If d <> |0|, 522 Show that: !n. n IN M ==> X ** n % z is a root of (lift d): 523 p IN P and p' IN P by reduceP_subset_setP, SUBSET_DEF 524 (p == p') (pm z) and (u % z = |0|) by pmod_def_alt 525 Hence !n. n IN M 526 ==> rootz (lift d) (X ** n % z) by setP_mod_eq_gives_modN_roots 527 Next, show that: 528 INJ (\n. X ** n % z) M (rootsz (lift d)) 529 By INJ_DEF, this is to show: 530 (1) X ** n % z IN rootsz (lift d) 531 Since rootz (lift d) (X ** n % z) by above 532 deg (X ** n % z) < deg z by poly_deg_mod_less 533 (X ** n % z) IN Rz by poly_mod_ring_element 534 Hence X ** n % h IN rootsz (lift d) by poly_roots_member 535 (2) n IN M /\ n' IN M /\ X ** n % z = X ** n' % z ==> n = n' 536 n IN M ==> n < k by modN_element_less 537 n' IN M ==> n' < k by modN_element_less 538 X ** n % z = X ** n' % z 539 ==> (X ** n == X ** n') (pm z) by pmod_def_alt 540 Hence n = n' by poly_mod_field_exp_eq_0 541 Apply INJ_CARD: 542 |- !f s t. INJ f s t /\ FINITE t ==> CARD s <= CARD t 543 First show: FINITE (rootsz (lift d)) 544 Since Field (PolyModRing r z) by poly_mod_irreducible_field 545 polyz (lift d) by poly_mod_lift_poly 546 |0|z = [] by poly_ring_property 547 lift d <> |0|z by poly_lift_eq_zero, poly_zero 548 Hence FINITE (rootsz (lift d)) by poly_roots_finite 549 Therefore CARD M <= CARD (rootsz (lift d)) by INJ_CARD 550 Apply poly_roots_count 551 |- !r. Field r ==> !p. poly p /\ p <> |0| ==> CARD (roots p) <= deg p 552 With polyz (lift d) by poly_mod_lift_poly, above 553 lift d <> |0|z by poly_lift_eq_zero, above 554 CARD (rootsz (lift d)) <= degz (lift d) 555 by poly_roots_count 556 But degz (lift d) = deg d by poly_mod_lift_deg 557 Hence CARD M <= deg d by LESS_EQ_TRANS 558 Get a contradiction: 559 p IN PM ==> deg p < CARD M by reduceP_element 560 p' IN PM ==> deg p' < CARD M by reduceP_element 561 deg d <= MAX (deg p) (deg p') by poly_deg_sub 562 or deg d < CARD M by MAX_LE, LESS_EQ_LESS_TRANS 563 Which contradicts CARD M <= deg d from above. 564*) 565val reduceP_mod_modP_inj_0 = store_thm( 566 "reduceP_mod_modP_inj_0", 567 ``!(r:'a field) k s:num z. FiniteField r /\ mifactor z (unity k) /\ 1 < deg z /\ 568 (forderz X = k) ==> INJ (\p. p % z) PM (Q z)``, 569 rpt (stripDup[FiniteField_def]) >> 570 `Ring r /\ #1 <> #0` by rw[] >> 571 `pmonic z` by rw[] >> 572 `0 < k` by rw[poly_X_order_nonzero] >> 573 qabbrev_tac `u = unity k` >> 574 `(X ** k == |1|) (pm u)` by rw[poly_unity_pmod_eqn, Abbr`u`] >> 575 rw_tac bool_ss[INJ_DEF] >- 576 metis_tac[reduceP_element_mod] >> 577 qabbrev_tac `k = forderz X` >> 578 `?d. d = p - p'` by rw[] >> 579 `poly p /\ poly p' /\ poly d` by metis_tac[reduceP_element_poly, poly_sub_poly] >> 580 Cases_on `d = |0|` >- 581 metis_tac[poly_sub_eq_zero] >> 582 `p IN P /\ p' IN P` by metis_tac[reduceP_subset_setP, SUBSET_DEF] >> 583 `(p == p') (pm z)` by rw[pmod_def_alt] >> 584 `INJ (\n. X ** n % z) M (rootsz (lift d))` by 585 (rw_tac bool_ss[INJ_DEF] >| [ 586 qabbrev_tac `d = p - p'` >> 587 `rootz (lift d) (X ** n % z)` by metis_tac[setP_mod_eq_gives_modN_roots] >> 588 rw[poly_roots_member, poly_deg_mod_less, poly_mod_ring_element], 589 `n < k /\ n' < k` by metis_tac[modN_element_less] >> 590 `(X ** n == X ** n') (pm z)` by rw[pmod_def_alt] >> 591 metis_tac[poly_mod_field_exp_eq_0] 592 ]) >> 593 `Field (PolyModRing r z)` by rw[poly_mod_irreducible_field] >> 594 `polyz (lift d)` by rw[poly_mod_lift_poly] >> 595 `lift d <> |0|z` by metis_tac[poly_lift_eq_zero, poly_zero, poly_ring_property] >> 596 `FINITE (rootsz (lift d))` by rw[poly_roots_finite] >> 597 `CARD M <= CARD (rootsz (lift d))` by metis_tac[INJ_CARD] >> 598 `CARD (rootsz (lift d)) <= degz (lift d)` by metis_tac[poly_roots_count] >> 599 `degz (lift d) = deg d` by rw[poly_mod_lift_deg] >> 600 `CARD M <= deg d` by metis_tac[LESS_EQ_TRANS] >> 601 `deg p < CARD M` by metis_tac[reduceP_element] >> 602 `deg p' < CARD M` by metis_tac[reduceP_element] >> 603 `deg d <= MAX (deg p) (deg p')` by metis_tac[poly_deg_sub] >> 604 `deg d < CARD M` by metis_tac[MAX_LE, LESS_EQ_LESS_TRANS] >> 605 `~(CARD M <= deg d)` by decide_tac); 606(* Not in use now *) 607 608(* Theorem: mifactor z (unity k) /\ (forderz X = k) ==> INJ (\p. p % z) PM (Q z) *) 609(* Proof: 610 Since 0 < deg z by mifactor z (unity k) 611 and monic z ==> pmonic z by notation 612 and 0 < k by poly_X_order_nonzero 613 Let u = unity k, 614 (X ** k == |1|) (pm u) by poly_unity_pmod_eqn, #1 <> #0, 0 < k. 615 By INJ_DEF, this is to show: 616 (1) p IN PM ==> p % h IN Q h 617 True by reduceP_element_mod. 618 (2) p IN PM /\ p' IN PM /\ p % h = p' % h ==> p = p' 619 Let d = p - p'. 620 We have poly p and poly p' by reduceP_element_poly 621 poly d by poly_sub_poly 622 If d = |0|, 623 |0| = p - p' ==> p = p' by poly_sub_eq_zero 624 If d <> |0|, 625 Show that: !n. n IN M ==> X ** n % h is a root of (lift d): 626 p IN P and p' IN P by reduceP_subset_setP, SUBSET_DEF 627 (p == p') (pm z) and (z % z = |0|) by pmod_def_alt 628 Hence !n. n IN M 629 ==> rootz (lift d) (X ** n % h) by setP_mod_eq_gives_modN_roots 630 Next, show that: 631 INJ (\n. X ** n % h) M (rootsz (lift d)) 632 By INJ_DEF, this is to show: 633 (1) X ** n % h IN rootsz (lift d) 634 Since rootz (lift d) (X ** n % h) by above 635 deg (X ** n % h) < deg h by poly_deg_mod_less 636 (X ** n % h) IN Rz by poly_mod_ring_element 637 Hence X ** n % h IN rootsz (lift d) by poly_roots_member 638 (2) n IN M /\ n' IN M /\ X ** n % h = X ** n' % h ==> n = n' 639 n IN M ==> n < k by modN_element_less 640 n' IN M ==> n' < k by modN_element_less 641 X ** n % z = X ** n' % z 642 ==> (X ** n == X ** n') (pm z) by pmod_def_alt 643 Since z <> X by poly_unity_irreducible_factor_not_X 644 Hence n = n' by poly_mod_field_exp_eq_1 645 Apply INJ_CARD: 646 |- !f s t. INJ f s t /\ FINITE t ==> CARD s <= CARD t 647 First show: FINITE (rootsz (lift d)) 648 Since Field (PolyModRing r z) by poly_mod_irreducible_field 649 polyz (lift d) by poly_mod_lift_poly 650 |0|z = [] by poly_ring_property 651 lift d <> |0|z by poly_lift_eq_zero, poly_zero 652 Hence FINITE (rootsz (lift d)) by poly_roots_finite 653 Therefore CARD M <= CARD (rootsz (lift d)) by INJ_CARD 654 Apply poly_roots_count 655 |- !r. Field r ==> !p. poly p /\ p <> |0| ==> CARD (roots p) <= deg p 656 With polyz (lift d) by poly_mod_lift_poly, above 657 lift d <> |0|z by poly_lift_eq_zero, above 658 CARD (rootsz (lift d)) <= degz (lift d) 659 by poly_roots_count 660 But degz (lift d) = deg d by poly_mod_lift_deg 661 Hence CARD M <= deg d by LESS_EQ_TRANS 662 Get a contradiction: 663 p IN PM ==> deg p < CARD M by reduceP_element 664 p' IN PM ==> deg p' < CARD M by reduceP_element 665 deg d <= MAX (deg p) (deg p') by poly_deg_sub 666 or deg d < CARD M by MAX_LE, LESS_EQ_LESS_TRANS 667 Which contradicts CARD M <= deg d from above. 668*) 669val reduceP_mod_modP_inj_1 = store_thm( 670 "reduceP_mod_modP_inj_1", 671 ``!(r:'a field) k s:num z. Field r /\ 0 < k /\ mifactor z (unity k) /\ 672 (forderz X = k) ==> INJ (\p. p % z) PM (Q z)``, 673 rpt strip_tac >> 674 `Ring r /\ #1 <> #0` by rw[] >> 675 `pmonic z` by metis_tac[poly_monic_irreducible_factor] >> 676 qabbrev_tac `u = unity k` >> 677 `(X ** k == |1|) (pm u)` by rw[poly_unity_pmod_eqn, Abbr`u`] >> 678 rw_tac bool_ss[INJ_DEF] >- 679 metis_tac[reduceP_element_mod] >> 680 qabbrev_tac `k = forderz X` >> 681 `?d. d = p - p'` by rw[] >> 682 `poly p /\ poly p' /\ poly d` by metis_tac[reduceP_element_poly, poly_sub_poly] >> 683 Cases_on `d = |0|` >- 684 metis_tac[poly_sub_eq_zero] >> 685 `p IN P /\ p' IN P` by metis_tac[reduceP_subset_setP, SUBSET_DEF] >> 686 `(p == p') (pm z)` by rw[pmod_def_alt] >> 687 `INJ (\n. X ** n % z) M (rootsz (lift d))` by 688 (rw_tac bool_ss[INJ_DEF] >| [ 689 qabbrev_tac `d = p - p'` >> 690 `rootz (lift d) (X ** n % z)` by metis_tac[setP_mod_eq_gives_modN_roots] >> 691 rw[poly_roots_member, poly_deg_mod_less, poly_mod_ring_element], 692 `n < k /\ n' < k` by metis_tac[modN_element_less] >> 693 `(X ** n == X ** n') (pm z)` by rw[pmod_def_alt] >> 694 `z <> X` by metis_tac[poly_unity_irreducible_factor_not_X] >> 695 metis_tac[poly_mod_field_exp_eq_1] 696 ]) >> 697 `Field (PolyModRing r z)` by rw[poly_mod_irreducible_field] >> 698 `polyz (lift d)` by rw[poly_mod_lift_poly] >> 699 `lift d <> |0|z` by metis_tac[poly_lift_eq_zero, poly_zero, poly_ring_property] >> 700 `FINITE (rootsz (lift d))` by rw[poly_roots_finite] >> 701 `CARD M <= CARD (rootsz (lift d))` by metis_tac[INJ_CARD] >> 702 `CARD (rootsz (lift d)) <= degz (lift d)` by metis_tac[poly_roots_count] >> 703 `degz (lift d) = deg d` by rw[poly_mod_lift_deg] >> 704 `CARD M <= deg d` by metis_tac[LESS_EQ_TRANS] >> 705 `deg p < CARD M` by metis_tac[reduceP_element] >> 706 `deg p' < CARD M` by metis_tac[reduceP_element] >> 707 `deg d <= MAX (deg p) (deg p')` by metis_tac[poly_deg_sub] >> 708 `deg d < CARD M` by metis_tac[MAX_LE, LESS_EQ_LESS_TRANS] >> 709 `~(CARD M <= deg d)` by decide_tac); 710(* for Version 1 *) 711 712(* ------------------------------------------------------------------------- *) 713(* Elements of Reduced Set P as roots. *) 714(* ------------------------------------------------------------------------- *) 715 716(* Theorem: 0 < k ==> !m n. n IN N /\ m IN N /\ (n MOD k = m MOD k) ==> 717 !p. p IN P ==> (peval (X ** n - X ** m) p == |0|) (pm (unity k)) *) 718(* Proof: 719 For p IN P, 720 ==> poly q /\ n intro p /\ m intro p by setP_element 721 If #1 = #0, 722 Then |1| = |0| by poly_one_eq_poly_zero 723 But poly (peval (X ** n - X ** m) p) by poly_peval_poly, poly_sub_poly, poly_X_exp 724 so peval (X ** n - X ** m) p = |0| by poly_one_eq_zero 725 Hence true by poly_mod_reflexive 726 If #1 <> #0, 727 Let u = unity k, and pmonic u by poly_unity_pmonic, 0 < k, #1 <> #0 728 Since n MOD k = m MOD k, by given 729 hence (X ** n == X ** m) (pm u) by poly_unity_exp_mod_eq 730 731 We also have: 732 (p ** n == peval p (X ** n)) (pm u) by poly_intro_def 733 (p ** m == peval p (X ** m)) (pm u) by poly_intro_def 734 But (X ** n == X ** m) (pm z) gives 735 (peval p (X ** n) == peval p (X ** m)) (pm u) by poly_peval_mod_eq 736 ==> (p ** n == p ** m) (pm u) by poly_mod_eq_eq 737 ==> (p ** n - p ** m == |0|) (pm u) by poly_pmod_sub_eq_zero 738 peval (X ** n - X ** m) p 739 = (peval (X ** n) p - peval (X ** m) p) by poly_peval_sub 740 = (p ** n - p ** m) by poly_peval_X_exp 741 Hence (peval (X ** n - X ** m) p == |0|) (pm u) 742*) 743val setP_element_as_root_mod_unity = store_thm( 744 "setP_element_as_root_mod_unity", 745 ``!(r:'a ring) k s:num. Ring r /\ 0 < k ==> 746 !n m. n IN N /\ m IN N /\ (n MOD k = m MOD k) ==> 747 !p. p IN P ==> (peval (X ** n - X ** m) p == |0|) (pm (unity k))``, 748 rpt strip_tac >> 749 `poly p /\ n intro p /\ m intro p` by metis_tac[setP_element] >> 750 Cases_on `#1 = #0` >| [ 751 `poly (peval (X ** n - X ** m) p)` by rw[] >> 752 metis_tac[poly_one_eq_poly_zero, poly_one_eq_zero, poly_mod_reflexive], 753 qabbrev_tac `u = unity k` >> 754 `poly X /\ poly (peval p (X ** n)) /\ poly (peval p (X ** m)) /\ poly |1| /\ pmonic u` by rw[poly_unity_pmonic, Abbr`u`] >> 755 `!p. poly p ==> !n. poly (p ** n)` by rw[] >> 756 `(X ** n == X ** m) (pm u)` by metis_tac[poly_unity_exp_mod_eq] >> 757 `(peval p (X ** n) == p ** n) (pm u)` by metis_tac[poly_intro_def, poly_mod_symmetric] >> 758 `(peval p (X ** m) == p ** m) (pm u)` by metis_tac[poly_intro_def, poly_mod_symmetric] >> 759 `(peval p (X ** n) == peval p (X ** m)) (pm u)` by rw[poly_peval_mod_eq] >> 760 `(p ** n == p ** m) (pm u)` by prove_tac[poly_mod_eq_eq] >> 761 `(p ** n - p ** m == |0|) (pm u)` by rw[GSYM poly_pmod_sub_eq_zero] >> 762 `peval (X ** n - X ** m) p = p ** n - p ** m` by rw[poly_peval_sub, poly_peval_X_exp] >> 763 metis_tac[] 764 ]); 765 766(* Theorem: 0 < k /\ mifactor z (unity k) ==> 767 !n m. n IN N /\ m IN N /\ (n MOD k = m MOD k) ==> 768 !p. p IN P ==> (peval (X ** n - X ** m) p == |0|) (pm z) *) 769(* Proof: 770 First, pmonic z, since ipoly z ==> 0 < deg z by poly_irreducible_deg_nonzero 771 For p IN P, 772 ==> poly q /\ n intro p /\ m intro p by setP_element 773 Let u = unity k, and pmonic u by poly_unity_pmonic, 0 < k 774 With the given, 775 (peval (X ** n - X ** m) p == |0|) (pm u) by setP_element_as_root_mod_unity 776 Hence (peval (X ** n - X ** m) p == |0|) (pm z) by poly_mod_eq_divisor 777*) 778val setP_element_as_root_mod_unity_factor = store_thm( 779 "setP_element_as_root_mod_unity_factor", 780 ``!(r:'a field) k s:num z. Field r /\ 0 < k /\ mifactor z (unity k) ==> 781 !n m. n IN N /\ m IN N /\ (n MOD k = m MOD k) ==> 782 !p. p IN P ==> (peval (X ** n - X ** m) p == |0|) (pm z)``, 783 rpt strip_tac >> 784 `Ring r /\ #1 <> #0` by rw[] >> 785 `pmonic z` by metis_tac[poly_monic_irreducible_factor] >> 786 `poly p /\ n intro p /\ m intro p` by metis_tac[setP_element] >> 787 qabbrev_tac `u = unity k` >> 788 `pmonic u` by rw[poly_unity_pmonic, Abbr`u`] >> 789 `(peval (X ** n - X ** m) p == |0|) (pm u)` by metis_tac[setP_element_as_root_mod_unity] >> 790 `poly (peval (X ** n - X ** m) p) /\ poly |0|` by rw[] >> 791 metis_tac[poly_mod_eq_divisor]); 792 793(* Theorem: 0 < k /\ mifactor z (unity k) /\ 1 < deg z ==> 794 !n m. n IN N /\ m IN N /\ (n MOD k = m MOD k) ==> 795 !p. p IN (Q z) ==> rootz (lift (X ** n - X ** m)) p *) 796(* Proof: 797 Note 0 < deg z by 1 < deg z 798 so pmonic z by poly_monic_pmonic 799 and #1 <> #0 by poly_deg_pos_ring_one_ne_zero, 0 < deg z 800 801 For p IN (Q z), there is q IN P such that p = q % z, by modP_element 802 We have: 803 q IN P ==> poly q /\ n intro q by setP_element 804 q IN P ==> poly q /\ m intro q by setP_element 805 806 Let u = unity k, and pmonic u by poly_unity_pmonic, 0 < k, #1 <> #0 807 Since n MOD k = m MOD k, by given 808 Hence (X ** n == X ** m) (pm z) by poly_unity_exp_mod_eq 809 and (peval (X ** n - X ** m) q == |0|) (pm u) by setP_element_as_root_mod_unity 810 or (peval (X ** n - X ** m) q == |0|) (pm z) by poly_mod_eq_divisor 811 Let d = X ** n - X ** m, (peval d q == |0|) (pm z) by above 812 or (peval d q) % z = |0| by pmod_zero 813 Since (peval d p) % z = (peval d q) % z by poly_peval_mod 814 and deg p < deg z by poly_deg_mod_less 815 or p is a root of d, of degree limited by n, m. by poly_mod_lift_root_by_mod_peval 816*) 817val setN_mod_eq_gives_modP_roots_0 = store_thm( 818 "setN_mod_eq_gives_modP_roots_0", 819 ``!(r:'a ring) k s:num z. Ring r /\ 0 < k /\ mifactor z (unity k) /\ 1 < deg z ==> 820 !n m. n IN N /\ m IN N /\ (n MOD k = m MOD k) ==> 821 !p. p IN Q z ==> rootz (lift (X ** n - X ** m)) p``, 822 rpt strip_tac >> 823 `pmonic z` by rw[] >> 824 `0 < deg z` by decide_tac >> 825 `#1 <> #0` by metis_tac[poly_deg_pos_ring_one_ne_zero] >> 826 `!p. poly p ==> !n. poly (p ** n)` by rw[] >> 827 `!p q. poly p /\ poly q ==> poly (peval p q)` by rw[] >> 828 qabbrev_tac `d = X ** n - X ** m` >> 829 `poly X /\ poly d` by rw[Abbr`d`] >> 830 `?q. q IN P /\ (p = q % z)` by rw[GSYM modP_element] >> 831 `poly q` by metis_tac[setP_element] >> 832 `n intro q /\ m intro q` by metis_tac[setP_element] >> 833 qabbrev_tac `u = unity k` >> 834 `pmonic u` by rw[poly_unity_pmonic, Abbr`u`] >> 835 `(peval d q == |0|) (pm u)` by metis_tac[setP_element_as_root_mod_unity] >> 836 `(peval d q == |0|) (pm z)` by metis_tac[poly_mod_eq_divisor, poly_peval_poly, poly_zero_poly] >> 837 `(peval d q) % z = |0|` by rw[GSYM pmod_zero] >> 838 rw[poly_peval_mod, poly_deg_mod_less, poly_mod_lift_root_by_mod_peval]); 839(* Not in use now *) 840 841(* 842Note: setN_mod_eq_gives_modP_roots_0 843|- !r k s z. Ring r /\ 0 < k /\ mifactor z (unity k) /\ 1 < deg z ==> 844 !n m. n IN N /\ m IN N /\ (n MOD k = m MOD k) ==> 845 !p. p IN Q z ==> rootz (lift (X ** n - X ** m)) p 846Note: originally 1 < deg h for pmonic h with 0 < 1 847Now use: poly_irreducible_deg_nonzero |- !r p. Field r /\ ipoly p ==> 0 < deg p 848This needs Field r due to essential use of poly_field_units, which uses properties of inverse. 849*) 850 851(* Theorem: Field r /\ 0 < k /\ mifactor z (unity k) ==> 852 !n m. n IN N /\ m IN N /\ (n MOD k = m MOD k) ==> 853 !p. p IN Q z ==> rootz (lift (X ** n - X ** m)) p *) 854(* Proof: 855 First, pmonic z, since ipoly h ==> 0 < deg z by poly_irreducible_deg_nonzero 856 For p IN Q z, there is q IN P such that p = q % z, by modP_element 857 We have: 858 q IN P ==> poly q /\ n intro q by setP_element 859 q IN P ==> poly q /\ m intro q by setP_element 860 861 Let u = unity k, and pmonic u by poly_unity_pmonic, 0 < k, #1 <> #0 862 Since n MOD k = m MOD k, by given 863 Hence (X ** n == X ** m) (pm u) by poly_unity_exp_mod_eq 864 and (peval (X ** n - X ** m) q == |0|) (pm u) by setP_element_as_root_mod_unity 865 or (peval (X ** n - X ** m) q == |0|) (pm z) by poly_mod_eq_divisor 866 Let d = X ** n - X ** m, 867 Then (peval d q == |0|) (pm z) by above 868 or (peval d q) % z = |0| by pmod_zero 869 Since (peval d p) % z = (peval d q) % z by poly_peval_mod 870 and deg p < deg z by poly_deg_mod_less 871 or p is a root of d, of degree limited by n, m. by poly_mod_lift_root_by_mod_peval 872*) 873val setN_mod_eq_gives_modP_roots_1 = store_thm( 874 "setN_mod_eq_gives_modP_roots_1", 875 ``!(r:'a field) k s:num z. Field r /\ 0 < k /\ mifactor z (unity k) ==> 876 !n m. n IN N /\ m IN N /\ (n MOD k = m MOD k) ==> 877 !p. p IN Q z ==> rootz (lift (X ** n - X ** m)) p``, 878 rpt strip_tac >> 879 `Ring r /\ #1 <> #0` by rw[] >> 880 qabbrev_tac `d = X ** n - X ** m` >> 881 `poly X /\ poly (X ** n) /\ poly (X ** m) /\ poly d` by rw[Abbr`d`] >> 882 `pmonic z` by rw[poly_irreducible_deg_nonzero] >> 883 `?q. q IN P /\ (p = q % z)` by rw[GSYM modP_element] >> 884 `poly q` by metis_tac[setP_element_poly] >> 885 `n intro q /\ m intro q` by metis_tac[setP_element] >> 886 qabbrev_tac `u = unity k` >> 887 `pmonic u` by rw[poly_unity_pmonic, Abbr`u`] >> 888 `(peval d q == |0|) (pm u)` by metis_tac[setP_element_as_root_mod_unity] >> 889 `(peval d q == |0|) (pm z)` by metis_tac[poly_mod_eq_divisor, poly_peval_poly, poly_zero_poly] >> 890 `(peval d q) % z = |0|` by rw[GSYM pmod_zero] >> 891 rw[poly_peval_mod, poly_deg_mod_less, poly_mod_lift_root_by_mod_peval]); 892(* for Version 1 *) 893 894(* Theorem: Field r /\ 0 < k /\ mifactor z (unity k) ==> 895 !n m. n IN N /\ m IN N /\ (n MOD k = m MOD k) ==> 896 (Q z) SUBSET rootsz (lift (X ** n - X ** m)) *) 897(* Proof: 898 Note ipoly z ==> pmonic z by poly_irreducible_pmonic, Field r 899 By poly_roots_member, SUBSET_DEF, this is to show: 900 (1) x IN Q z ==> x IN Rz 901 Note poly x /\ deg x < deg z by modP_element_poly 902 Thus x IN Rz by poly_mod_ring_element 903 (2) x IN Q z ==> rootz (lift (X ** n - X ** m)) x 904 This is true by setN_mod_eq_gives_modP_roots_1 905*) 906val setN_mod_eq_gives_modP_roots_2 = store_thm( 907 "setN_mod_eq_gives_modP_roots_2", 908 ``!r:'a field k s:num z. Field r /\ 0 < k /\ mifactor z (unity k) ==> 909 !n m. n IN N /\ m IN N /\ (n MOD k = m MOD k) ==> 910 (Q z) SUBSET rootsz (lift (X ** n - X ** m))``, 911 rpt strip_tac >> 912 `Ring r` by rw[] >> 913 `pmonic z` by rw[poly_irreducible_pmonic] >> 914 rw_tac std_ss[poly_roots_member, SUBSET_DEF] >- 915 metis_tac[modP_element_poly, poly_mod_ring_element, NOT_ZERO] >> 916 metis_tac[setN_mod_eq_gives_modP_roots_1]); 917 918(* Theorem: 0 < k /\ mifactor z (unity k) ==> 919 !n m. n IN N /\ m IN N /\ (n MOD k = m MOD k) ==> 920 !p. p IN Q z ==> (peval (X ** n - X ** m) p == |0|) (pm z) *) 921(* Proof: 922 First, pmonic z, since ipoly z ==> 0 < deg z by poly_irreducible_deg_nonzero 923 For p IN Q z, there is q IN P such that p = q % z, by modP_element 924 We have: 925 q IN P ==> poly q /\ n intro q by setP_element 926 q IN P ==> poly q /\ m intro q by setP_element 927 928 Let u = unity k, and pmonic u by poly_unity_pmonic, 0 < k, #1 <> #0 929 Since n MOD k = m MOD k, by given 930 Hence (X ** n == X ** m) (pm u) by poly_unity_exp_mod_eq 931 and (peval (X ** n - X ** m) q == |0|) (pm u) by setP_element_as_root_mod_unity 932 or (peval (X ** n - X ** m) q == |0|) (pm z) by poly_mod_eq_divisor 933 Let d = X ** n - X ** m, 934 Then (peval d q == |0|) (pm z) by above 935 Since (peval d p) % h = (peval d q) % z by poly_peval_mod 936 or (peval d p == peval d q) (pm z) by pmod_def_alt 937 Hence (peval d p == |0|) (pm z) by poly_mod_transitive 938*) 939val setN_mod_eq_gives_modP_roots = store_thm( 940 "setN_mod_eq_gives_modP_roots", 941 ``!(r:'a field) k s:num z. Field r /\ 0 < k /\ mifactor z (unity k) ==> 942 !n m. n IN N /\ m IN N /\ (n MOD k = m MOD k) ==> 943 !p. p IN Q z ==> (peval (X ** n - X ** m) p == |0|) (pm z)``, 944 rpt strip_tac >> 945 `Ring r /\ #1 <> #0` by rw[] >> 946 qabbrev_tac `d = X ** n - X ** m` >> 947 `poly X /\ poly (X ** n) /\ poly (X ** m) /\ poly d` by rw[Abbr`d`] >> 948 `pmonic z` by rw[poly_irreducible_deg_nonzero] >> 949 `?q. q IN P /\ (p = q % z)` by rw[GSYM modP_element] >> 950 `poly q` by metis_tac[setP_element_poly] >> 951 `n intro q /\ m intro q` by metis_tac[setP_element] >> 952 qabbrev_tac `u = unity k` >> 953 `pmonic u` by rw[poly_unity_pmonic, Abbr`u`] >> 954 `poly (peval d p) /\ poly (peval d q) /\ poly |0|` by rw[] >> 955 `(peval d q == |0|) (pm u)` by metis_tac[setP_element_as_root_mod_unity] >> 956 `(peval d q == |0|) (pm z)` by metis_tac[poly_mod_eq_divisor] >> 957 `(peval d p == peval d q) (pm z)` by rw[poly_peval_mod, pmod_def_alt] >> 958 metis_tac[poly_mod_transitive]); 959(* for showing root by peval *) 960 961(* ------------------------------------------------------------------------- *) 962(* Injective Map into M *) 963(* ------------------------------------------------------------------------- *) 964 965(* Theorem: mifactor z (unity k) /\ 1 < deg z ==> 966 1 < p /\ 1 < q /\ p IN N /\ q IN N /\ 967 (MAX p q) ** (2 * (SQRT (CARD M))) < CARD (Q z) ==> 968 INJ (\m. m MOD k) (NM p q (SQRT (CARD M))) M *) 969(* Proof: 970 Let t = CARD M. 971 First, since 1 < deg z means 0 < deg z, we have pmonic z. 972 Also p IN N ==> coprime p k by setN_element_coprime 973 With 1 < p, that is p <> 1, k <> 0 by coprime_0R 974 Thus 0 < k. 975 976 By INJ_DEF, this is to show: 977 (1) m IN NM p q (SQRT t) ==> m MOD k IN M 978 m IN NM p q (SQRT t) 979 ==> m IN N by reduceN_element_in_setN 980 ==> m MOD k IN M by setN_element_mod 981 (2) m IN NM p q (SQRT t) /\ m' IN NM p q (SQRT t) ==> m = m' 982 By contradiction. 983 Suppose m <> m', then X ** m <> X ** m' by poly_X_exp_eq 984 Let d = X ** m - X ** m', then d <> |0| by poly_sub_eq_zero 985 m IN NM p q (SQRT t) ==> m IN N by reduceN_element_in_setN 986 m' IN NM p q (SQRT t) ==> m' IN N by reduceN_element_in_setN 987 Hence !p. p IN (Q z) 988 ==> rootz (lift d) p by setN_mod_eq_gives_modP_roots_0 989 Now, poly d ==> polyz (lift d) by poly_mod_lift_poly 990 So (Q z) SUBSET Rz by modP_element_poly 991 Thus (Q z) SUBSET rootsz (lift d) by poly_roots_has_subset 992 Given ipoly z, 993 Field (PolyModRing r z) by poly_mod_irreducible_field 994 Since d <> |0|, 995 lift d <> |0|z by poly_lift_eq_zero, poly_ring_property 996 Thus FINITE (rootsz (lift d)) by poly_roots_finite 997 Hence CARD (Q z) <= CARD (rootsz (lift d)) by CARD_SUBSET 998 Since degz (lift d) = deg d by poly_mod_lift_deg 999 CARD (rootsz (lift d)) <= deg d by poly_roots_count 1000 Now deg d 1001 <= MAX (deg (X ** m) (deg (X ** m') by poly_deg_sub 1002 = MAX m m' by poly_deg_X_exp 1003 Since !m n. m IN NM p q n ==> 1004 m <= (MAX p q) ** (2 * n) by reduceN_element_upper 1005 Thus MAX m m' 1006 <= (MAX p q) ** (2 * SQRT t) by MAX_LE 1007 Overall, 1008 deg d <= (MAX p q) ** (2 * SQRT t) 1009 CARD (Q z) <= (MAX p q) ** (2 * SQRT t) 1010 which contradicts the given: (MAX p q) ** (2 * SQRT t) < CARD (Q z). 1011*) 1012val reduceN_mod_modN_inj_0 = store_thm( 1013 "reduceN_mod_modN_inj_0", 1014 ``!(r:'a field) k s:num z. Field r /\ mifactor z (unity k) /\ 1 < deg z ==> 1015 !p q. 1 < p /\ 1 < q /\ p IN N /\ q IN N /\ 1016 (MAX p q) ** (2 * (SQRT (CARD M))) < CARD (Q z) ==> 1017 INJ (\m. m MOD k) (NM p q (SQRT (CARD M))) M``, 1018 rpt strip_tac >> 1019 `Ring r /\ #1 <> #0` by rw[] >> 1020 `pmonic z` by rw[] >> 1021 qabbrev_tac `t = CARD M` >> 1022 `0 < k` by metis_tac[setN_element_coprime, coprime_0R, LESS_NOT_EQ, NOT_ZERO_LT_ZERO] >> 1023 rw_tac bool_ss[INJ_DEF] >- 1024 metis_tac[reduceN_element_in_setN, setN_element_mod] >> 1025 spose_not_then strip_assume_tac >> 1026 qabbrev_tac `d = X ** m - X ** m'` >> 1027 `poly X /\ poly (X ** m) /\ poly (X ** m') /\ poly d` by rw[Abbr`d`] >> 1028 `d <> |0|` by rw[poly_X_exp_eq, poly_sub_eq_zero, Abbr`d`] >> 1029 `m IN N` by metis_tac[reduceN_element_in_setN] >> 1030 `m' IN N` by metis_tac[reduceN_element_in_setN] >> 1031 `!p. p IN Q z ==> rootz (lift d) p` by metis_tac[setN_mod_eq_gives_modP_roots_0] >> 1032 `polyz (lift d)` by rw[poly_mod_lift_poly] >> 1033 `deg z <> 0` by decide_tac >> 1034 `Q z SUBSET Rz` by prove_tac[modP_element_poly, poly_mod_ring_element, SUBSET_DEF] >> 1035 `Q z SUBSET rootsz (lift d)` by rw[poly_roots_has_subset] >> 1036 `Field (PolyModRing r z)` by rw[poly_mod_irreducible_field] >> 1037 `lift d <> |0|z` by metis_tac[poly_lift_eq_zero, poly_zero, poly_ring_property] >> 1038 `FINITE (rootsz (lift d))` by rw[poly_roots_finite] >> 1039 `CARD (Q z) <= CARD (rootsz (lift d))` by rw[CARD_SUBSET] >> 1040 `degz (lift d) = deg d` by rw[poly_mod_lift_deg] >> 1041 `CARD (rootsz (lift d)) <= deg d` by metis_tac[poly_roots_count] >> 1042 `deg d <= MAX m m'` by metis_tac[poly_deg_sub, poly_deg_X_exp, Abbr`d`] >> 1043 `MAX m m' <= (MAX p q) ** (2 * SQRT t)` by rw[reduceN_element_upper] >> 1044 `~(MAX p q ** (2 * SQRT t) < CARD (Q z))` by decide_tac); 1045(* Not used now *) 1046 1047(* Theorem: mifactor z (unity k) ==> 1 < p /\ 1 < q /\ p IN N /\ q IN N /\ 1048 (MAX p q) ** (2 * (SQRT (CARD M))) < CARD (Q z) ==> 1049 INJ (\m. m MOD k) (NM p q (SQRT (CARD M))) M *) 1050(* Proof: 1051 First, pmonic z, since ipoly z ==> 0 < deg z by poly_irreducible_deg_nonzero 1052 Let t = CARD M. 1053 Since p IN N, coprime p k by setN_element_coprime 1054 Given 1 < p, so p <> 1, hence k <> 0 by coprime_0R 1055 or 0 < k. 1056 By INJ_DEF, this is to show: 1057 (1) m IN NM p q (SQRT t) ==> m MOD k IN M 1058 m IN NM p q (SQRT t) 1059 ==> m IN N by reduceN_element_in_setN 1060 ==> m MOD k IN M by setN_element_mod 1061 (2) m IN NM p q (SQRT t) /\ m' IN NM p q (SQRT t) ==> m = m' 1062 By contradiction. 1063 Suppose m <> m', then X ** m <> X ** m' by poly_X_exp_eq 1064 Let d = X ** m - X ** m', then d <> |0| by poly_sub_eq_zero 1065 m IN NM p q (SQRT t) ==> m IN N by reduceN_element_in_setN 1066 m' IN NM p q (SQRT t) ==> m' IN N by reduceN_element_in_setN 1067 Hence !p. p IN (Q z) 1068 ==> rootz (lift d) p by setN_mod_eq_gives_modP_roots_1 1069 Now, poly d ==> polyz (lift d) by poly_mod_lift_poly 1070 So (Q z) SUBSET Rz by modP_element_poly 1071 Thus (Q z) SUBSET rootsz (lift d) by poly_roots_has_subset 1072 Given ipoly z, 1073 Field (PolyModRing r z) by poly_mod_irreducible_field 1074 Since d <> |0|, 1075 lift d <> |0|z by poly_lift_eq_zero, poly_ring_property 1076 Thus FINITE (rootsz (lift d)) by poly_roots_finite 1077 Hence CARD (Q z) <= CARD (rootsz (lift d)) by CARD_SUBSET 1078 Since degz (lift d) = deg d by poly_mod_lift_deg 1079 CARD (rootsz (lift d)) <= deg d by poly_roots_count 1080 Now deg d 1081 <= MAX (deg (X ** m) (deg (X ** m') by poly_deg_sub 1082 = MAX m m' by poly_deg_X_exp 1083 Since !m n. m IN NM p q n ==> 1084 m <= (MAX p q) ** (2 * n) by reduceN_element_upper 1085 Thus MAX m m' <= (MAX p q) ** (2 * SQRT t) by MAX_LE 1086 Overall, 1087 deg d <= (MAX p q) ** (2 * SQRT t) 1088 CARD (Q z) <= (MAX p q) ** (2 * SQRT t) 1089 which contradicts the given: (MAX p q) ** (2 * SQRT t) < CARD (Q z). 1090*) 1091val reduceN_mod_modN_inj_1 = store_thm( 1092 "reduceN_mod_modN_inj_1", 1093 ``!(r:'a field) k s:num z. Field r /\ mifactor z (unity k) ==> 1094 !p q. 1 < p /\ 1 < q /\ p IN N /\ q IN N /\ 1095 (MAX p q) ** (2 * (SQRT (CARD M))) < CARD (Q z) ==> 1096 INJ (\m. m MOD k) (NM p q (SQRT (CARD M))) M``, 1097 rpt strip_tac >> 1098 `Ring r /\ #1 <> #0` by rw[] >> 1099 `pmonic z` by rw[poly_irreducible_deg_nonzero] >> 1100 `0 < k` by metis_tac[setN_element_coprime, coprime_0R, LESS_NOT_EQ, NOT_ZERO_LT_ZERO] >> 1101 qabbrev_tac `t = CARD M` >> 1102 rw_tac bool_ss[INJ_DEF] >- 1103 metis_tac[reduceN_element_in_setN, setN_element_mod] >> 1104 spose_not_then strip_assume_tac >> 1105 qabbrev_tac `d = X ** m - X ** m'` >> 1106 `poly X /\ poly (X ** m) /\ poly (X ** m') /\ poly d` by rw[Abbr`d`] >> 1107 `d <> |0|` by rw[poly_X_exp_eq, poly_sub_eq_zero, Abbr`d`] >> 1108 `m IN N` by metis_tac[reduceN_element_in_setN] >> 1109 `m' IN N` by metis_tac[reduceN_element_in_setN] >> 1110 `!p. p IN Q z ==> rootz (lift d) p` by metis_tac[setN_mod_eq_gives_modP_roots_1] >> 1111 `polyz (lift d)` by rw[poly_mod_lift_poly] >> 1112 `deg z <> 0` by decide_tac >> 1113 `Q z SUBSET Rz` by prove_tac[modP_element_poly, poly_mod_ring_element, SUBSET_DEF] >> 1114 `Q z SUBSET rootsz (lift d)` by rw[poly_roots_has_subset] >> 1115 `Field (PolyModRing r z)` by rw[poly_mod_irreducible_field] >> 1116 `lift d <> |0|z` by metis_tac[poly_lift_eq_zero, poly_zero, poly_ring_property] >> 1117 `FINITE (rootsz (lift d))` by rw[poly_roots_finite] >> 1118 `CARD (Q z) <= CARD (rootsz (lift d))` by rw[CARD_SUBSET] >> 1119 `degz (lift d) = deg d` by rw[poly_mod_lift_deg] >> 1120 `CARD (rootsz (lift d)) <= deg d` by metis_tac[poly_roots_count] >> 1121 `deg d <= MAX m m'` by metis_tac[poly_deg_sub, poly_deg_X_exp, Abbr`d`] >> 1122 `MAX m m' <= (MAX p q) ** (2 * SQRT t)` by rw[reduceN_element_upper] >> 1123 `~(MAX p q ** (2 * SQRT t) < CARD (Q z))` by decide_tac); 1124 1125(* Theorem: mifactor z (unity k) ==> 1126 !p q. 1 < p /\ 1 < q /\ p IN N /\ q IN N /\ (p * q) ** (SQRT (CARD M)) < CARD (Q z) ==> 1127 INJ (\m. m MOD k) (NM p q (SQRT (CARD M))) M *) 1128(* Proof: 1129 First, pmonic z, since ipoly z ==> 0 < deg z by poly_irreducible_deg_nonzero 1130 Let t = CARD M. 1131 Since p IN N, coprime p k by setN_element_coprime 1132 Given 1 < p, so p <> 1, hence k <> 0, or 0 < k by coprime_0R 1133 By INJ_DEF, this is to show: 1134 (1) m IN NM p q (SQRT t) ==> m MOD k IN M 1135 m IN NM p q (SQRT t) 1136 ==> m IN N by reduceN_element_in_setN 1137 ==> m MOD k IN M by setN_element_mod 1138 (2) m IN NM p q (SQRT t) /\ m' IN NM p q (SQRT t) ==> m = m' 1139 By contradiction. 1140 Suppose m <> m', then X ** m <> X ** m' by poly_X_exp_eq 1141 Let d = X ** m - X ** m', then d <> |0| by poly_sub_eq_zero 1142 m IN NM p q (SQRT t) ==> m IN N by reduceN_element_in_setN 1143 m' IN NM p q (SQRT t) ==> m' IN N by reduceN_element_in_setN 1144 Hence !p. p IN (Q z) 1145 ==> rootz (lift d) p by setN_mod_eq_gives_modP_roots_1 1146 Now, poly d ==> polyz (lift d) by poly_mod_lift_poly 1147 So (Q z) SUBSET Rz by modP_element_poly 1148 Thus (Q z) SUBSET rootsz (lift d) by poly_roots_has_subset 1149 Given ipoly z, 1150 Field (PolyModRing r z) by poly_mod_irreducible_field 1151 Since d <> |0|, 1152 lift d <> |0|z by poly_lift_eq_zero, poly_ring_property 1153 Thus FINITE (rootsz (lift d)) by poly_roots_finite 1154 Hence CARD (Q z) <= CARD (rootsz (lift d)) by CARD_SUBSET 1155 Since degz (lift d) = deg d by poly_mod_lift_deg 1156 CARD (rootsz (lift d)) <= deg d by poly_roots_count 1157 Now deg d <= MAX (deg (X ** m) (deg (X ** m') by poly_deg_sub 1158 = MAX m m' by poly_deg_X_exp 1159 Since !m n. m IN NM p q n ==> m <= (p * q) ** n by reduceN_element_upper_better 1160 Thus MAX m m' <= (p * q) ** (SQRT t) by MAX_LE 1161 Overall, 1162 deg d <= (p * q) ** (SQRT t) 1163 CARD (Q z) <= (p * q) ** (SQRT t) 1164 which contradicts the given: (p * q) ** (SQRT t) < CARD (Q z). 1165*) 1166val reduceN_mod_modN_inj_2 = store_thm( 1167 "reduceN_mod_modN_inj_2", 1168 ``!(r:'a field) k s:num z. Field r /\ mifactor z (unity k) ==> 1169 !p q. 1 < p /\ 1 < q /\ p IN N /\ q IN N /\ 1170 (p * q) ** (SQRT (CARD M)) < CARD (Q z) ==> 1171 INJ (\m. m MOD k) (NM p q (SQRT (CARD M))) M``, 1172 rpt strip_tac >> 1173 `Ring r /\ #1 <> #0` by rw[] >> 1174 `pmonic z` by rw[poly_irreducible_deg_nonzero] >> 1175 `0 < k` by metis_tac[setN_element_coprime, coprime_0R, LESS_NOT_EQ, NOT_ZERO_LT_ZERO] >> 1176 qabbrev_tac `t = CARD M` >> 1177 rw_tac bool_ss[INJ_DEF] >- 1178 metis_tac[reduceN_element_in_setN, setN_element_mod] >> 1179 spose_not_then strip_assume_tac >> 1180 qabbrev_tac `d = X ** m - X ** m'` >> 1181 `poly X /\ poly (X ** m) /\ poly (X ** m') /\ poly d` by rw[Abbr`d`] >> 1182 `d <> |0|` by rw[poly_X_exp_eq, poly_sub_eq_zero, Abbr`d`] >> 1183 `m IN N` by metis_tac[reduceN_element_in_setN] >> 1184 `m' IN N` by metis_tac[reduceN_element_in_setN] >> 1185 `!p. p IN Q z ==> rootz (lift d) p` by metis_tac[setN_mod_eq_gives_modP_roots_1] >> 1186 `polyz (lift d)` by rw[poly_mod_lift_poly] >> 1187 `deg z <> 0` by decide_tac >> 1188 `Q z SUBSET Rz` by prove_tac[modP_element_poly, poly_mod_ring_element, SUBSET_DEF] >> 1189 `Q z SUBSET rootsz (lift d)` by rw[poly_roots_has_subset] >> 1190 `Field (PolyModRing r z)` by rw[poly_mod_irreducible_field] >> 1191 `lift d <> |0|z` by metis_tac[poly_lift_eq_zero, poly_zero, poly_ring_property] >> 1192 `FINITE (rootsz (lift d))` by rw[poly_roots_finite] >> 1193 `CARD (Q z) <= CARD (rootsz (lift d))` by rw[CARD_SUBSET] >> 1194 `degz (lift d) = deg d` by rw[poly_mod_lift_deg] >> 1195 `CARD (rootsz (lift d)) <= deg d` by metis_tac[poly_roots_count] >> 1196 `deg d <= MAX m m'` by metis_tac[poly_deg_sub, poly_deg_X_exp, Abbr`d`] >> 1197 `MAX m m' <= (p * q) ** (SQRT t)` by rw[reduceN_element_upper_better] >> 1198 `~((p * q) ** (SQRT t) < CARD (Q z))` by decide_tac); 1199 1200(* ------------------------------------------------------------------------- *) 1201(* Polynomial Product map to Power set of Monomials *) 1202(* ------------------------------------------------------------------------- *) 1203 1204(* Theorem: t SUBSET (IMAGE SUC (count s)) ==> (IMAGE (\c. X + |c|) t) SUBSET P *) 1205(* Proof: 1206 By setP_def and SUBSET_DEF, this is to show: 1207 (1) poly (X + |c|) 1208 True by poly_X_add_c. 1209 (2) m IN N ==> m intro X + |c| 1210 ?n. (c = SUC n) /\ n < s by the given condition 1211 Hence 0 < c and c = SUC n <= s, 1212 Thus true by setN_element. 1213*) 1214val set_of_X_add_c_subset_setP_0 = store_thm( 1215 "set_of_X_add_c_subset_setP_0", 1216 ``!(r:'a ring) k s:num. Ring r ==> 1217 !t. t SUBSET (IMAGE SUC (count s)) ==> (IMAGE (\c. X + |c|) t) SUBSET P``, 1218 rw[setP_def, SUBSET_DEF] >- 1219 rw[] >> 1220 `?n. (c = SUC n) /\ n < s` by rw[] >> 1221 `0 < c /\ c <= s` by decide_tac >> 1222 metis_tac[setN_element]); 1223 1224(* Theorem: t SUBSET (IMAGE SUC (count (MIN s h))) ==> (IMAGE (\c. X + |c|) t) SUBSET P *) 1225(* Proof: 1226 By setP_def and SUBSET_DEF, this is to show: 1227 (1) poly (X + |c|) 1228 True by poly_X_add_c. 1229 (2) m IN N ==> m intro X + |c| 1230 ?n. (c = SUC n) /\ n < s /\ n < CARD M by the given condition 1231 Hence 0 < c and SUC n < SUC s, or c <= s, 1232 Thus true by setN_element. 1233*) 1234val set_of_X_add_c_subset_setP = store_thm( 1235 "set_of_X_add_c_subset_setP", 1236 ``!(r:'a ring) k s:num. Ring r ==> 1237 !h t. t SUBSET (IMAGE SUC (count (MIN s h))) ==> (IMAGE (\c. X + |c|) t) SUBSET P``, 1238 rw[setP_def, SUBSET_DEF] >- 1239 rw[] >> 1240 `?n. (c = SUC n) /\ n < s /\ n < h` by rw[] >> 1241 `0 < c /\ c <= s` by decide_tac >> 1242 metis_tac[setN_element]); 1243 1244(* Theorem: Ring r /\ 0 < k ==> !t. FINITE t /\ t SUBSET P ==> PPROD t IN P *) 1245(* Proof: 1246 By complete induction on t. 1247 If t = {}, 1248 PPROD {} = |1| by poly_prod_set_empty 1249 and |1| IN P by setP_has_one, 0 < k 1250 Hence true. 1251 If t <> {}, 1252 t = (CHOICE t) INSERT (REST t) by CHOICE_INSERT_REST 1253 PPROD t 1254 = PPROD ((CHOICE t) INSERT (REST t)) 1255 = (CHOICE t) * PPROD z ((REST t) DELETE (CHOICE t) by poly_prod_set_thm 1256 = (CHOICE t) * PPROD z (REST t by CHOICE_NOT_IN_REST, DELETE_NON_ELEMENT 1257 Since (CHOICE t) IN t by CHOICE_DEF 1258 and t SUBSET P by given 1259 (CHOICE t) IN P by SUBSET_DEF 1260 also PPROD z (REST t) IN P by induction hypothesis 1261 !p. p IN P ==> poly p ==> p IN (PolyRing r).carrier by setP_element_poly, poly_ring_element 1262 Hence (CHOICE t) * PPROD z (REST t) IN P by setP_closure 1263*) 1264val poly_prod_set_in_setP = store_thm( 1265 "poly_prod_set_in_setP", 1266 ``!(r:'a ring) k s:num. Ring r /\ 0 < k ==> 1267 !t. FINITE t /\ t SUBSET P ==> PPROD t IN P``, 1268 rpt strip_tac >> 1269 completeInduct_on `CARD t` >> 1270 rule_assum_tac(SIMP_RULE bool_ss[GSYM RIGHT_FORALL_IMP_THM, AND_IMP_INTRO]) >> 1271 rw_tac std_ss[] >> 1272 Cases_on `t = {}` >- 1273 rw[poly_prod_set_empty, setP_has_one] >> 1274 `t = (CHOICE t) INSERT (REST t)` by rw[CHOICE_INSERT_REST] >> 1275 `CHOICE t IN t` by rw[CHOICE_DEF] >> 1276 `CHOICE t IN P` by metis_tac[SUBSET_DEF] >> 1277 `CARD (REST t) < CARD t` by rw[CARD_REST, DECIDE ``!n. n <> 0 ==> n - 1 < n``] >> 1278 `(REST t) SUBSET P` by metis_tac[REST_SUBSET, SUBSET_TRANS] >> 1279 `PPROD (REST t) IN P` by rw[] >> 1280 `poly (CHOICE t)` by metis_tac[setP_element_poly] >> 1281 `P SUBSET (PolyRing r).carrier` by metis_tac[setP_element_poly, poly_ring_element, SUBSET_DEF] >> 1282 `(REST t) SUBSET (PolyRing r).carrier` by metis_tac[SUBSET_TRANS] >> 1283 `!p. p IN (REST t) ==> poly p` by metis_tac[poly_ring_element, SUBSET_DEF] >> 1284 `PPROD t = PPROD ((CHOICE t) INSERT (REST t))` by metis_tac[] >> 1285 `_ = (CHOICE t) * PPROD ((REST t) DELETE (CHOICE t))` by rw[poly_prod_set_thm] >> 1286 `_ = (CHOICE t) * PPROD (REST t)` by metis_tac[CHOICE_NOT_IN_REST, DELETE_NON_ELEMENT] >> 1287 rw[setP_closure]); 1288 1289(* 1290INSERT_SUBSET; 1291val it = |- !x s t. x INSERT s SUBSET t <=> x IN t /\ s SUBSET t: thm 1292CARD_INSERT; 1293val it = |- !s. FINITE s ==> !x. CARD (x INSERT s) = if x IN s then CARD s else SUC (CARD s): thm 1294*) 1295 1296(* The idea: 1297Let p = |0|. 1298 Then p NOTIN (PPM (MIN s (CARD M))) by reduceP_poly_has_no_zero 1299Since p IN PM by reduceP_has_zero 1300 and (PPM (MIN s (CARD M))) SUBSET PM, 1301Hence (p INSERT (PPM (MIN s (CARD M)))) SUBSET SUBSET PM. 1302But CARD (p INSERT (PPM (MIN s (CARD M)))) 1303 = SUC (CARD (PPM (MIN s (CARD M)))) since p NOTIN the set, 1304 = SUC (PRE (2 ** MIN s (CARD M)))) by reduceP_poly_card 1305 = 2 ** MIN s (CARD M)) by SUC_PRE 1306*) 1307 1308(* Theorem: 0 < k /\ s < CARD M /\ CARD M < char r ==> PPM s SUBSET PM *) 1309(* Proof: 1310 Note char r <> 1 by s < CARD M /\ CARD M < char r 1311 Thus #1 <> #0 by ring_char_eq_1 1312 This is to show: 1313 s' IN PPOW (IMAGE SUC (count s)) ==> 1314 PPROD (IMAGE (\c. X + |c|) s') IN PM 1315 s' IN PPOW (IMAGE SUC (count s)) 1316 ==> s' PSUBSET (IMAGE SUC (count s)) by IN_PPOW 1317 ==> s' SUBSET (IMAGE SUC (count s)) by PSUBSET_DEF 1318 Since FINITE (count s) by FINITE_COUNT 1319 so FINITE (IMAGE SUC (count s)) by IMAGE_FINITE 1320 and FINITE s' by SUBSET_FINITE 1321 To show IN PM, 1322 (1) PPROD (IMAGE (\c. X + |c|) s') IN P 1323 Since s' SUBSET (IMAGE SUC (count s)) 1324 IMAGE (\c. X + |c|) s' SUBSET P by set_of_X_add_c_subset_setP_0 1325 and FINITE (IMAGE (\c. X + |c|) s') by IMAGE_FINITE 1326 Now by poly_prod_set_in_setP, 1327 !t. FINITE t /\ t SUBSET P ==> PPROD t IN P 1328 Hence true. 1329 (2) deg (PPROD (IMAGE (\c. X + |c|) s')) < CARD M 1330 Since FINITE (IMAGE SUC (count s)) 1331 and FINITE s', this gives: 1332 MAX_SET s' <= MAX_SET (IMAGE SUC (count s)) by SUBSET_MAX_SET 1333 Since MAX_SET (IMAGE SUC (count s)) 1334 = s by MAX_SET_IMAGE_SUC_COUNT 1335 < char r by given 1336 we have MAX_SET s' < char r 1337 Therefore, 1338 deg (PPROD (IMAGE (\c. X + |c|) s')) = CARD s' by poly_prod_set_image_X_add_c_deg, #1 <> #0 1339 Let q = PPROD (IMAGE (\c. X + |c|) s') 1340 This is to show: deg q < CARD M 1341 Now, since SUC is injective, 1342 CARD (IMAGE SUC (count s)) 1343 = CARD (count s) by FINITE_CARD_IMAGE 1344 = s by CARD_COUNT 1345 < CARD M by given 1346 Since s' PSUBSET IMAGE SUC count s) 1347 Hence CARD s' < CARD (IMAGE SUC (count s)) by CARD_PSUBSET 1348 Therefore deg (PPROD (IMAGE (\c. X + |c|) s')) < CARD M. 1349*) 1350val reduceP_poly_subset_reduceP_0 = store_thm( 1351 "reduceP_poly_subset_reduceP_0", 1352 ``!(r:'a ring) k s. Ring r /\ 0 < k /\ s < CARD M /\ CARD M < char r ==> 1353 PPM s SUBSET PM``, 1354 rpt strip_tac >> 1355 `char r <> 1` by decide_tac >> 1356 `#1 <> #0` by rw[GSYM ring_char_eq_1] >> 1357 rw_tac std_ss[reduceP_poly_def, SUBSET_DEF, IN_IMAGE] >> 1358 `s' PSUBSET (IMAGE SUC (count s))` by rw[GSYM IN_PPOW] >> 1359 `s' SUBSET (IMAGE SUC (count s))` by metis_tac[PSUBSET_DEF] >> 1360 `FINITE (IMAGE SUC (count s))` by rw[] >> 1361 `FINITE s'` by metis_tac[SUBSET_FINITE] >> 1362 rw_tac std_ss[reduceP_element] >| [ 1363 `IMAGE (\c. X + |c|) s' SUBSET P` by metis_tac[set_of_X_add_c_subset_setP_0] >> 1364 `FINITE (IMAGE (\c. X + |c|) s')` by metis_tac[IMAGE_FINITE] >> 1365 rw[poly_prod_set_in_setP], 1366 `MAX_SET s' <= MAX_SET (IMAGE SUC (count s))` by rw[SUBSET_MAX_SET] >> 1367 `MAX_SET (IMAGE SUC (count s)) = s` by rw[MAX_SET_IMAGE_SUC_COUNT] >> 1368 `MAX_SET s' < char r` by decide_tac >> 1369 `deg (PPROD (IMAGE (\c. X + |c|) s')) = CARD s'` by rw[poly_prod_set_image_X_add_c_deg] >> 1370 qabbrev_tac `q = PPROD (IMAGE (\c. X + |c|) s')` >> 1371 `CARD (IMAGE SUC (count s)) = s` by rw[FINITE_CARD_IMAGE] >> 1372 `CARD s' < CARD (IMAGE SUC (count s))` by rw[CARD_PSUBSET] >> 1373 decide_tac 1374 ]); 1375 1376(* 1377The theorem above is reasonable, since PPM s takes (X + 1) ... (X + s) to form products. 1378If s >= CARD M, then the product will have degree >= CARD M, not an element of PM. 1379 1380The theorem above is not very useful, as we cannot confirm s < CARD M. 1381Later, s = SQRT (phi k) * ulog n is fixed, but only known to be s <= phi k. 1382Also, the best one can show is that CARD M <= phi k, 1383so it is possible, but not necessarily, that s < CARD M. 1384 1385*) 1386 1387(* 1388reduceP_def |- !r k s. PM = {p | p IN P /\ deg p < CARD M} 1389reduceP_poly_def |- !r n. PPM n = IMAGE (\s. PPIMAGE (\c. X + |c|) s) (PPOW (natural n)) 1390*) 1391 1392(* Theorem: 0 < k /\ 0 < s /\ s < char r ==> PPM (MIN s (CARD M)) SUBSET PM *) 1393(* Proof: 1394 Note char r <> 1 by 0 < s /\ s < char r 1395 Thus #1 <> #0 by ring_char_eq_1 1396 Let t = CARD M, and z = MIN s t. 1397 Note z <= s, and z <= t by MIN_DEF 1398 This is to show: 1399 s' IN PPOW (IMAGE SUC (count z)) ==> 1400 PPROD (IMAGE (\c. X + |c|) s') IN PM 1401 s' IN PPOW (IMAGE SUC (count z)) 1402 ==> s' PSUBSET (IMAGE SUC (count z)) by IN_PPOW 1403 ==> s' SUBSET (IMAGE SUC (count z)) by PSUBSET_DEF 1404 Since FINITE (count z) by FINITE_COUNT 1405 so FINITE (IMAGE SUC (count z)) by IMAGE_FINITE 1406 and FINITE s' by SUBSET_FINITE 1407 To show IN PM, 1408 (1) PPROD (IMAGE (\c. X + |c|) s') IN P 1409 Since s' SUBSET (IMAGE SUC (count z)) 1410 IMAGE (\c. X + |c|) s' SUBSET P by set_of_X_add_c_subset_setP 1411 and FINITE (IMAGE (\c. X + |c|) s') by IMAGE_FINITE 1412 Now by poly_prod_set_in_setP, 1413 !t. FINITE t /\ t SUBSET P ==> PPROD t IN P 1414 Hence true. 1415 (2) deg (PPROD (IMAGE (\c. X + |c|) s')) < t 1416 Since FINITE (IMAGE SUC (count z)) 1417 and FINITE s', this gives: 1418 MAX_SET s' <= MAX_SET (IMAGE SUC (count z)) by SUBSET_MAX_SET 1419 Since MAX_SET (IMAGE SUC (count z)) 1420 = z by MAX_SET_IMAGE_SUC_COUNT 1421 <= s < char r by given 1422 we have MAX_SET s' < char r 1423 Therefore, 1424 deg (PPROD (IMAGE (\c. X + |c|) s')) = CARD s' by poly_prod_set_image_X_add_c_deg 1425 Let q = PPROD (IMAGE (\c. X + |c|) s') 1426 This is to show: deg q < CARD M 1427 Now, since SUC is injective, 1428 CARD (IMAGE SUC (count z)) 1429 = CARD (count z) by FINITE_CARD_IMAGE 1430 = z by CARD_COUNT 1431 Since s' PSUBSET IMAGE SUC count z) 1432 Hence CARD s' < CARD (IMAGE SUC (count z)) by CARD_PSUBSET 1433 Therefore deg (PPROD (IMAGE (\c. X + |c|) s')) < z <= t. 1434*) 1435val reduceP_poly_subset_reduceP = store_thm( 1436 "reduceP_poly_subset_reduceP", 1437 ``!(r:'a ring) k s:num. Ring r /\ 0 < k /\ 0 < s /\ s < char r ==> 1438 PPM (MIN s (CARD M)) SUBSET PM``, 1439 rpt strip_tac >> 1440 `char r <> 1` by decide_tac >> 1441 `#1 <> #0` by rw[GSYM ring_char_eq_1] >> 1442 qabbrev_tac `t = CARD M` >> 1443 qabbrev_tac `z = MIN s t` >> 1444 `z <= s /\ z <= t` by rw[Abbr`z`, Abbr`t`] >> 1445 rw_tac std_ss[reduceP_poly_def, SUBSET_DEF, IN_IMAGE] >> 1446 `s' PSUBSET (IMAGE SUC (count z))` by rw[GSYM IN_PPOW] >> 1447 `s' SUBSET (IMAGE SUC (count z))` by metis_tac[PSUBSET_DEF] >> 1448 `FINITE (IMAGE SUC (count z))` by rw[] >> 1449 `FINITE s'` by metis_tac[SUBSET_FINITE] >> 1450 rw_tac std_ss[reduceP_element] >| [ 1451 `IMAGE (\c. X + |c|) s' SUBSET P` by metis_tac[set_of_X_add_c_subset_setP] >> 1452 `FINITE (IMAGE (\c. X + |c|) s')` by metis_tac[IMAGE_FINITE] >> 1453 rw[poly_prod_set_in_setP], 1454 `MAX_SET s' <= MAX_SET (IMAGE SUC (count z))` by rw[SUBSET_MAX_SET] >> 1455 `MAX_SET (IMAGE SUC (count z)) = z` by rw[MAX_SET_IMAGE_SUC_COUNT] >> 1456 `MAX_SET s' < char r` by decide_tac >> 1457 `deg (PPROD (IMAGE (\c. X + |c|) s')) = CARD s'` by rw[poly_prod_set_image_X_add_c_deg] >> 1458 qabbrev_tac `q = PPROD (IMAGE (\c. X + |c|) s')` >> 1459 `CARD (IMAGE SUC (count z)) = z` by rw[FINITE_CARD_IMAGE] >> 1460 `CARD s' < CARD (IMAGE SUC (count z))` by rw[CARD_PSUBSET] >> 1461 decide_tac 1462 ]); 1463 1464(* ------------------------------------------------------------------------- *) 1465(* Lower Bound for (Q z) by Combinatorics *) 1466(* ------------------------------------------------------------------------- *) 1467 1468(* Theorem: mifactor z (unity k) /\ 1 < deg z /\ 1469 (forderz X = k) /\ s < char r ==> 2 ** (MIN s (CARD M)) <= CARD (Q z) *) 1470(* Proof: 1471 First, 1 < k by poly_X_order_gt_1, hence 0 < k. 1472 Let n = MIN s (CARD M). 1473 1474 Given the conditions, 1475 INJ (\p. p % z) PM (Q z) by reduceP_mod_modP_inj_0 1476 Now, FINITE (Q z) by modP_finite 1477 Hence FINITE PM by FINITE_INJ 1478 and CARD PM <= CARD (Q z) by INJ_CARD 1479 But PPM n SUBSET PM by reduceP_poly_subset_reduceP, 0 < k, 0 < s, s < char r. 1480 and |0| IN PM by reduceP_has_zero, 1 < k. 1481 Hence ( |0| INSERT PPM n) SUBSET PM by INSERT_SUBSET 1482 So CARD ( |0| INSERT PPM n) <= CARD PM by CARD_SUBSET 1483 Since |0| NOTIN PPM n by reduceP_poly_has_no_zero 1484 and FINITE (PPM n) by reduceP_poly_finite 1485 CARD ( |0| INSERT PPM n) 1486 = SUC (CARD (PPM n)) by CARD_INSERT, since p NOTIN the set 1487 = SUC (PRE (2 ** n)) by reduceP_poly_card 1488 = 2 ** n by SUC_PRE, with 0 < 2 ** n by ZERO_LT_EXP. 1489 Hence 2 ** n <= CARD (Q z) by LESS_EQ_TRANS 1490*) 1491val modP_card_lower_0 = store_thm( 1492 "modP_card_lower_0", 1493 ``!(r:'a field) k s z. FiniteField r /\ mifactor z (unity k) /\ 1 < deg z /\ 1494 (forderz X = k) /\ 0 < s /\ s < char r ==> 2 ** (MIN s (CARD M)) <= CARD (Q z)``, 1495 rpt (stripDup[FiniteField_def]) >> 1496 `Ring r /\ #1 <> #0` by rw[] >> 1497 `FiniteRing r` by rw[FiniteRing_def] >> 1498 `pmonic z` by metis_tac[poly_monic_irreducible_factor] >> 1499 `INJ (\p. p % z) PM (Q z)` by rw[reduceP_mod_modP_inj_0] >> 1500 `FINITE (Q z)` by rw[modP_finite, DECIDE``0 < 1``] >> 1501 `FINITE PM` by rw[reduceP_finite] >> 1502 `CARD PM <= CARD (Q z)` by metis_tac[INJ_CARD] >> 1503 `1 < k` by rw[poly_X_order_gt_1] >> 1504 `|0| IN PM` by rw[reduceP_has_zero] >> 1505 qabbrev_tac `n = MIN s (CARD M)` >> 1506 `0 < k` by decide_tac >> 1507 `PPM n SUBSET PM` by rw[reduceP_poly_subset_reduceP, Abbr`n`] >> 1508 `( |0| INSERT PPM n) SUBSET PM` by rw[INSERT_SUBSET] >> 1509 `CARD ( |0| INSERT PPM n) <= CARD PM` by rw[CARD_SUBSET] >> 1510 `n <= s` by rw[Abbr`n`] >> 1511 `n < char r` by decide_tac >> 1512 `|0| NOTIN PPM n` by rw[reduceP_poly_has_no_zero] >> 1513 `FINITE (PPM n)` by rw[reduceP_poly_finite] >> 1514 `CARD ( |0| INSERT PPM n) = SUC (CARD (PPM n))` by metis_tac[CARD_INSERT] >> 1515 `_ = SUC (PRE (2 ** n))` by rw[reduceP_poly_card] >> 1516 `_ = 2 ** n` by metis_tac[SUC_PRE, ZERO_LT_EXP, DECIDE``0 < 2``] >> 1517 decide_tac); 1518(* Not in use now *) 1519 1520(* Theorem: mifactor z (unity k) /\ (forderz X = k) /\ 1521 1 < k /\ 0 < s /\ s < char r ==> 2 ** (MIN s (CARD M)) <= CARD (Q z) *) 1522(* Proof: 1523 First, 1 < k by given, hence 0 < k. 1524 Let n = MIN s (CARD M). 1525 1526 Given the conditions, 1527 INJ (\p. p % z) PM (Q z) by reduceP_mod_modP_inj_1, 0 < k. 1528 Now, FINITE (Q z) by modP_finite 1529 Hence FINITE PM by FINITE_INJ 1530 and CARD PM <= CARD (Q z) by INJ_CARD 1531 But PPM n SUBSET PM by reduceP_poly_subset_reduceP, 0 < k, 0 < s, s < char r. 1532 and |0| IN PM by reduceP_has_zero, 1 < k. 1533 Hence ( |0| INSERT PPM n) SUBSET PM by INSERT_SUBSET 1534 So CARD ( |0| INSERT PPM n) <= CARD PM by CARD_SUBSET 1535 Since |0| NOTIN PPM n by reduceP_poly_has_no_zero 1536 and FINITE (PPM n) by reduceP_poly_finite 1537 CARD ( |0| INSERT PPM n) 1538 = SUC (CARD (PPM n)) by CARD_INSERT, since p NOTIN the set 1539 = SUC (PRE (2 ** n)) by reduceP_poly_card 1540 = 2 ** n by SUC_PRE, with 0 < 2 ** n by ZERO_LT_EXP. 1541 Hence 2 ** n <= CARD (Q z) by LESS_EQ_TRANS 1542*) 1543val modP_card_lower_1 = store_thm( 1544 "modP_card_lower_1", 1545 ``!(r:'a field) k s:num z. FiniteField r /\ mifactor z (unity k) /\ (forderz X = k) /\ 1546 1 < k /\ 0 < s /\ s < char r ==> 2 ** (MIN s (CARD M)) <= CARD (Q z)``, 1547 rpt (stripDup[FiniteField_def]) >> 1548 `Ring r /\ #1 <> #0` by rw[] >> 1549 `FiniteRing r` by rw[FiniteRing_def] >> 1550 `pmonic z` by metis_tac[poly_monic_irreducible_factor] >> 1551 `0 < k` by decide_tac >> 1552 `INJ (\p. p % z) PM (Q z)` by rw[reduceP_mod_modP_inj_1] >> 1553 `FINITE (Q z)` by rw[modP_finite] >> 1554 `FINITE PM` by rw[reduceP_finite] >> 1555 `CARD PM <= CARD (Q z)` by metis_tac[INJ_CARD] >> 1556 `|0| IN PM` by rw[reduceP_has_zero] >> 1557 qabbrev_tac `n = MIN s (CARD M)` >> 1558 `PPM n SUBSET PM` by rw[reduceP_poly_subset_reduceP, Abbr`n`] >> 1559 `( |0| INSERT PPM n) SUBSET PM` by rw[INSERT_SUBSET] >> 1560 `CARD ( |0| INSERT PPM n) <= CARD PM` by rw[CARD_SUBSET] >> 1561 `n <= s` by rw[Abbr`n`] >> 1562 `n < char r` by decide_tac >> 1563 `|0| NOTIN PPM n` by rw[reduceP_poly_has_no_zero] >> 1564 `FINITE (PPM n)` by rw[reduceP_poly_finite] >> 1565 `CARD ( |0| INSERT PPM n) = SUC (CARD (PPM n))` by metis_tac[CARD_INSERT] >> 1566 `_ = SUC (PRE (2 ** n))` by rw[reduceP_poly_card] >> 1567 `_ = 2 ** n` by metis_tac[SUC_PRE, ZERO_LT_EXP, DECIDE``0 < 2``] >> 1568 decide_tac); 1569(* for version 1 *) 1570 1571(* ------------------------------------------------------------------------- *) 1572(* Improvements for Version 2 *) 1573(* ------------------------------------------------------------------------- *) 1574 1575(* Theorem: poly p /\ deg p < deg z /\ p <> |0| /\ p <> |1| ==> 1576 !k. prime k /\ (p ** k == |1|) (pm z) ==> (forderz p = k) *) 1577(* Proof: 1578 Let h = forderz p. 1579 First, (PolyModRing r z).sum.id = |0| by poly_mod_ring_ids 1580 and ((PolyModRing r z).prod excluding |0|).id = |1| by poly_mod_prod_nonzero_id 1581 Now, FiniteField (PolyModRing r z) by poly_mod_irreducible_finite_field 1582 and FiniteGroup ((PolyModRing r z).prod excluding |0|) by finite_field_alt 1583 Since deg p < deg z and p <> |0| by given 1584 p IN ((PolyModRing r z).prod excluding |0|).carrier by poly_mod_ring_property, excluding_def 1585 Hence ((PolyModRing r z).prod excluding |0|).exp p k 1586 = (p ** k) % z by poly_mod_exp_alt 1587 = |1| % z by pmod_def_alt 1588 = |1| by poly_mod_one 1589 1590 Therefore h divides k by group_order_condition 1591 which means h = 1, or h = k by prime_def 1592 But h = 1 ==> p = |1| by group_order_eq_1 1593 which is excluded by p <> |1|. 1594*) 1595val poly_order_prime_condition_0 = store_thm( 1596 "poly_order_prime_condition_0", 1597 ``!r:'a field. Field r ==> !z. monic z /\ ipoly z ==> 1598 !p. poly p /\ deg p < deg z /\ p <> |0| /\ p <> |1| ==> 1599 !k. prime k /\ (p ** k == |1|) (pm z) ==> (forderz p = k)``, 1600 rpt strip_tac >> 1601 `Ring r /\ #1 <> #0` by rw[] >> 1602 `0 < deg z` by rw[poly_irreducible_deg_nonzero] >> 1603 `pmonic z` by rw[] >> 1604 qabbrev_tac `h = forderz p` >> 1605 `(PolyModRing r z).sum.id = |0|` by metis_tac[poly_mod_ring_ids] >> 1606 `((PolyModRing r z).prod excluding |0|).id = |1|` by rw[poly_mod_prod_nonzero_id] >> 1607 `Group ((PolyModRing r z).prod excluding |0|)` by metis_tac[poly_mod_prod_group] >> 1608 (`p IN ((PolyModRing r z).prod excluding |0|).carrier` by (rw[poly_mod_ring_property, excluding_def] >> metis_tac[poly_zero])) >> 1609 `((PolyModRing r z).prod excluding |0|).exp p k = (p ** k) % z` by rw[poly_mod_exp_alt] >> 1610 `_ = |1| % z` by rw[GSYM pmod_def_alt] >> 1611 `_ = |1|` by rw[] >> 1612 metis_tac[group_order_condition, prime_def, group_order_eq_1]); 1613(* Not in use now *) 1614 1615(* Theorem: poly p /\ p % z <> |0| /\ p % z <> |1| ==> 1616 !k. prime k /\ (p ** k == |1|) (pm z) ==> (forderz p = k) *) 1617(* Proof: 1618 Let h = forderz p = forderz (p % z) by poly_order_eq_poly_mod_order 1619 First, (PolyModRing r z).sum.id = |0| by poly_mod_ring_ids 1620 and ((PolyModRing r z).prod excluding |0|).id = |1| by poly_mod_prod_nonzero_id 1621 Now, Group ((PolyModRing r z).prod excluding |0|) by poly_mod_prod_group 1622 Since deg (p % z) < deg z by poly_deg_mod_less 1623 and p % z <> |0| by given 1624 p % z IN ((PolyModRing r z).prod excluding |0|).carrier by poly_mod_ring_property, excluding_def 1625 Given (p ** k == |1|) (pm z) 1626 means (p ** k) % z = |1| % z by pmod_def_alt 1627 = |1| by poly_deg_one, poly_mod_less 1628 Hence ((PolyModRing r z).prod excluding |0|).exp (p % z) k 1629 = (p % z) ** k % z by poly_mod_exp_alt 1630 = (p ** k) % z by poly_mod_exp 1631 = |1| by above 1632 1633 Therefore h divides k by group_order_condition 1634 which means h = 1, or h = k by prime_def 1635 But h = 1 ==> p % z = |1| by group_order_eq_1 1636 which is excluded by p % z <> |1|. 1637*) 1638val poly_order_prime_condition = store_thm( 1639 "poly_order_prime_condition", 1640 ``!r:'a field. Field r ==> !z. monic z /\ ipoly z ==> 1641 !p. poly p /\ p % z <> |0| /\ p % z <> |1| ==> 1642 !k. prime k /\ (p ** k == |1|) (pm z) ==> (forderz p = k)``, 1643 rpt strip_tac >> 1644 `Ring r /\ #1 <> #0` by rw[] >> 1645 `0 < deg z` by rw[poly_irreducible_deg_nonzero] >> 1646 `pmonic z` by rw[] >> 1647 qabbrev_tac `h = forderz p` >> 1648 `forderz (p % z) = h` by rw[poly_order_eq_poly_mod_order, Abbr`h`] >> 1649 `(PolyModRing r z).sum.id = |0|` by metis_tac[poly_mod_ring_ids] >> 1650 `((PolyModRing r z).prod excluding |0|).id = |1|` by rw[poly_mod_prod_nonzero_id] >> 1651 `Group ((PolyModRing r z).prod excluding |0|)` by metis_tac[poly_mod_prod_group] >> 1652 (`p % z IN ((PolyModRing r z).prod excluding |0|).carrier` by (rw[poly_mod_ring_property, excluding_def, poly_deg_mod_less] >> metis_tac[poly_zero])) >> 1653 `(p ** k) % z = |1|` by metis_tac[pmod_def_alt, poly_one_poly, poly_deg_one, poly_mod_less] >> 1654 `((PolyModRing r z).prod excluding |0|).exp (p % z) k = ((p % z) ** k) % z` by rw[poly_mod_exp_alt] >> 1655 `_ = (p ** k) % z` by rw[GSYM poly_mod_exp] >> 1656 `_ = |1|` by rw[] >> 1657 `h divides k` by metis_tac[group_order_condition] >> 1658 `(h = 1) \/ (h = k)` by metis_tac[prime_def] >> 1659 metis_tac[group_order_eq_1]); 1660 1661(* Theorem: monic z /\ ipoly z /\ z <> unity 1 ==> 1662 !k. prime k /\ (X ** k == |1|) (pm z) ==> (forderz X = k) *) 1663(* Proof: 1664 First, 0 < deg z by poly_irreducible_deg_nonzero 1665 Hence pmonic z by notation 1666 Show z <> X 1667 Since prime k, 0 < k by PRIME_POS 1668 and pmonic X by poly_deg_X, poly_monic_X 1669 Given (X ** k == |1|) (pm z), 1670 This is X ** k % z = |1| by pmod_def_alt 1671 But X ** k % X = |0| by poly_mod_exp, poly_div_mod_id 1672 If z = X, this means |0| = |1| 1673 which is not possible for Field by poly_one_eq_poly_zero 1674 With z <> X, and z <> unity 1 by given 1675 We claim: X % z <> |0| 1676 If deg z = 1, z = factor c by poly_monic_deg1_factor 1677 and X % z = c * |1| by poly_factor_divides_X 1678 This equals |0| when c = #0 by poly_cmult_lzero 1679 but this makes z = X by poly_sub_rzero 1680 which contradicts z <> X. 1681 If 1 < deg z, X % z = X by poly_mod_less 1682 and X <> |0| as they differ in degree. 1683 and: X % z <> |1| 1684 If deg z = 1, z = factor c by poly_monic_deg1_factor 1685 and X % z = c * |1| by poly_factor_divides_X 1686 This equals |1| when c = #1 by poly_cmult_lone 1687 but this makes z = unity 1 by poly_unity_1 1688 which contradicts z <> unity 1 1689 If 1 < deg z, X % z = X by poly_mod_less 1690 and X <> |1| as they differ in degree. 1691 Hence X % z <> |0|, and X % z <> |1|. 1692 and the result follows by poly_order_prime_condition. 1693*) 1694val poly_X_order_prime_condition = store_thm( 1695 "poly_X_order_prime_condition", 1696 ``!r:'a field. Field r ==> !z. monic z /\ ipoly z /\ z <> unity 1 ==> 1697 !k. prime k /\ (X ** k == |1|) (pm z) ==> (forderz X = k)``, 1698 rpt strip_tac >> 1699 `Ring r /\ #1 <> #0` by rw[] >> 1700 `0 < deg z` by rw[poly_irreducible_deg_nonzero] >> 1701 `pmonic z` by rw[] >> 1702 `poly X` by rw[] >> 1703 `0 < k` by rw[PRIME_POS] >> 1704 `k <> 0` by decide_tac >> 1705 `pmonic X` by rw[] >> 1706 `X ** k % z = |1|` by metis_tac[pmod_def_alt, poly_one_poly, poly_deg_one, poly_mod_less] >> 1707 `X ** k % X = |0|` by metis_tac[poly_mod_exp, poly_div_mod_id, poly_zero_exp, poly_mod_zero] >> 1708 `z <> X` by metis_tac[poly_one_eq_poly_zero] >> 1709 `X % z <> |0| /\ X % z <> |1|` by 1710 (rw_tac std_ss[] >| [ 1711 Cases_on `deg z = 1` >| [ 1712 `?c. c IN R /\ (z = factor c)` by rw[poly_monic_deg1_factor] >> 1713 `c <> #0` by metis_tac[poly_factor_alt, poly_cmult_lzero, poly_sub_rzero, poly_one_poly] >> 1714 rw[poly_factor_divides_X], 1715 `1 < deg z` by decide_tac >> 1716 rw[poly_mod_less] 1717 ], 1718 Cases_on `deg z = 1` >| [ 1719 `?c. c IN R /\ (z = factor c)` by rw[poly_monic_deg1_factor] >> 1720 `c <> #1` by metis_tac[poly_factor_alt, poly_cmult_lone, poly_one_poly, poly_unity_1] >> 1721 rw[poly_factor_divides_X, poly_one], 1722 `1 < deg z` by decide_tac >> 1723 rw[poly_mod_less, poly_one, poly_unity_1] 1724 ] 1725 ]) >> 1726 rw[poly_order_prime_condition]); 1727 1728(* Theorem: prime k /\ mifactor z (unity k) /\ z <> unity 1 ==> INJ (\p. p % z) PM (Q z) *) 1729(* Proof: 1730 Since ipoly z ==> 0 < deg z by poly_irreducible_deg_nonzero 1731 monic z ==> pmonic z 1732 and 0 < k by PRIME_POS 1733 Let u = unity k, and pmonic u by poly_unity_pmonic 1734 Since (X ** k == |1|) (pm u) by poly_unity_pmod_eqn, 0 < k 1735 (X ** k == |1|) (pm z) by poly_mod_eq_divisor 1736 ==> forderz X = k by poly_X_order_prime_condition, z <> unity 1 1737 The result follows by reduceP_mod_modP_inj_1 1738*) 1739val reduceP_mod_modP_inj_2 = store_thm( 1740 "reduceP_mod_modP_inj_2", 1741 ``!(r:'a field) k s:num z. Field r /\ 1742 prime k /\ mifactor z (unity k) /\ z <> unity 1 ==> INJ (\p. p % z) PM (Q z)``, 1743 rpt strip_tac >> 1744 `Ring r /\ #1 <> #0` by rw[] >> 1745 `0 < deg z` by rw[poly_irreducible_deg_nonzero] >> 1746 `pmonic z` by rw[] >> 1747 qabbrev_tac `u = unity k` >> 1748 `0 < k` by rw[PRIME_POS] >> 1749 `poly X /\ poly |1| /\ poly (X ** k) /\ pmonic u` by rw[poly_unity_pmonic, Abbr`u`] >> 1750 `(X ** k == |1|) (pm u)` by metis_tac[poly_unity_pmod_eqn] >> 1751 `(X ** k == |1|) (pm z)` by metis_tac[poly_mod_eq_divisor] >> 1752 `forderz X = k` by rw[poly_X_order_prime_condition] >> 1753 rw[reduceP_mod_modP_inj_1]); 1754(* for version 2 *) 1755 1756(* Theorem: prime k /\ 0 < s /\ s < char r /\ mifactor z (unity k) /\ z <> unity 1 ==> 1757 2 ** (MIN s (CARD M)) <= CARD (Q z) *) 1758(* Proof: 1759 First, 1 < k by ONE_LT_PRIME, hence 0 < k. 1760 Let n = MIN s (CARD M). 1761 1762 Given the conditions, 1763 INJ (\p. p % z) PM (Q z) by reduceP_mod_modP_inj_2 1764 Now, FINITE (Q z) by modP_finite 1765 Hence FINITE PM by FINITE_INJ 1766 and CARD PM <= CARD (Q z) by INJ_CARD 1767 But PPM n SUBSET PM by reduceP_poly_subset_reduceP, 0 < k, 0 < s, s < char r 1768 and |0| IN PM by reduceP_has_zero 1769 Hence ( |0| INSERT PPM n) SUBSET PM by INSERT_SUBSET 1770 So CARD ( |0| INSERT PPM n) <= CARD PM by CARD_SUBSET 1771 Since |0| NOTIN PPM n by reduceP_poly_has_no_zero 1772 and FINITE (PPM n) by reduceP_poly_finite 1773 CARD ( |0| INSERT PPM n) 1774 = SUC (CARD (PPM n)) by CARD_INSERT, since p NOTIN the set 1775 = SUC (PRE (2 ** n)) by reduceP_poly_card 1776 = 2 ** n by SUC_PRE, with 0 < 2 ** n by ZERO_LT_EXP. 1777 Hence 2 ** n <= CARD (Q z) by LESS_EQ_TRANS 1778*) 1779val modP_card_lower_2 = store_thm( 1780 "modP_card_lower_2", 1781 ``!(r:'a field) k s:num z. FiniteField r /\ prime k /\ 0 < s /\ s < char r /\ 1782 mifactor z (unity k) /\ z <> unity 1 ==> 2 ** (MIN s (CARD M)) <= CARD (Q z)``, 1783 rpt (stripDup[FiniteField_def]) >> 1784 `Ring r /\ #1 <> #0` by rw[] >> 1785 `FiniteRing r` by rw[FiniteRing_def] >> 1786 `pmonic z` by metis_tac[poly_monic_irreducible_factor] >> 1787 `INJ (\p. p % z) PM (Q z)` by rw[reduceP_mod_modP_inj_2] >> 1788 `FINITE (Q z)` by rw[modP_finite] >> 1789 `FINITE PM` by rw[reduceP_finite] >> 1790 `CARD PM <= CARD (Q z)` by metis_tac[INJ_CARD] >> 1791 `1 < k` by rw[ONE_LT_PRIME] >> 1792 `|0| IN PM` by rw[reduceP_has_zero] >> 1793 qabbrev_tac `n = MIN s (CARD M)` >> 1794 `0 < k` by decide_tac >> 1795 `PPM n SUBSET PM` by rw[reduceP_poly_subset_reduceP, Abbr`n`] >> 1796 `( |0| INSERT PPM n) SUBSET PM` by rw[INSERT_SUBSET] >> 1797 `CARD ( |0| INSERT PPM n) <= CARD PM` by rw[CARD_SUBSET] >> 1798 `n <= s` by rw[Abbr`n`] >> 1799 `n < char r` by decide_tac >> 1800 `|0| NOTIN PPM n` by rw[reduceP_poly_has_no_zero] >> 1801 `FINITE (PPM n)` by rw[reduceP_poly_finite] >> 1802 `CARD ( |0| INSERT PPM n) = SUC (CARD (PPM n))` by metis_tac[CARD_INSERT] >> 1803 `_ = SUC (PRE (2 ** n))` by rw[reduceP_poly_card] >> 1804 `_ = 2 ** n` by metis_tac[SUC_PRE, ZERO_LT_EXP, DECIDE``0 < 2``] >> 1805 decide_tac); 1806(* for version 2 *) 1807 1808(* ------------------------------------------------------------------------- *) 1809(* Upper Bound for (Q z) by Roots. *) 1810(* ------------------------------------------------------------------------- *) 1811 1812(* Theorem: coprime k (CARD R) /\ 1 < ordz k (CARD R) /\ 1813 char r divides n /\ n IN N /\ ~perfect_power n (char r) /\ mifactor z (unity k) ==> 1814 CARD (Q z) <= n ** SQRT (CARD M) *) 1815(* Proof: 1816 Let p = char r, q = n DIV p, t = CARD M. 1817 The goal is: CARD (Q z) <= n ** SQRT t 1818 1819 Step 0: useful bits 1820 Note prime p by finite_field_char 1821 so 1 < p and 0 < p by ONE_LT_PRIME 1822 and n = p * q by DIVIDES_EQN_COMM, 0 < p 1823 Note 1 < CARD R by finite_field_card_gt_1 1824 so 1 < k by ZN_order_with_coprime_1 1825 Note n <> p by perfect_power_self, ~perfect_power n p 1826 and coprime n k by setN_element, n IN N 1827 so n <> 0 by GCD_0, k <> 1 1828 or q <> 0 by MULT_EQ_0, 0 < n, 0 < p 1829 and q <> 1 by MULT_RIGHT_1, n <> p 1830 ==> 1 < q by q <> 0, q <> 1 1831 Note p IN N /\ q IN N by setN_has_char_and_cofactor 1832 1833 Let u = NM p q (SQRT t). 1834 Step 1: A collision with m1 IN u, m2 IN u, m1 <> m2, but m1 MOD k = m2 MOD k. 1835 Note ~perfect_power q p by perfect_power_cofactor, 0 < p, ~perfect_power n p 1836 ==> CARD u = (SUC (SQRT t)) ** 2 by reduceN_card, ADD1, 0 < k, prime p, 1 < q, ~perfect_power q p 1837 Now FINITE M by modN_finite, 0 < k 1838 so t < (SUC (SQRT t)) ** 2 by SQRT_PROPERTY 1839 or t < CARD u by above 1840 ==> ~INJ (\m. m MOD k) u M by PHP 1841 By INJ_DEF, such a collision exists if m IN u ==> m MOD k IN M. 1842 But m IN u ==> m IN N by reduceN_element_in_setN 1843 ==> m MOD k IN M by setN_element_mod 1844 1845 Let f = PolyModRing r z, d = lift (X ** m1 - X ** m2). 1846 Step 2: properties of quotient field and special polynomial z. 1847 Note Field f by poly_mod_irreducible_field 1848 and poly (X ** m1 - X ** m2) by poly_sub_poly 1849 and 0 < deg h by poly_irreducible_deg_nonzero, ipoly h 1850 ==> Poly f d by poly_mod_lift_poly, 0 < deg h 1851 Also X ** m1 <> X ** m2 by poly_X_exp_eq, m1 <> m2 1852 thus X ** m1 - X ** m2 <> |0| by poly_sub_eq_zero 1853 ==> d <> poly_zero f by poly_mod_lift_eq_zero 1854 1855 Step 3: CARD (Q z) <= Deg f d 1856 Note m1 IN N /\ m2 IN N by reduceN_element_in_setN, 0 < k, p IN N, q IN N 1857 ==> Q z SUBSET poly_roots f d by setN_mod_eq_gives_modP_roots_2 1858 Also FINITE (poly_roots f d) by poly_roots_finite, Poly f d, d <> poly_zero f 1859 Thus CARD (Q z) 1860 <= CARD (poly_roots f d) by CARD_SUBSET 1861 <= Deg f d by poly_roots_count 1862 1863 Step 4: Deg f d <= n ** SQRT t 1864 Note Deg f d 1865 = deg (X ** m1 - X ** m2) by poly_mod_lift_deg 1866 <= MAX (deg (X ** m1)) (deg (X ** m2)) by poly_deg_sub 1867 = MAX m1 m2 by poly_deg_X_exp 1868 Now m1 <= n ** SQRT t by reduceN_element_upper_better 1869 and m2 <= n ** SQRT t by reduceN_element_upper_better 1870 Thus MAX m1 m2 <= n ** SQRT t by MAX_LE 1871 1872 Therefore, CARD (Q z) <= n ** SQRT t by [3], [4] 1873*) 1874val modP_card_upper_better = store_thm( 1875 "modP_card_upper_better", 1876 ``!r:'a field k n s:num z. FiniteField r /\ coprime k (CARD R) /\ 1 < ordz k (CARD R) /\ 1877 char r divides n /\ n IN N /\ ~perfect_power n (char r) /\ mifactor z (unity k) ==> 1878 CARD (Q z) <= n ** SQRT (CARD M)``, 1879 rpt (stripDup[FiniteField_def]) >> 1880 `Ring r /\ #1 <> #0` by rw[] >> 1881 qabbrev_tac `p = char r` >> 1882 qabbrev_tac `q = n DIV p` >> 1883 qabbrev_tac `t = CARD M` >> 1884 `prime p` by rw[finite_field_char, Abbr`p`] >> 1885 `1 < p` by rw[ONE_LT_PRIME] >> 1886 `0 < p` by decide_tac >> 1887 `n = p * q` by metis_tac[DIVIDES_EQN_COMM] >> 1888 `1 < k` by metis_tac[ZN_order_with_coprime_1, finite_field_card_gt_1] >> 1889 `0 < k` by decide_tac >> 1890 `1 < q` by 1891 (`n <> p` by metis_tac[perfect_power_self] >> 1892 `n <> 0` by metis_tac[GCD_0, setN_element, DECIDE``1 < k ==> k <> 1``] >> 1893 `q <> 0` by metis_tac[MULT_EQ_0, NOT_ZERO_LT_ZERO] >> 1894 `q <> 1` by metis_tac[MULT_RIGHT_1] >> 1895 decide_tac) >> 1896 `p IN N /\ q IN N` by metis_tac[setN_has_char_and_cofactor] >> 1897 qabbrev_tac `u = NM p q (SQRT t)` >> 1898 `?m1 m2. m1 IN u /\ m2 IN u /\ m1 <> m2 /\ (m1 MOD k = m2 MOD k)` by 1899 (`~perfect_power q p` by metis_tac[perfect_power_cofactor] >> 1900 `CARD u = (SUC (SQRT t)) ** 2` by metis_tac[reduceN_card, ADD1] >> 1901 `FINITE M` by rw[modN_finite] >> 1902 `t < (SUC (SQRT t)) ** 2` by rw[SQRT_PROPERTY] >> 1903 `t < CARD u` by decide_tac >> 1904 `~INJ (\m. m MOD k) u M` by metis_tac[PHP] >> 1905 fs[INJ_DEF] >- 1906 metis_tac[reduceN_element_in_setN, setN_element_mod] >> 1907 metis_tac[] 1908 ) >> 1909 qabbrev_tac `f = PolyModRing r z` >> 1910 qabbrev_tac `d = lift (X ** m1 - X ** m2)` >> 1911 `Field f` by rw[poly_mod_irreducible_field, Abbr`f`] >> 1912 `Poly f d` by 1913 (`poly (X ** m1 - X ** m2)` by rw[] >> 1914 `0 < deg z` by rw[poly_irreducible_deg_nonzero] >> 1915 rw[poly_mod_lift_poly, Abbr`f`, Abbr`d`]) >> 1916 `d <> poly_zero f` by 1917 (`X ** m1 <> X ** m2` by rw[poly_X_exp_eq] >> 1918 `X ** m1 - X ** m2 <> |0|` by rw[poly_sub_eq_zero] >> 1919 rw[poly_mod_lift_eq_zero, Abbr`f`, Abbr`d`]) >> 1920 `CARD (Q z) <= Deg f d` by 1921 (`m1 IN N /\ m2 IN N` by metis_tac[reduceN_element_in_setN] >> 1922 `Q z SUBSET poly_roots f d` by rw[setN_mod_eq_gives_modP_roots_2, Abbr`f`, Abbr`d`] >> 1923 `FINITE (poly_roots f d)` by rw[poly_roots_finite] >> 1924 `CARD (Q z) <= CARD (poly_roots f d)` by rw[CARD_SUBSET] >> 1925 `CARD (poly_roots f d) <= Deg f d` by rw[poly_roots_count] >> 1926 decide_tac) >> 1927 `Deg f d <= n ** SQRT t` by 1928 (`Deg f d = deg (X ** m1 - X ** m2)` by metis_tac[poly_mod_lift_deg] >> 1929 `deg (X ** m1 - X ** m2) <= MAX (deg (X ** m1)) (deg (X ** m2))` by rw[poly_deg_sub] >> 1930 `MAX (deg (X ** m1)) (deg (X ** m2)) = MAX m1 m2` by rw[] >> 1931 `m1 <= n ** SQRT t /\ m2 <= n ** SQRT t` by rw[reduceN_element_upper_better] >> 1932 `MAX m1 m2 <= n ** SQRT t` by rw[] >> 1933 decide_tac) >> 1934 decide_tac); 1935 1936(* This is the usual story in conventional proofs of the AKS theorem! *) 1937 1938(* 1939This upper bound is also independent of the range s of polynomial checks. 1940Although M = N MOD k, and N is the introspective exponents valid for all the range s, 1941N consists only of 4 seeds: 1, p = char r, q = n DIV p, n, all valid for any range s. 1942And (CARD M <= phi k) by modN_card_upper_better. 1943*) 1944 1945(* Theorem: coprime k (CARD R) /\ 1 < ordz k (CARD R) /\ 1946 char r divides n /\ n IN N /\ ~perfect_power n (char r) /\ mifactor z (unity k) ==> 1947 CARD (Q z) <= 2 ** (SQRT (CARD M) * ulog n) *) 1948(* Proof: 1949 Note 1 < CARD R by finite_field_card_gt_1 1950 so 1 < k by ZN_order_with_coprime_1 1951 Note coprime n k by setN_element 1952 Thus n <> 0 by GCD_0, k <> 1 1953 1954 Let t = CARD M. 1955 CARD (Q z) 1956 <= n ** SQRT t by modP_card_upper_better 1957 <= (2 ** ulog n) ** SQRT t by ulog_property, 0 < n 1958 = 2 ** (ulog n * SQRT t) by EXP_EXP_MULT 1959 = 2 ** (SQRT t * ulog n) by arithmetic 1960*) 1961val modP_card_upper_better_1 = store_thm( 1962 "modP_card_upper_better_1", 1963 ``!r:'a field k n s:num z. FiniteField r /\ coprime k (CARD R) /\ 1 < ordz k (CARD R) /\ 1964 char r divides n /\ n IN N /\ ~perfect_power n (char r) /\ mifactor z (unity k) ==> 1965 CARD (Q z) <= 2 ** (SQRT (CARD M) * ulog n)``, 1966 rpt strip_tac >> 1967 `1 < k` by metis_tac[ZN_order_with_coprime_1, finite_field_card_gt_1] >> 1968 `n <> 0` by metis_tac[GCD_0, setN_element, LESS_NOT_EQ] >> 1969 qabbrev_tac `t = CARD M` >> 1970 `CARD (Q z) <= n ** SQRT t` by rw[modP_card_upper_better, Abbr`t`] >> 1971 `n ** SQRT t <= (2 ** ulog n) ** SQRT t` by rw[ulog_property] >> 1972 `(2 ** ulog n) ** SQRT t = 2 ** (ulog n * SQRT t)` by rw[EXP_EXP_MULT] >> 1973 `_ = 2 ** (SQRT t * ulog n)` by rw[] >> 1974 decide_tac); 1975 1976(* Theorem: coprime k (CARD R) /\ 1 < ordz k (CARD R) /\ 1977 char r divides n /\ n IN N /\ ~perfect_power n (char r) /\ mifactor z (unity k) ==> 1978 CARD (Q z) <= 2 ** (SQRT (phi k) * ulog n) *) 1979(* Proof: 1980 Note 1 < CARD R by finite_field_card_gt_1 1981 so 1 < k by ZN_order_with_coprime_1 1982 1983 Let t = CARD M. 1984 CARD (Q z) 1985 <= 2 ** (SQRT t * ulog n) by modP_card_upper_better_1, 1 < k 1986 <= 2 ** (SQRT (phi k) * ulog n) by modN_card_upper_better, EXP_BASE_LE_MONO 1987*) 1988val modP_card_upper_better_2 = store_thm( 1989 "modP_card_upper_better_2", 1990 ``!r:'a field k n s:num z. FiniteField r /\ coprime k (CARD R) /\ 1 < ordz k (CARD R) /\ 1991 char r divides n /\ n IN N /\ ~perfect_power n (char r) /\ mifactor z (unity k) ==> 1992 CARD (Q z) <= 2 ** (SQRT (phi k) * ulog n)``, 1993 rpt strip_tac >> 1994 `1 < k` by metis_tac[ZN_order_with_coprime_1, finite_field_card_gt_1] >> 1995 qabbrev_tac `t = CARD M` >> 1996 `CARD (Q z) <= 2 ** (SQRT t * ulog n)` by rw[modP_card_upper_better_1, Abbr`t`] >> 1997 `SQRT t <= SQRT (phi k)` by rw[modN_card_upper_better, SQRT_LE, Abbr`t`] >> 1998 `2 ** (SQRT t * ulog n) <= 2 ** (SQRT (phi k) * ulog n)` by rw[] >> 1999 decide_tac); 2000 2001(* 2002This clearly shows that the upper bound is independent of the range s of polynomial checks. 2003*) 2004 2005(* ------------------------------------------------------------------------- *) 2006(* Better Lower Bound for (Q z). *) 2007(* ------------------------------------------------------------------------- *) 2008 2009(* Theorem: mifactor z (unity k) /\ 1 < deg z /\ 2010 (forderz X = k) /\ 1 < CARD M /\ 0 < s /\ s < char r ==> 2 ** (MIN s (CARD M)) < CARD (Q z) *) 2011(* Proof: 2012 First, 1 < k by poly_X_order_gt_1. 2013 Let n = MIN s (CARD M). 2014 2015 Given the conditions, 2016 INJ (\p. p % z) PM (Q z) by reduceP_mod_modP_inj_0 2017 Now, FINITE (Q z) by modP_finite 2018 Hence FINITE PM by FINITE_INJ 2019 and CARD PM <= CARD (Q z) by INJ_CARD 2020 But PPM n SUBSET PM by reduceP_poly_subset_reduceP, 0 < k, 0 < s, s < char 2021 and |0| IN PM by reduceP_has_zero 2022 and X IN PM by reduceP_has_X 2023 Hence X INSERT |0| INSERT PPM n SUBSET PM by INSERT_SUBSET 2024 So CARD (X INSERT |0| INSERT PPM n) <= CARD PM by CARD_SUBSET 2025 2026 Since |0| NOTIN PPM n by reduceP_poly_has_no_zero 2027 and X NOTIN PPM n by reduceP_poly_has_no_X 2028 and FINITE (PPM n) by reduceP_poly_finite 2029 CARD (X INSERT |0| INSERT PPM n) 2030 = SUC (SUC (CARD (PPM n))) by CARD_INSERT, since X, 0 NOTIN the set 2031 = SUC (SUC (PRE (2 ** n))) by reduceP_poly_card 2032 = SUC (2 ** n) by SUC_PRE, with 0 < 2 ** n by ZERO_LT_EXP. 2033 Hence SUC (2 ** n) <= CARD (Q z) by LESS_EQ_TRANS 2034 or 2 ** n < CARD (Q z) by LESS_SUC, x < SUC x 2035*) 2036val modP_card_lower_better = store_thm( 2037 "modP_card_lower_better", 2038 ``!(r:'a field) k s:num z. FiniteField r /\ mifactor z (unity k) /\ 1 < deg z /\ 2039 (forderz X = k) /\ 1 < CARD M /\ 0 < s /\ s < char r ==> 2 ** (MIN s (CARD M)) < CARD (Q z)``, 2040 rpt (stripDup[FiniteField_def]) >> 2041 `Ring r /\ #1 <> #0` by rw[] >> 2042 `FiniteRing r` by rw[FiniteRing_def] >> 2043 `pmonic z` by metis_tac[poly_monic_irreducible_factor] >> 2044 `INJ (\p. p % z) PM (Q z)` by rw[reduceP_mod_modP_inj_0] >> 2045 `FINITE (Q z)` by rw[modP_finite] >> 2046 `FINITE PM` by metis_tac[FINITE_INJ] >> 2047 `CARD PM <= CARD (Q z)` by metis_tac[INJ_CARD] >> 2048 `1 < k` by rw[poly_X_order_gt_1] >> 2049 `|0| IN PM` by rw[reduceP_has_zero] >> 2050 `0 < k` by decide_tac >> 2051 `X IN PM` by rw[reduceP_has_X] >> 2052 qabbrev_tac `n = MIN s (CARD M)` >> 2053 `PPM n SUBSET PM` by rw[reduceP_poly_subset_reduceP, Abbr`n`] >> 2054 `(X INSERT |0| INSERT PPM n) SUBSET PM` by rw[INSERT_SUBSET] >> 2055 `CARD (X INSERT |0| INSERT PPM n) <= CARD PM` by rw[CARD_SUBSET] >> 2056 `n <= s` by rw[Abbr`n`] >> 2057 `n < char r` by decide_tac >> 2058 `|0| NOTIN PPM n` by rw[reduceP_poly_has_no_zero] >> 2059 `X NOTIN PPM n` by rw[reduceP_poly_has_no_X] >> 2060 `FINITE (PPM n)` by rw[reduceP_poly_finite] >> 2061 `CARD ( |0| INSERT PPM n) = SUC (CARD (PPM n))` by rw[CARD_INSERT] >> 2062 `CARD (X INSERT |0| INSERT PPM n) = SUC (SUC (CARD (PPM n)))` by rw[CARD_INSERT] >> 2063 `_ = SUC (SUC (PRE (2 ** n)))` by rw[reduceP_poly_card] >> 2064 `_ = SUC (2 ** n)` by metis_tac[SUC_PRE, ZERO_LT_EXP, DECIDE``0 < 2``] >> 2065 decide_tac); 2066 2067(* Theorem: FiniteField r /\ coprime k (CARD R) /\ 1 < ordz k (CARD R) /\ 2068 char r divides n /\ n IN N /\ ~perfect_power n (char r) /\ 0 < s /\ s < char r /\ 2069 mifactor z (unity k) /\ 1 < deg z /\ (forderz X = k) /\ 2070 1 < CARD M ==> 2 ** MIN s (CARD M) < CARD (Q z) /\ CARD (Q z) <= n ** SQRT (CARD M) *) 2071(* Proof: 2072 Note 1 < CARD R by finite_field_card_gt_1 2073 so 1 < k by ZN_order_with_coprime_1 2074 The lower bound follows by modP_card_lower_better, 1 < CARD M 2075 The upper bound follows by modP_card_upper_better 2076*) 2077val modP_card_range = store_thm( 2078 "modP_card_range", 2079 ``!r:'a field k n s:num z. FiniteField r /\ coprime k (CARD R) /\ 1 < ordz k (CARD R) /\ 2080 char r divides n /\ n IN N /\ ~perfect_power n (char r) /\ 0 < s /\ s < char r /\ 2081 mifactor z (unity k) /\ 1 < deg z /\ (forderz X = k) /\ 2082 1 < CARD M ==> 2 ** MIN s (CARD M) < CARD (Q z) /\ CARD (Q z) <= n ** SQRT (CARD M)``, 2083 ntac 6 strip_tac >> 2084 `1 < k` by metis_tac[ZN_order_with_coprime_1, finite_field_card_gt_1] >> 2085 rw[modP_card_lower_better, modP_card_upper_better]); 2086 2087(* ------------------------------------------------------------------------- *) 2088(* Exponent bounds for (CARD M) *) 2089(* ------------------------------------------------------------------------- *) 2090 2091(* Theorem: Ring r ==> 2092 !k n s. 1 < k /\ n IN N /\ 1 < k /\ n IN N /\ (ulog n) ** 2 <= ordz k n ==> 2093 SQRT (CARD M) * ulog n <= MIN (SQRT (phi k) * ulog n) (CARD M) *) 2094(* Proof: 2095 Let t = CARD M 2096 h = ordz k n 2097 m = ulog n 2098 c = SQRT (phi k) * m 2099 and the goal: SQRT t * m <= MIN c 2100 2101 Step 1: SQRT t * m <= c 2102 Note t <= phi k by modN_card_upper_better 2103 so SQRT t <= SQRT (phi k) by SQRT_LE 2104 ===> c = SQRT (phi k) * m by notation 2105 >= SQRT t * m by arithmetic 2106 2107 Step 2: SQRT t * m <= t 2108 Note h <= t by modN_card_lower, 1 < k, Ring r 2109 and m <= SQRT h by SQRT_LE, SQRT_OF_SQ, m ** 2 <= h 2110 ==> t >= (SQRT t) * (SQRT t) by SQ_SQRT_LE 2111 >= (SQRT t) * (SQRT h) by SQRT_LE, h <= t 2112 >= SQRT t * m by above 2113 2114 Hence SQRT t * m <= MIN c t by MIN_DEF 2115*) 2116val modN_card_with_ulog_le_min_1 = store_thm( 2117 "modN_card_with_ulog_le_min_1", 2118 ``!r:'a ring. Ring r ==> 2119 !k n s:num. 1 < k /\ n IN N /\ (ulog n) ** 2 <= ordz k n ==> 2120 SQRT (CARD M) * ulog n <= MIN (SQRT (phi k) * ulog n) (CARD M)``, 2121 rpt strip_tac >> 2122 qabbrev_tac `t = CARD M` >> 2123 qabbrev_tac `h = ordz k n` >> 2124 qabbrev_tac `m = ulog n` >> 2125 qabbrev_tac `c = SQRT (phi k) * m` >> 2126 `SQRT t * m <= c` by 2127 (`t <= phi k` by rw[modN_card_upper_better, Abbr`t`] >> 2128 `SQRT t <= SQRT (phi k)` by rw[SQRT_LE] >> 2129 rw_tac arith_ss[Abbr`c`]) >> 2130 `SQRT t * m <= t` by 2131 (`h <= t` by rw[modN_card_lower, Abbr`h`, Abbr`t`] >> 2132 `SQRT h <= SQRT t` by rw[SQRT_LE] >> 2133 `(SQRT h) * (SQRT t) <= (SQRT t) * (SQRT t)` by rw_tac arith_ss[] >> 2134 `m <= SQRT h` by metis_tac[SQRT_LE, SQRT_OF_SQ] >> 2135 `m * SQRT t <= SQRT h * SQRT t` by rw_tac arith_ss[] >> 2136 `(SQRT t) * (SQRT t) <= t` by rw[SQ_SQRT_LE] >> 2137 decide_tac) >> 2138 metis_tac[MIN_DEF]); 2139 2140(* Theorem: Ring r ==> 2141 !k n s. 1 < k /\ n IN N /\ (2 * ulog n) ** 2 <= ordz k n ==> 2142 2 * SQRT (CARD M) * ulog n <= MIN (2 * SQRT (phi k) * ulog n) (CARD M) *) 2143(* Proof: 2144 Let t = CARD M 2145 h = ordz k n 2146 m = ulog n 2147 c = 2 * SQRT (phi k) * m 2148 and the goal: 2 * SQRT t * m <= MIN c 2149 2150 Step 1: 2 * SQRT t * m <= c 2151 Note t <= phi k by modN_card_upper_better 2152 so SQRT t <= SQRT (phi k) by SQRT_LE 2153 ===> c = 2 * SQRT (phi k) * m by notation 2154 >= 2 * SQRT t * m by arithmetic 2155 2156 Step 2: 2 * SQRT t * m <= t 2157 Note h <= t by modN_card_lower, 1 < k, Ring r 2158 and 2 * m <= SQRT h by SQRT_LE, SQRT_OF_SQ, (2 * m) ** 2 <= h 2159 ==> t >= (SQRT t) * (SQRT t) by SQ_SQRT_LE 2160 >= (SQRT h) * (SQRT t) by SQRT_LE, h <= t 2161 >= 2 * m * SQRT t by above 2162 = 2 * SQRT t * m 2163 2164 Hence 2 * SQRT t * m <= MIN c t by MIN_DEF 2165*) 2166val modN_card_with_ulog_le_min_2 = store_thm( 2167 "modN_card_with_ulog_le_min_2", 2168 ``!r:'a ring. Ring r ==> 2169 !k n s:num. 1 < k /\ n IN N /\ (2 * ulog n) ** 2 <= ordz k n ==> 2170 2 * SQRT (CARD M) * ulog n <= MIN (2 * SQRT (phi k) * ulog n) (CARD M)``, 2171 rpt strip_tac >> 2172 qabbrev_tac `t = CARD M` >> 2173 qabbrev_tac `h = ordz k n` >> 2174 qabbrev_tac `m = ulog n` >> 2175 qabbrev_tac `c = 2 * SQRT (phi k) * m` >> 2176 `2 * SQRT t * m <= c` by 2177 (`t <= phi k` by rw[modN_card_upper_better, Abbr`t`] >> 2178 `SQRT t <= SQRT (phi k)` by rw[SQRT_LE] >> 2179 rw_tac arith_ss[Abbr`c`]) >> 2180 `2 * SQRT t * m <= t` by 2181 (`h <= t` by rw[modN_card_lower, Abbr`h`, Abbr`t`] >> 2182 `SQRT h <= SQRT t` by rw[SQRT_LE] >> 2183 `(SQRT h) * (SQRT t) <= (SQRT t) * (SQRT t)` by rw_tac arith_ss[] >> 2184 `2 * m <= SQRT h` by metis_tac[SQRT_LE, SQRT_OF_SQ] >> 2185 `2 * m * SQRT t <= SQRT h * SQRT t` by rw_tac arith_ss[] >> 2186 `(SQRT t) * (SQRT t) <= t` by rw[SQ_SQRT_LE] >> 2187 decide_tac) >> 2188 metis_tac[MIN_DEF]); 2189 2190(* 2191> reduceN_mod_modN_inj_1; 2192val it = |- !r k s z. Field r /\ mifactor z (unity k) ==> 2193 !p q. 1 < p /\ 1 < q /\ p IN N /\ q IN N /\ 2194 MAX p q ** TWICE (SQRT (CARD M)) < CARD (Q z) ==> 2195 INJ (\m. m MOD k) (NM p q (SQRT (CARD M))) M: thm 2196 2197> reduceP_mod_modP_inj_1; 2198val it = |- !r k s z. Field r /\ 0 < k /\ mifactor z (unity k) /\ (forderz X = k) ==> 2199 INJ (\p. p % z) PM (Q z): thm 2200 2201Since: 2202> modN_card_upper; 2203val it = |- !r k s. 1 < k ==> CARD M < k: thm 2204> modN_card_lower; 2205val it = |- !r k s. Ring r /\ #1 <> #0 /\ 1 < k ==> 2206 !n. n IN N ==> order (ZN k).prod n <= CARD M: thm 2207> modP_card_upper_max; 2208val it = |- !r k s z. FiniteField r /\ mifactor z (unity k) ==> 2209 CARD (Q z) <= CARD R ** deg z: thm 2210> modP_card_lower_1; 2211val it = |- !r k s z. FiniteField r /\ mifactor z (unity k) /\ (forderz X = k) /\ 2212 1 < k /\ s < char r ==> 2 ** MIN s (CARD M) <= CARD (Q z): thm 2213 2214The condition in reduceN_mod_modN_inj_1 can be satisfied if: 2215 MAX p q ** (2 * SQRT (CARD M)) < 2 ** MIN s (CARD M) 2216 2217Later, will pick p = p IN N, and q = n IN N. Better: q = n DIV p IN N. 2218*) 2219 2220(* ------------------------------------------------------------------------- *) 2221(* Less-than Bounds *) 2222(* ------------------------------------------------------------------------- *) 2223 2224(* Theorem: 1 < k /\ 1 < n /\ n IN N /\ (2 * SUC (LOG2 n)) ** 2 <= ordz k n ==> 2225 n ** (2 * SQRT (CARD M)) < 2 ** MIN (2 * (SQRT (phi k)) * SUC (LOG2 n)) (CARD M) *) 2226(* Proof: 2227 Let t = CARD M 2228 h = ordz k n 2229 m = SUC (LOG2 n) 2230 c = 2 * (SQRT (phi k)) * m 2231 and the goal: n ** (2 * SQRT t) < 2 ** MIN c t 2232 Thus c = 2 * SQRT k * m by given 2233 and (2 * m) ** 2 <= h by given 2234 <= t <= phi k by modN_card_lower, modN_card_upper_better, 1 < k 2235 also n < 2 ** m by LOG, this is critical. 2236 2237 Taking square roots, 2238 SQRT h <= SQRT t <= SQRT (phi k) by SQRT_LE 2239 SQRT ((2 * m) ** 2) <= SQRT h by SQRT_LE 2240 or 2 * m <= SQRT h by SQRT_OF_SQ 2241 2242 First, show m * (2 * SQRT t) <= MIN c t 2243 Since c = 2 * SQRT (phi k) * m 2244 >= 2 * SQRT t * m by SQRT t <= SQRT (phi k) 2245 = m * (2 * SQRT t) by arithmetic 2246 Also t >= (SQRT t) * (SQRT t) by SQ_SQRT_LE 2247 >= (SQRT h) * (SQRT t) by SQRT h <= SQRT t 2248 >= 2 * m * (SQRT t) by 2 * m <= SQRT h 2249 = m * (2 * SQRT t) by arithmetic 2250 Hence m * (2 * SQRT t) <= MIN c t by MIN_DEF 2251 2252 From m * (2 * SQRT t) <= MIN c t 2253 2 ** (m * (2 * SQRT t)) <= 2 ** MIN c t by EXP_BASE_LE_MONO 2254 or (2 ** m) ** (2 * SQRT t) <= 2 ** MIN c t by EXP_EXP_MULT 2255 Now n < 2 ** m by LOG (from above) 2256 n ** (2 * SQRT t) < (2 ** m) ** (2 * SQRT t) by EXP_EXP_LT_MONO 2257 Overall, n ** (2 * SQRT t) < 2 ** MIN c t 2258*) 2259val modN_card_in_exp_lt_bound_0 = store_thm( 2260 "modN_card_in_exp_lt_bound_0", 2261 ``!r:'a ring. Ring r ==> 2262 !k n s:num. 1 < k /\ 1 < n /\ n IN N /\ (2 * SUC (LOG2 n)) ** 2 <= ordz k n ==> 2263 n ** (2 * SQRT (CARD M)) < 2 ** MIN (2 * (SQRT (phi k)) * SUC (LOG2 n)) (CARD M)``, 2264 rpt strip_tac >> 2265 qabbrev_tac `t = CARD M` >> 2266 qabbrev_tac `h = ordz k n` >> 2267 qabbrev_tac `m = SUC (LOG2 n)` >> 2268 qabbrev_tac `c = 2 * (SQRT (phi k)) * m` >> 2269 `h <= t` by rw[modN_card_lower, Abbr`h`, Abbr`t`] >> 2270 `t <= phi k` by rw[modN_card_upper_better, Abbr`t`] >> 2271 `0 < m` by rw[LESS_SUC, Abbr`m`] >> 2272 `m <> 0 /\ 0 < k /\ 0 < n` by decide_tac >> 2273 `2 * m <> 0 /\ (2 * m) ** 2 <> 0` by metis_tac[EXP_EQ_0, MULT_EQ_0, DECIDE``0 < 2 /\ 0 <> 2``] >> 2274 `0 < 2 * m /\ 0 < t` by decide_tac >> 2275 `2 * m <= SQRT h` by metis_tac[SQRT_LE, SQRT_OF_SQ] >> 2276 `SQRT t <= SQRT (phi k)` by rw[SQRT_LE] >> 2277 `SQRT h <= SQRT t` by rw[SQRT_LE] >> 2278 `m * (2 * SQRT t) <= c` by rw_tac arith_ss[Abbr`c`] >> 2279 `(SQRT t) * (SQRT t) <= t` by rw[SQ_SQRT_LE] >> 2280 `(SQRT h) * (SQRT t) <= (SQRT t) * (SQRT t)` by rw_tac arith_ss[] >> 2281 `m * 2 * (SQRT t) <= SQRT h * SQRT t` by rw_tac arith_ss[] >> 2282 `m * (2 * SQRT t) <= t` by decide_tac >> 2283 `m * (2 * SQRT t) <= MIN c t` by metis_tac[MIN_DEF] >> 2284 `2 ** (m * (2 * SQRT t)) <= 2 ** MIN c t` by rw[EXP_BASE_LE_MONO] >> 2285 `2 ** (m * (2 * SQRT t)) = (2 ** m) ** (2 * SQRT t)` by rw[EXP_EXP_MULT] >> 2286 `n < 2 ** m` by rw[LOG2_PROPERTY, Abbr`m`] >> 2287 `0 < 2 * SQRT t` by metis_tac[SQRT_EQ_0, MULT_EQ_0, NOT_ZERO_LT_ZERO] >> 2288 `n ** (2 * SQRT t) < (2 ** m) ** (2 * SQRT t)` by rw[EXP_EXP_LT_MONO] >> 2289 decide_tac); 2290 2291(* Theorem: 1 < k /\ 1 < n /\ n IN N /\ (SUC (LOG2 n)) ** 2 <= ordz k n ==> 2292 n ** (SQRT (CARD M)) < 2 ** MIN (SQRT (phi k) * SUC (LOG2 n)) (CARD M) *) 2293(* Proof: 2294 Let t = CARD M, h = ordz k n, m = SUC (LOG2 n), c = SQRT (phi k) * m. 2295 and the goal is: n ** SQRT t < 2 ** MIN s t 2296 2297 The strategy is to prove in two steps: 2298 (1) show n ** SQRT t < 2 ** (m * SQRT t) 2299 (2) show 2 ** (m * SQRT t) <= 2 ** MIN c t 2300 2301 Step 0: some useful bits, show h <= t and 0 < t 2302 Since m = LOG2 n + 1, 0 < m /\ m <> 0 by arithmetic 2303 so m ** 2 <> 0 by EXP_2, MULT_EQ_0, m <> 0 2304 Note h <= t by modN_card_lower, 1 < k, n IN N 2305 so 0 < n /\ 0 < t by 1 < n, 0 <> m ** 2 <= h (given), h <= t 2306 2307 Step 1: show n ** SQRT t < 2 ** (m * SQRT t) [1] 2308 Note 0 < SQRT t by SQRT_EQ_0, MULT_EQ_0, 0 < t 2309 and n < 2 ** m by LOG2_PROPERTY, ADD1, 0 < n 2310 ==> n ** SQRT t < (2 ** m) ** SQRT t by EXP_EXP_LT_MONO, 0 < SQRT t 2311 and 2 ** (m * SQRT t) = (2 ** m) ** SQRT t by EXP_EXP_MULT 2312 Thus n ** SQRT t < 2 ** (m * SQRT t) by arithmetic 2313 2314 Step 2: show 2 ** (m * SQRT t) <= 2 ** MIN s t [2] 2315 Since base 2 is the same, we can just show: 2316 m * SQRT t <= MIN c t by EXP_BASE_LE_MONO 2317 Easy part: show m * SQRT t <= c 2318 Note t <= phi k by modN_card_upper_better, 1 < k 2319 ==> SQRT t <= SQRT (phi k) by SQRT_LE, t <= phi k 2320 or m * SQRT t <= c by c = SQRT (phi k) * m 2321 Hard part: show m * SQRT t <= t 2322 Since m ** 2 <= h 2323 ==> m <= SQRT h by SQRT_LE, SQRT_OF_SQ 2324 or m * SQRT t <= SQRT h * SQRT t by arithmetic 2325 But SQRT h <= SQRT t by SQRT_LE, h <= t 2326 so SQRT h * SQRT t <= SQRT t * SQRT t by SQRT h <= SQRT t 2327 and SQRT t * SQRT t <= t by SQ_SQRT_LE 2328 Overall, m * SQRT t <= t by combining above 2329 2330 With m * SQRT t <= c /\ m * SQRT t <= t 2331 ==> m * SQRT t <= MIN c t by MIN_DEF 2332 2333 Combining [1] and [2], the result follows. 2334*) 2335val modN_card_in_exp_lt_bound_1 = store_thm( 2336 "modN_card_in_exp_lt_bound_1", 2337 ``!r:'a ring. Ring r ==> 2338 !k n s:num. 1 < k /\ 1 < n /\ n IN N /\ (SUC (LOG2 n)) ** 2 <= ordz k n ==> 2339 n ** (SQRT (CARD M)) < 2 ** MIN (SQRT (phi k) * SUC (LOG2 n)) (CARD M)``, 2340 rpt strip_tac >> 2341 qabbrev_tac `t = CARD M` >> 2342 qabbrev_tac `m = SUC (LOG2 n)` >> 2343 qabbrev_tac `h = ordz k n` >> 2344 qabbrev_tac `c = SQRT (phi k) * m` >> 2345 `h <= t` by rw[modN_card_lower, Abbr`h`, Abbr`t`] >> 2346 `0 < m /\ m <> 0` by rw[LESS_SUC, Abbr`m`] >> 2347 `m ** 2 <> 0` by metis_tac[EXP_2, MULT_EQ_0] >> 2348 `0 < n /\ 0 < t` by decide_tac >> 2349 `n ** SQRT t < 2 ** (m * SQRT t)` by 2350 (`0 < SQRT t` by metis_tac[SQRT_EQ_0, MULT_EQ_0, NOT_ZERO_LT_ZERO] >> 2351 `n < 2 ** m` by metis_tac[LOG2_PROPERTY, ADD1] >> 2352 `n ** SQRT t < (2 ** m) ** SQRT t` by rw[EXP_EXP_LT_MONO] >> 2353 `2 ** (m * SQRT t) = (2 ** m) ** SQRT t` by rw[EXP_EXP_MULT] >> 2354 decide_tac) >> 2355 `2 ** (m * SQRT t) <= 2 ** MIN c t` by 2356 (`m * SQRT t <= MIN c t` suffices_by rw[EXP_BASE_LE_MONO] >> 2357 `t <= phi k` by rw[modN_card_upper_better, Abbr`t`] >> 2358 `SQRT t <= SQRT (phi k)` by rw[SQRT_LE] >> 2359 `m * SQRT t <= c` by rw_tac arith_ss[Abbr`c`] >> 2360 `m <= SQRT h` by metis_tac[SQRT_LE, SQRT_OF_SQ] >> 2361 `m * SQRT t <= SQRT h * SQRT t` by rw_tac arith_ss[] >> 2362 `SQRT h <= SQRT t` by rw[SQRT_LE] >> 2363 `SQRT h * SQRT t <= SQRT t * SQRT t` by rw_tac arith_ss[] >> 2364 `SQRT t * SQRT t <= t` by rw[SQ_SQRT_LE] >> 2365 `m * SQRT t <= t` by decide_tac >> 2366 metis_tac[MIN_DEF]) >> 2367 decide_tac); 2368 2369(* Theorem: 1 < k /\ n IN N ==> 2370 !h. 0 < h /\ n < 2 ** h /\ h ** 2 <= ordz k n ==> 2371 n ** SQRT (CARD M) < 2 ** MIN (SQRT (phi k) * h) (CARD M) *) 2372(* Proof: 2373 Let t = CARD M, p = SQRT (phi k) * h, q = ordz k n 2374 Then the goal is: n ** SQRT t < 2 ** MIN p t 2375 2376 The strategy is to prove in two steps: 2377 (1) show n ** SQRT t < 2 ** (h * SQRT t) 2378 (2) show 2 ** (h * SQRT t) <= 2 ** MIN p t 2379 2380 Step 0: some useful bits, show q <= t and 0 < t 2381 Note q <= t by modN_card_lower, 1 < k, n IN N 2382 and h <> 0 by 0 < h 2383 so h ** 2 <> 0 by EXP_2, MULT_EQ_0, h <> 0 2384 so 0 < t by 0 <> h ** 2 <= q (given), q <= t 2385 2386 Step 1: show n ** SQRT t < 2 ** (h * SQRT t) [1] 2387 Note 0 < SQRT t by SQRT_EQ_0, MULT_EQ_0, 0 < t 2388 and n < 2 ** h by given 2389 ==> n ** SQRT t < (2 ** h) ** SQRT t by EXP_EXP_LT_MONO, 0 < SQRT t 2390 and = 2 ** (h * SQRT t) by EXP_EXP_MULT 2391 Thus n ** SQRT t < 2 ** (h * SQRT t) by inequalities 2392 2393 Step 2: show 2 ** (h * SQRT t) <= 2 ** MIN p t [2] 2394 Since base 2 is the same, we can just show: 2395 h * SQRT t <= MIN p t by EXP_BASE_LE_MONO 2396 Easy part: show h * SQRT t <= p 2397 Note t <= phi k by modN_card_upper_better, 1 < k 2398 ==> SQRT t <= SQRT (phi k) by SQRT_LE, t <= phi k 2399 or h * SQRT t <= p by p = SQRT (phi k) * h 2400 Hard part: show h * SQRT t <= t 2401 Since h ** 2 <= q by given 2402 ==> h <= SQRT q by SQRT_LE, SQRT_OF_SQ 2403 Note q <= t by modN_card_lower, above 2404 ==> SQRT q <= SQRT t by SQRT_LE, q <= t 2405 2406 Thus h * SQRT t <= SQRT q * SQRT t by LESS_MONO_MULT 2407 <= SQRT t * SQRT t by LESS_MONO_MULT 2408 <= t by SQ_SQRT_LE 2409 2410 With both (h * SQRT t <= p) /\ (h * SQRT t <= t) 2411 ==> h * SQRT t <= MIN s t by MIN_DEF 2412 2413 Combining [1] and [2], the result follows. 2414*) 2415val modN_card_in_exp_lt_bound_2 = store_thm( 2416 "modN_card_in_exp_lt_bound_2", 2417 ``!r:'a ring. Ring r ==> !k n s:num. 1 < k /\ n IN N ==> 2418 !h. 0 < h /\ n < 2 ** h /\ h ** 2 <= ordz k n ==> 2419 n ** SQRT (CARD M) < 2 ** MIN (SQRT (phi k) * h) (CARD M)``, 2420 rpt strip_tac >> 2421 qabbrev_tac `t = CARD M` >> 2422 qabbrev_tac `p = SQRT (phi k) * h` >> 2423 qabbrev_tac `q = ordz k n` >> 2424 `q <= t` by rw[modN_card_lower, Abbr`q`, Abbr`t`] >> 2425 `h <> 0` by decide_tac >> 2426 `h ** 2 <> 0` by metis_tac[EXP_2, MULT_EQ_0] >> 2427 `0 < t` by decide_tac >> 2428 `n ** SQRT t < 2 ** (h * SQRT t)` by 2429 (`0 < SQRT t` by metis_tac[SQRT_EQ_0, MULT_EQ_0, NOT_ZERO_LT_ZERO] >> 2430 `n ** SQRT t < (2 ** h) ** SQRT t` by rw[EXP_EXP_LT_MONO] >> 2431 `(2 ** h) ** SQRT t = 2 ** (h * SQRT t)` by rw[EXP_EXP_MULT] >> 2432 decide_tac) >> 2433 `2 ** (h * SQRT t) <= 2 ** MIN p t` by 2434 (`h * SQRT t <= MIN p t` suffices_by rw[EXP_BASE_LE_MONO] >> 2435 `t <= phi k` by rw[modN_card_upper_better, Abbr`t`] >> 2436 `SQRT t <= SQRT (phi k)` by rw[SQRT_LE] >> 2437 `h * SQRT t <= p` by rw_tac arith_ss[Abbr`p`] >> 2438 `h <= SQRT q` by metis_tac[SQRT_LE, SQRT_OF_SQ] >> 2439 `h * SQRT t <= SQRT q * SQRT t` by rw_tac arith_ss[] >> 2440 `SQRT q <= SQRT t` by rw[SQRT_LE] >> 2441 `SQRT q * SQRT t <= SQRT t * SQRT t` by rw_tac arith_ss[] >> 2442 `SQRT t * SQRT t <= t` by rw[SQ_SQRT_LE] >> 2443 `h * SQRT t <= t` by decide_tac >> 2444 metis_tac[MIN_DEF]) >> 2445 decide_tac); 2446 2447(* Theorem: 1 < k /\ 1 < n /\ ~(perfect_power n 2) /\ n IN N /\ (ulog n) ** 2 <= ordz k n ==> 2448 n ** SQRT (CARD M) < 2 ** MIN (SQRT (phi k) * (ulog n)) (CARD M) *) 2449(* Proof: 2450 Note 0 < ulog n by ulog_pos, 1 < n 2451 and n < 2 ** (ulog n) by ulog_property_not_exact, ~(perfect_power 2 n) 2452 Let h = ulog n in modN_card_in_exp_lt_bound_2, the result follows. 2453*) 2454val modN_card_in_exp_lt_bound_3 = store_thm( 2455 "modN_card_in_exp_lt_bound_3", 2456 ``!r:'a ring. Ring r ==> 2457 !k n s:num. 1 < k /\ 1 < n /\ ~(perfect_power n 2) /\ n IN N /\ (ulog n) ** 2 <= ordz k n ==> 2458 n ** SQRT (CARD M) < 2 ** MIN (SQRT (phi k) * (ulog n)) (CARD M)``, 2459 rw[modN_card_in_exp_lt_bound_2, ulog_property_not_exact]); 2460 2461(* Theorem: Ring r ==> 2462 !k n s. 1 < k /\ 1 < n /\ ~(perfect_power n 2) /\ 2463 n IN N /\ (ulog n) ** 2 <= ordz k n /\ 2464 (s = SQRT (phi k) * (ulog n)) ==> 2465 n ** SQRT (CARD M) < 2 ** MIN s (CARD M) *) 2466(* Proof: by modN_card_in_exp_lt_bound_3 *) 2467val modN_card_in_exp_lt_bound_3_alt = store_thm( 2468 "modN_card_in_exp_lt_bound_3_alt", 2469 ``!r:'a ring. Ring r ==> 2470 !n a k s. 1 < k /\ 1 < n /\ ~(perfect_power n 2) /\ 2471 (a = (ulog n) ** 2) /\ (s = SQRT (phi k) * (ulog n)) /\ 2472 a <= ordz k n /\ n IN N ==> 2473 n ** SQRT (CARD M) < 2 ** MIN s (CARD M)``, 2474 rw[modN_card_in_exp_lt_bound_3]); 2475 2476(* Theorem: Ring r ==> 2477 !k n s. 1 < k /\ 1 < n /\ ~perfect_power n 2 /\ n IN N /\ 2478 (2 * ulog n) ** 2 <= ordz k n ==> 2479 n ** (2 * SQRT (CARD M)) < 2 ** MIN (2 * SQRT (phi k) * ulog n) (CARD M) *) 2480(* Proof: 2481 Let t = CARD M 2482 h = ordz k n 2483 m = ulog n 2484 c = 2 * SQRT (phi k) * m 2485 and the goal: n ** (2 * SQRT t) < 2 ** MIN c t 2486 2487 This is proved by two parts: 2488 (1) n ** (2 * SQRT t) < (2 ** m) ** (2 * SQRT t) 2489 (2) (2 ** m) ** (2 * SQRT t) <= 2 ** MIN c t 2490 2491 Claim: n ** (2 * SQRT t) < (2 ** m) ** (2 * SQRT t) 2492 Proof: Note ~perfect_power n 2 by given 2493 ==> n < 2 ** m by ulog_property_not_exact 2494 Thus n ** (2 * SQRT t) < (2 ** m) ** (2 * SQRT t) by EXP_EXP_LT_MONO, (1) 2495 2496 Claim: (2 ** m) ** (2 * SQRT t) <= 2 ** MIN c t 2497 Proof: Note 2 * (SQRT t) * m <= MIN c t by modN_card_with_ulog_le_min_2 2498 so 2 ** (2 * (SQRT t) * m) <= 2 ** MIN c t by EXP_BASE_LE_MONO 2499 or (2 ** m) ** (2 * SQRT t) <= 2 ** MIN c t by EXP_EXP_MULT, (2) 2500 2501 Overall, n ** (2 * SQRT t) < 2 ** MIN c t by (1), (2) 2502*) 2503val modN_card_in_exp_lt_bound_4 = store_thm( 2504 "modN_card_in_exp_lt_bound_4", 2505 ``!(r:'a ring). Ring r ==> 2506 !k n s:num. 1 < k /\ 1 < n /\ ~perfect_power n 2 /\ n IN N /\ 2507 (2 * ulog n) ** 2 <= ordz k n ==> 2508 n ** (2 * SQRT (CARD M)) < 2 ** MIN (2 * SQRT (phi k) * ulog n) (CARD M)``, 2509 rpt strip_tac >> 2510 qabbrev_tac `t = CARD M` >> 2511 qabbrev_tac `h = ordz k n` >> 2512 qabbrev_tac `m = ulog n` >> 2513 qabbrev_tac `c = 2 * SQRT (phi k) * m` >> 2514 `n ** (2 * SQRT t) < (2 ** m) ** (2 * SQRT t)` by 2515 (`n < 2 ** m` by rw[ulog_property_not_exact, Abbr`m`] >> 2516 `0 < m` by rw[ulog_pos, MULT_POS, Abbr`m`] >> 2517 `(2 * m) ** 2 <> 0` by rw[] >> 2518 `h <= t` by rw[modN_card_lower, Abbr`h`, Abbr`t`] >> 2519 `0 < t` by decide_tac >> 2520 `0 < SQRT t` by metis_tac[SQRT_EQ_0, MULT_EQ_0, NOT_ZERO] >> 2521 rw[EXP_EXP_LT_MONO]) >> 2522 `2 * (SQRT t) * m <= MIN c t` by rw[modN_card_with_ulog_le_min_2, Abbr`t`, Abbr`h`, Abbr`m`, Abbr`c`] >> 2523 `2 ** (2 * (SQRT t) * m) <= 2 ** MIN c t` by rw[EXP_BASE_LE_MONO] >> 2524 `2 ** (2 * (SQRT t) * m) = 2 ** (m * (2 * SQRT t))` by decide_tac >> 2525 `_ = (2 ** m) ** (2 * SQRT t)` by rw[EXP_EXP_MULT] >> 2526 decide_tac); 2527 2528(* ------------------------------------------------------------------------- *) 2529(* Less-than-or-equal Bounds *) 2530(* ------------------------------------------------------------------------- *) 2531 2532(* Theorem: Ring r ==> 2533 !k n s. 1 < k /\ 1 < n /\ n IN N /\ (2 * ulog n) ** 2 <= ordz k n ==> 2534 n ** (2 * SQRT (CARD M)) <= 2 ** MIN (2 * SQRT (phi k) * ulog n) (CARD M) *) 2535(* Proof: 2536 Let t = CARD M 2537 h = ordz k n 2538 m = ulog n 2539 c = 2 * SQRT (phi k) * m 2540 and the goal: n ** (2 * SQRT t) <= 2 ** MIN c t 2541 2542 This is proved by two parts: 2543 (1) n ** (2 * SQRT t) <= (2 ** m) ** (2 * SQRT t) 2544 (2) (2 ** m) ** (2 * SQRT t) <= 2 ** MIN c t 2545 2546 Claim: n ** (2 * SQRT t) <= (2 ** m) ** (2 * SQRT t) 2547 Proof: Note n <= 2 ** m by ulog_property 2548 Thus n ** (2 * SQRT t) <= (2 ** m) ** (2 * SQRT t) by EXP_EXP_LE_MONO, (1) 2549 2550 Claim: (2 ** m) ** (2 * SQRT t) <= 2 ** MIN c t 2551 Proof: Note 2 * (SQRT t) * m <= MIN c t by modN_card_with_ulog_le_min_2 2552 so 2 ** (2 * (SQRT t) * m) <= 2 ** MIN c t by EXP_BASE_LE_MONO 2553 or (2 ** m) ** (2 * SQRT t) <= 2 ** MIN c t by EXP_EXP_MULT, (2) 2554 2555 Overall, n ** (2 * SQRT t) <= 2 ** MIN c t by (1), (2) 2556*) 2557val modN_card_in_exp_le_bound_0 = store_thm( 2558 "modN_card_in_exp_le_bound_0", 2559 ``!r:'a ring. Ring r ==> 2560 !k n s:num. 1 < k /\ 1 < n /\ n IN N /\ (2 * ulog n) ** 2 <= ordz k n ==> 2561 n ** (2 * SQRT (CARD M)) <= 2 ** MIN (2 * SQRT (phi k) * ulog n) (CARD M)``, 2562 rpt strip_tac >> 2563 qabbrev_tac `t = CARD M` >> 2564 qabbrev_tac `h = ordz k n` >> 2565 qabbrev_tac `m = ulog n` >> 2566 qabbrev_tac `c = 2 * SQRT (phi k) * m` >> 2567 `n ** (2 * SQRT t) <= (2 ** m) ** (2 * SQRT t)` by 2568 (`n <= 2 ** m` by rw[ulog_property, Abbr`m`] >> 2569 rw[EXP_EXP_LE_MONO]) >> 2570 `2 * (SQRT t) * m <= MIN c t` by rw[modN_card_with_ulog_le_min_2, Abbr`t`, Abbr`h`, Abbr`m`, Abbr`c`] >> 2571 `2 ** (2 * (SQRT t) * m) <= 2 ** MIN c t` by rw[EXP_BASE_LE_MONO] >> 2572 `2 ** (2 * (SQRT t) * m) = 2 ** (m * (2 * SQRT t))` by decide_tac >> 2573 `_ = (2 ** m) ** (2 * SQRT t)` by rw[EXP_EXP_MULT] >> 2574 decide_tac); 2575 2576(* Theorem: 1 < k /\ n IN N ==> !h. 0 < h /\ n <= 2 ** h /\ h ** 2 <= ordz k n ==> 2577 n ** SQRT (CARD M) <= 2 ** MIN (SQRT (phi k) * h) (CARD M) *) 2578(* Proof: 2579 Let t = CARD M, p = SQRT (phi k) * h, q = ordz k n 2580 Then the goal is: n ** SQRT t < 2 ** MIN p t 2581 2582 The strategy is to prove in two steps: 2583 (1) show n ** SQRT t < 2 ** (h * SQRT t) 2584 (2) show 2 ** (h * SQRT t) <= 2 ** MIN p t 2585 2586 Step 0: some useful bits, show q <= t and 0 < t 2587 Note q <= t by modN_card_lower, 1 < k, n IN N 2588 and h <> 0 by 0 < h 2589 so h ** 2 <> 0 by EXP_2, MULT_EQ_0, h <> 0 2590 so 0 < t by 0 <> h ** 2 <= q (given), q <= t 2591 2592 Step 1: show n ** SQRT t < 2 ** (h * SQRT t) [1] 2593 Note SQRT t <> 0 by SQRT_EQ_0, MULT_EQ_0, 0 < t 2594 and n <= 2 ** h by given 2595 ==> n ** SQRT t <= (2 ** h) ** SQRT t by EXP_EXP_LE_MONO, SQRT t <> 0 2596 and = 2 ** (h * SQRT t) by EXP_EXP_MULT 2597 Thus n ** SQRT t <= 2 ** (h * SQRT t) by inequalities 2598 2599 Step 2: show 2 ** (h * SQRT t) <= 2 ** MIN p t [2] 2600 Since base 2 is the same, we can just show: 2601 h * SQRT t <= MIN p t by EXP_BASE_LE_MONO 2602 Easy part: show h * SQRT t <= p 2603 Note t <= phi k by modN_card_upper_better, 1 < k 2604 ==> SQRT t <= SQRT (phi k) by SQRT_LE, t <= phi k 2605 or h * SQRT t <= p by p = SQRT (phi k) * h 2606 Hard part: show h * SQRT t <= t 2607 Since h ** 2 <= q by given 2608 ==> h <= SQRT q by SQRT_LE, SQRT_OF_SQ 2609 Note q <= t by modN_card_lower, above 2610 ==> SQRT q <= SQRT t by SQRT_LE, q <= t 2611 2612 Thus h * SQRT t <= SQRT q * SQRT t by LESS_MONO_MULT 2613 <= SQRT t * SQRT t by LESS_MONO_MULT 2614 <= t by SQ_SQRT_LE 2615 2616 With both (h * SQRT t <= p) /\ (h * SQRT t <= t) 2617 ==> h * SQRT t <= MIN s t by MIN_DEF 2618 2619 Combining [1] and [2], the result follows. 2620*) 2621val modN_card_in_exp_le_bound_1 = store_thm( 2622 "modN_card_in_exp_le_bound_1", 2623 ``!r:'a ring. Ring r ==> !k n s:num. 1 < k /\ n IN N ==> 2624 !h. 0 < h /\ n <= 2 ** h /\ h ** 2 <= ordz k n ==> 2625 n ** SQRT (CARD M) <= 2 ** MIN (SQRT (phi k) * h) (CARD M)``, 2626 rpt strip_tac >> 2627 qabbrev_tac `t = CARD M` >> 2628 qabbrev_tac `p = SQRT (phi k) * h` >> 2629 qabbrev_tac `q = ordz k n` >> 2630 `q <= t` by rw[modN_card_lower, Abbr`q`, Abbr`t`] >> 2631 `h <> 0` by decide_tac >> 2632 `h ** 2 <> 0` by metis_tac[EXP_2, MULT_EQ_0] >> 2633 `t <> 0` by decide_tac >> 2634 `n ** SQRT t <= 2 ** (h * SQRT t)` by 2635 (`SQRT t <> 0` by metis_tac[SQRT_EQ_0, MULT_EQ_0] >> 2636 `n ** SQRT t <= (2 ** h) ** SQRT t` by rw[EXP_EXP_LE_MONO] >> 2637 `(2 ** h) ** SQRT t = 2 ** (h * SQRT t)` by rw[EXP_EXP_MULT] >> 2638 decide_tac) >> 2639 `2 ** (h * SQRT t) <= 2 ** MIN p t` by 2640 (`h * SQRT t <= MIN p t` suffices_by rw[EXP_BASE_LE_MONO] >> 2641 `t <= phi k` by rw[modN_card_upper_better, Abbr`t`] >> 2642 `SQRT t <= SQRT (phi k)` by rw[SQRT_LE] >> 2643 `h * SQRT t <= p` by rw_tac arith_ss[Abbr`p`] >> 2644 `h <= SQRT q` by metis_tac[SQRT_LE, SQRT_OF_SQ] >> 2645 `h * SQRT t <= SQRT q * SQRT t` by rw_tac arith_ss[] >> 2646 `SQRT q <= SQRT t` by rw[SQRT_LE] >> 2647 `SQRT q * SQRT t <= SQRT t * SQRT t` by rw_tac arith_ss[] >> 2648 `SQRT t * SQRT t <= t` by rw[SQ_SQRT_LE] >> 2649 `h * SQRT t <= t` by decide_tac >> 2650 metis_tac[MIN_DEF]) >> 2651 decide_tac); 2652 2653(* Theorem: 1 < k /\ 1 < n /\ n IN N /\ (ulog n) ** 2 <= ordz k n ==> 2654 n ** SQRT (CARD M) <= 2 ** MIN (SQRT (phi k) * (ulog n)) (CARD M) *) 2655(* Proof: 2656 Note 0 < ulog n by ulog_pos, 1 < n 2657 and n <= 2 ** (ulog n) by ulog_property, 0 < n 2658 Let h = ulog n in modN_card_in_exp_le_bound_1, the result follows. 2659*) 2660val modN_card_in_exp_le_bound_2 = store_thm( 2661 "modN_card_in_exp_le_bound_2", 2662 ``!r:'a ring. Ring r ==> 2663 !k n s:num. 1 < k /\ 1 < n /\ n IN N /\ (ulog n) ** 2 <= ordz k n ==> 2664 n ** SQRT (CARD M) <= 2 ** MIN (SQRT (phi k) * (ulog n)) (CARD M)``, 2665 rw[modN_card_in_exp_le_bound_1, ulog_property]); 2666 2667(* Theorem: coprime k (CARD R) /\ 1 < ordz k (CARD R) /\ 2668 char r divides n /\ n IN N /\ ~perfect_power n (char r) /\ mifactor z (unity k) /\ 2669 ulog n ** 2 <= ordz k n ==> 2670 CARD (Q z) <= 2 ** MIN (SQRT (phi k) * ulog n) (CARD M) *) 2671(* Proof: 2672 Note 1 < CARD R by finite_field_card_gt_1 2673 so 1 < k by ZN_order_with_coprime_1 2674 Also n <> 0 by setN_has_no_0, 1 < k 2675 and char r <> 1 by field_char_ne_1 2676 so n <> 1 by DIVIDES_ONE 2677 ==> 1 < n by n <> 0, n <> 1 2678 Let u = SQRT (phi k) * ulog n, t = CARD M. 2679 CARD (Q z) 2680 <= n ** SQRT t by modP_card_upper_better 2681 <= 2 ** MIN u t by modN_card_in_exp_le_bound_2 2682 The result follows by LESS_EQ_TRANS 2683*) 2684val modP_card_upper_better_3 = store_thm( 2685 "modP_card_upper_better_3", 2686 ``!r:'a field k n s:num z. FiniteField r /\ coprime k (CARD R) /\ 1 < ordz k (CARD R) /\ 2687 char r divides n /\ n IN N /\ ~perfect_power n (char r) /\ mifactor z (unity k) /\ 2688 ulog n ** 2 <= ordz k n ==> 2689 CARD (Q z) <= 2 ** MIN (SQRT (phi k) * ulog n) (CARD M)``, 2690 rpt (stripDup[FiniteField_def]) >> 2691 `1 < CARD R` by rw[finite_field_card_gt_1] >> 2692 `1 < k` by metis_tac[ZN_order_with_coprime_1] >> 2693 `1 < n` by 2694 (`n <> 0` by metis_tac[setN_has_no_0] >> 2695 `n <> 1` by metis_tac[DIVIDES_ONE, field_char_ne_1] >> 2696 decide_tac) >> 2697 qabbrev_tac `u = SQRT (phi k) * ulog n` >> 2698 qabbrev_tac `t = CARD M` >> 2699 `CARD (Q z) <= n ** SQRT t` by rw[modP_card_upper_better, Abbr`t`] >> 2700 `n ** SQRT t <= 2 ** MIN u t` by rw[modN_card_in_exp_le_bound_2, Abbr`u`, Abbr`t`] >> 2701 decide_tac); 2702 2703(* Theorem: FiniteField r /\ 2704 mifactor z (unity k) /\ 1 < deg z /\ (forderz X = k) /\ (* conditions on z *) 2705 1 < n /\ n IN N /\ (ulog n) ** 2 <= ordz k n /\ (* conditions on n *) 2706 (s = SQRT (phi k) * ulog n) /\ s < char r ==> n ** SQRT (CARD M) < CARD (Q z) *) 2707(* Proof: 2708 Note n <> 0 and n <> 1 by 1 < n 2709 Thus ulog n <> 0 by ulog_eq_0 2710 Also 1 < k by poly_X_order_gt_1, ipoly z 2711 Note (ulog n) ** 2 <> 0 by SQ_EQ_0, EXP_2 2712 so ordz k n <> 0 by (ulog n) ** 2 <= ordz k n 2713 2714 Claim: ordz k n <> 1 2715 Proof: If n = 2, 2716 By contradiction, assue ordz k n = 1. 2717 Then k divides 2 ** 1 - 1 by ZN_order_divisibility, 0 < k 2718 Thus k = 1 by DIVIDES_ONE 2719 which contradicts 1 < k. 2720 If n <> 2, 2721 Then ulog n <> 1 by ulog_eq_1 2722 so (ulog n) ** 2 <> 1 by SQ_EQ_1 2723 or ordz k n <> 1 by (ulog n) ** 2 <= ordz k n 2724 2725 Therefore, 1 < ordz k n by ordz k n <> 0, ordz k n <> 1 2726 Note ordz k n <= CARD M by modN_card_lower 2727 Thus 1 < CARD M by 1 < ordz k n 2728 2729 Claim: 0 < s 2730 Proof: Note k <> 0 by 1 < k 2731 ==> phi k <> 0 by phi_eq_0 2732 ==> SQRT (phi k) <> 0 by SQRT_EQ_0 2733 Thus s <> 0 by s = SQRT (phi k) * ulog n), MULT_EQ_0 2734 or 0 < s 2735 2736 Thus 2 ** MIN s (CARD M) < CARD (Q z) by modP_card_lower_better 2737 Note n <= 2 ** ulog n by ulog_property 2738 Thus n ** SQRT (CARD M) <= 2 ** MIN s (CARD M) 2739 by modN_card_in_exp_le_bound_1 2740 The result follows. 2741*) 2742val modP_card_lower_better_3 = store_thm( 2743 "modP_card_lower_better_3", 2744 ``!r:'a field k n s z. FiniteField r /\ 2745 mifactor z (unity k) /\ 1 < deg z /\ (forderz X = k) /\ (* conditions on z *) 2746 1 < n /\ n IN N /\ (ulog n) ** 2 <= ordz k n /\ (* conditions on n *) 2747 (s = SQRT (phi k) * ulog n) /\ s < char r ==> n ** SQRT (CARD M) < CARD (Q z)``, 2748 rpt (stripDup[FiniteField_def]) >> 2749 `ulog n <> 0` by metis_tac[ulog_eq_0, DECIDE``1n < n ==> ~(n = 0) /\ ~(n = 1)``] >> 2750 `0 < ulog n` by decide_tac >> 2751 `1 < k` by rw[poly_X_order_gt_1] >> 2752 `1 < ordz k n` by 2753 (`(ulog n) ** 2 <> 0` by metis_tac[SQ_EQ_0, EXP_2] >> 2754 `ordz k n <> 0` by decide_tac >> 2755 `ordz k n <> 1` by 2756 (Cases_on `n = 2` >| [ 2757 spose_not_then strip_assume_tac >> 2758 `0 < k` by decide_tac >> 2759 `k divides 2 ** 1 - 1` by metis_tac[ZN_order_divisibility] >> 2760 fs[DIVIDES_ONE], 2761 `ulog n <> 1` by fs[ulog_eq_1] >> 2762 `(ulog n) ** 2 <> 1` by fs[SQ_EQ_1] >> 2763 decide_tac 2764 ]) >> 2765 decide_tac) >> 2766 `ordz k n <= CARD M` by rw[modN_card_lower] >> 2767 `1 < CARD M` by decide_tac >> 2768 `0 < s` by 2769 (`k <> 0` by decide_tac >> 2770 `phi k <> 0` by rw[phi_eq_0] >> 2771 `SQRT (phi k) <> 0` by metis_tac[SQRT_EQ_0] >> 2772 `s <> 0` by metis_tac[MULT_EQ_0] >> 2773 decide_tac) >> 2774 `2 ** MIN s (CARD M) < CARD (Q z)` by rw[modP_card_lower_better] >> 2775 `n <= 2 ** ulog n` by rw[ulog_property] >> 2776 `n ** SQRT (CARD M) <= 2 ** MIN s (CARD M)` by rw[modN_card_in_exp_le_bound_1] >> 2777 decide_tac); 2778 2779(* ------------------------------------------------------------------------- *) 2780 2781(* export theory at end *) 2782val _ = export_theory(); 2783 2784(*===========================================================================*) 2785