QuadraticPacketBoundary.lean

1 import Mathlib.NumberTheory.Padics.RingHoms
2 import Mathlib.Algebra.Ring.Commute
3 import Mathlib.Tactic
4 
5 /-! Exact arithmetic boundaries for the dyadic quadratic packet equation.
6 The finite roots are computed in the actual quotient rings.  In particular,
7 an occupied node at precision three need not have a child at precision four.
8 -/
9 set_option autoImplicit false
10 namespace PaperX.QuadraticPacketBoundary
11 
12 /-- There are exactly two integral dyadic roots, since the integers are a domain. -/
13 theorem dyadic_roots (x : ℤ_[2]) : x ^ 2 = 1 ↔ x = 1 ∨ x = -1 :=
14   sq_eq_one_iff
15 
16 theorem dyadic_signs_distinct : (1 : ℤ_[2]) ≠ -1 := by norm_num
17 
18 /-- The two integral packets have the same residual value. -/
19 theorem signs_same_mod_two :
20     (PadicInt.toZMod : ℤ_[2] →+* ZMod 2) 1 =
21       (PadicInt.toZMod : ℤ_[2] →+* ZMod 2) (-1) := by
22   simp
23 
24 /-- The actual reduction modulo four separates them. -/
25 theorem signs_distinct_mod_four :
26     (PadicInt.toZModPow 2 : ℤ_[2] →+* ZMod 4) 1 ≠
27       (PadicInt.toZModPow 2 : ℤ_[2] →+* ZMod 4) (-1) := by
28   simpa only [map_one, map_neg] using (by decide : (1 : ZMod 4) ≠ -1)
29 
30 def reduceSixteen : ZMod 16 →+* ZMod 8 := ZMod.castHom (by decide) (ZMod 8)
31 
32 theorem three_root_mod_eight : (3 : ZMod 8) ^ 2 = 1 := by decide +kernel
33 
34 theorem three_not_sign_mod_eight : (3 : ZMod 8) ≠ 1 ∧ (3 : ZMod 8) ≠ -1 := by
35   decide +kernel
36 
37 /-- The quotient ring has four roots, although the integral ring has only two. -/
38 theorem roots_mod_eight (x : ZMod 8) :
39     x ^ 2 = 1 ↔ x = 1 ∨ x = 3 ∨ x = 5 ∨ x = 7 := by
40   revert x
41   decide +kernel
42 
43 theorem roots_mod_sixteen (x : ZMod 16) :
44     x ^ 2 = 1 ↔ x = 1 ∨ x = 7 ∨ x = 9 ∨ x = 15 := by
45   revert x
46   decide +kernel
47 
48 /-- Only the reductions of the two integral signs have children at this step. -/
49 theorem has_root_lift_mod_sixteen (x : ZMod 8) :
50     (∃ y : ZMod 16, y ^ 2 = 1 ∧ reduceSixteen y = x) ↔ x = 1 ∨ x = -1 := by
51   revert x
52   decide +kernel
53 
54 theorem three_no_root_lift_mod_sixteen :
55     ¬ ∃ y : ZMod 16, y ^ 2 = 1 ∧ reduceSixteen y = 3 := by
56   rw [has_root_lift_mod_sixteen]
57   exact not_or_intro three_not_sign_mod_eight.1 three_not_sign_mod_eight.2
58 
59 /-- A finite admissible scalar can therefore fail to lift to any integral packet. -/
60 theorem three_no_integral_root_lift :
61     ¬ ∃ x : ℤ_[2], x ^ 2 = 1 ∧ PadicInt.toZModPow 3 x = 3 := by
62   rintro ⟨x, hx, hr⟩
63   rcases (dyadic_roots x).mp hx with rfl | rfl
64   · exact three_not_sign_mod_eight.1 (by simpa only [map_one] using hr.symm)
65   · exact three_not_sign_mod_eight.2 (by simpa only [map_neg, map_one] using hr.symm)
66 
67 end PaperX.QuadraticPacketBoundary

Back to source controls