PolynomialWeightedControls.lean

1 module
2 public import PolynomialPadicUnique
3 public import Mathlib.Tactic
4 
5 @[expose] public section
6 noncomputable section
7 set_option autoImplicit false
8 
9 namespace Komorebi.PolynomialWeightedControls
10 open MvPolynomial Komorebi.PolynomialPadicUnique
11 
12 /-- The excluded binary boundary is an actual polynomial over the p-adic integers. -/
13 def squarePlusThree : MvPolynomial (Fin 1) ℤ_[2] := X 0 ^ 2 + C 3
14 
15 /-- At a = 1 the residual has depth exactly two, while the derivative has depth one. -/
16 theorem boundary_residual_derivative :
17     eval (fun _ : Fin 1 => (1 : ℤ_[2])) squarePlusThree = 4 ∧
18     eval (fun _ : Fin 1 => (1 : ℤ_[2])) (pderiv 0 squarePlusThree) = 2 := by
19   norm_num [squarePlusThree]
20 
21 /-- The scalar effective inverse A = 1 clears the derivative denominator with s = 1. -/
22 theorem boundary_scaled_inverse :
23     (1 : ℤ_[2]) * eval (fun _ : Fin 1 => (1 : ℤ_[2]))
24       (pderiv 0 squarePlusThree) = (2 : ℤ_[2]) ^ 1 ∧
25     eval (fun _ : Fin 1 => (1 : ℤ_[2])) (pderiv 0 squarePlusThree) *
26       (1 : ℤ_[2]) = (2 : ℤ_[2]) ^ 1 := by
27   simp [boundary_residual_derivative.2]
28 
29 /-- No residue class modulo eight solves X^2 + 3 = 0. -/
30 theorem boundary_no_mod_eight (t : ZMod 8) : t ^ 2 + 3 ≠ 0 := by
31   have h : ∀ x : ZMod 8, x ^ 2 + 3 ≠ 0 := by decide
32   exact h t
33 
34 /-- Consequently the excluded boundary does not even admit a p-adic root. -/
35 theorem boundary_no_padic_root (a : Fin 1 → ℤ_[2]) :
36     eval a squarePlusThree ≠ 0 := by
37   intro h
38   have h8 := congrArg (PadicInt.toZModPow 3) h
39   have heq : (PadicInt.toZModPow 3 (a 0)) ^ 2 + 3 = 0 := by
40     simpa only [squarePlusThree, map_add, map_pow, eval_X, eval_C,
41       map_ofNat, map_zero] using h8
42   exact boundary_no_mod_eight (PadicInt.toZModPow 3 (a 0)) heq
43 
44 /-- Existence-form refutation for the strict-threshold negative control. -/
45 theorem boundary_no_root :
46     ¬ ∃ a : Fin 1 → ℤ_[2], eval a squarePlusThree = 0 := by
47   rintro ⟨a, ha⟩
48   exact boundary_no_padic_root a ha
49 
50 /-- Powers of p have their stated exact depth in the actual p-adic integers. -/
51 theorem prime_power_exact_depth (p k : ℕ) [Fact (Nat.Prime p)] :
52     ¬ (p : ℤ_[p]) ^ (k + 1) ∣ (p : ℤ_[p]) ^ k := by
53   intro h
54   have hz : (p : ℤ) ^ (k + 1) ∣ (p : ℤ) ^ k := by
55     apply (int_pow_dvd_iff p (k + 1) ((p : ℤ) ^ k)).mpr
56     simpa using h
57   have hn : p ^ (k + 1) ∣ p ^ k := by exact_mod_cast hz
58   have hle := (Nat.pow_dvd_pow_iff_le_right (Fact.out : Nat.Prime p).one_lt).mp hn
59   omega
60 
61 /-- The boundary residual is divisible by p^r at r = 2s, and not at r + 1. -/
62 theorem boundary_exact_residual_depth :
63     (2 : ℤ_[2]) ^ 2 ∣ eval (fun _ : Fin 1 => (1 : ℤ_[2])) squarePlusThree ∧
64     ¬ (2 : ℤ_[2]) ^ 3 ∣ eval (fun _ : Fin 1 => (1 : ℤ_[2])) squarePlusThree := by
65   rw [boundary_residual_derivative.1]
66   constructor
67   · norm_num
68   · convert prime_power_exact_depth 2 2 using 1
69     norm_num
70 
71 /-- A scalar linear polynomial realizes the full loss of s digits. -/
72 def weightedLinear (p s : ℕ) [Fact (Nat.Prime p)] :
73     MvPolynomial (Fin 1) ℤ_[p] := C ((p : ℤ_[p]) ^ s) * X 0
74 
75 /-- The root after adding p^M is exactly -p^(M-s). -/
76 theorem linear_perturbation_root (p s M : ℕ) [Fact (Nat.Prime p)] (hM : s ≤ M) :
77     eval (fun _ : Fin 1 => -(p : ℤ_[p]) ^ (M - s))
78       (weightedLinear p s + C ((p : ℤ_[p]) ^ M)) = 0 := by
79   simp only [weightedLinear, map_add, map_mul, eval_C, eval_X, mul_neg]
80   rw [← pow_add, Nat.add_sub_of_le hM]
81   ring
82 
83 /-- No uniformly stronger displacement depth is possible, even in dimension one. -/
84 theorem linear_displacement_sharp (p s M : ℕ) [Fact (Nat.Prime p)] :
85     (p : ℤ_[p]) ^ (M - s) ∣ -(p : ℤ_[p]) ^ (M - s) ∧
86     ¬ (p : ℤ_[p]) ^ (M - s + 1) ∣ -(p : ℤ_[p]) ^ (M - s) := by
87   constructor
88   · exact dvd_neg.mpr dvd_rfl
89   · intro h
90     exact prime_power_exact_depth p (M - s) (dvd_neg.mp h)
91 
92 end Komorebi.PolynomialWeightedControls

Back to source controls