PolynomialParameterTowerControls.lean

1 module
2 public import PolynomialPrescribedTowerUnique
3 
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 
8 namespace Komorebi.PolynomialParameterTowerControls
9 
10 open MvPolynomial Komorebi.PolynomialPadicLift Komorebi.PolynomialParameterSystem
11 
12 local instance : Fact (Nat.Prime 2) := ⟨by decide⟩
13 
14 /-- One equation, two solved coordinates, and one parameter. -/
15 def firstSolved : Fin 1 → MvPolynomial (Fin (2 + 1)) ℤ := fun _ => X 0
16 
17 /-- The rectangular solved block is surjective. -/
18 theorem firstSolved_surjective :
19     Function.Surjective (PolynomialPrescribedSystem.solvedJacobian 2 firstSolved (fun _ => 0)) := by
20   intro t
21   refine ⟨![t 0, 0], ?_⟩
22   ext i
23   simp [PolynomialPrescribedSystem.solvedJacobian, firstSolved,
24     Fin.eq_zero i, Fin.sum_univ_two]
25 
26 /-- Surjectivity of a rectangular solved block permits distinct exact roots with the same parameter.
27 Both roots lie in the initial ball modulo two, so square-case uniqueness cannot be generalized. -/
28 theorem rectangular_same_parameter_nonunique :
29     ∃ b c : Fin (2 + 1) → ℤ_[2],
30       (∀ i, padicEval 2 firstSolved b i = 0) ∧
31       (∀ i, padicEval 2 firstSolved c i = 0) ∧
32       (∀ i, (2 : ℤ_[2])^1 ∣ b i - ((0 : Fin (2 + 1) → ℤ) i : ℤ_[2])) ∧
33       (∀ i, (2 : ℤ_[2])^1 ∣ c i - ((0 : Fin (2 + 1) → ℤ) i : ℤ_[2])) ∧
34       freePart (e := 2) (q := 1) b = freePart c ∧ b ≠ c := by
35   refine ⟨![0, 0, 0], ![0, 2, 0], ?_, ?_, ?_, ?_, ?_, ?_⟩
36   · intro i
37     simp [padicEval, firstSolved]
38   · intro i
39     simp [padicEval, firstSolved]
40   · intro i
41     fin_cases i <;> simp
42   · intro i
43     fin_cases i <;> simp
44   · ext j
45     fin_cases j
46     simp [freePart]
47   · intro h
48     have hi := congrFun h 1
49     norm_num at hi
50 
51 end Komorebi.PolynomialParameterTowerControls

Back to source controls