PolynomialPrescribedControls.lean

1 module
2 public import PolynomialPrescribedLifts
3 
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 
8 namespace Komorebi.PolynomialPrescribedControls
9 
10 open MvPolynomial PolynomialDigitBridge PolynomialPrescribedSystem
11 open PolynomialPrescribedLifts PolynomialParameterSystem
12 open PolynomialObstruction NativeAffine FiniteFiberCounts
13 
14 /-- The equation only sees the parameter coordinate. -/
15 def parameterOnly : Fin 1 → MvPolynomial (Fin (1 + 1)) ℤ := fun _ => X 1
16 
17 /-- Full Jacobian surjectivity does not imply freedom to prescribe parameters. -/
18 theorem full_jacobian_surjective :
19     Function.Surjective (digitJacobian 2 parameterOnly (fun _ => 0)) := by
20   intro t
21   refine ⟨![0, t 0], ?_⟩
22   ext i
23   simp [digitJacobian, parameterOnly, Fin.eq_zero i, Fin.sum_univ_two]
24 
25 theorem solved_jacobian_zero :
26     PolynomialPrescribedSystem.solvedJacobian 2 parameterOnly (fun _ => 0) = 0 := by
27   ext u i
28   simp [PolynomialPrescribedSystem.solvedJacobian, parameterOnly, Fin.eq_zero i]
29 
30 /-- The nonzero prescribed parameter digit obstructs lifting already modulo four. -/
31 theorem digit_one_empty :
32     ¬ Nonempty (PrescribedDigits 2 parameterOnly (fun _ => 0) (fun _ => 0) (fun _ => 1)) := by
33   rintro ⟨u, hu⟩
34   have hi := congrFun hu 0
35   norm_num [parameterResidual, reduction, parameterJacobian,
36     PolynomialPrescribedSystem.solvedJacobian, parameterOnly, Pi.single_apply, Fin.ext_iff] at hi
37 
38 /-- A zero parameter digit leaves precisely the solved-coordinate digit free. -/
39 def zeroDigitEquiv :
40     PrescribedDigits 2 parameterOnly (fun _ => 0) (fun _ => 0) (fun _ => 0) ≃
41       (Fin 1 → ZMod 2) where
42   toFun := Subtype.val
43   invFun u := ⟨u, by
44     ext i
45     simp [parameterResidual, reduction, parameterJacobian,
46       PolynomialPrescribedSystem.solvedJacobian, parameterOnly, Fin.eq_zero i]⟩
47   left_inv _ := rfl
48   right_inv _ := rfl
49 
50 theorem zero_digit_card :
51     Nat.card (PrescribedDigits 2 parameterOnly (fun _ => 0) (fun _ => 0) (fun _ => 0)) = 2 := by
52   rw [Nat.card_congr zeroDigitEquiv]
53   simp [Nat.card_eq_fintype_card]
54 
55 theorem zero_residual : evalSystem parameterOnly (fun _ => 0) = (2 : ℤ)^1 • (fun _ => 0) := by
56   ext i
57   simp [evalSystem, parameterOnly]
58 
59 /-- The obstructed digit has no actual next-level polynomial residue lift. -/
60 theorem prescribed_one_no_actual_lift :
61     ¬ Nonempty (PrescribedLifts 2 1 parameterOnly (fun _ => 0) (fun _ => 1)) := by
62   rintro ⟨y⟩
63   exact digit_one_empty ⟨(prescribedDigitEquivLifts 2 1 (by decide) (by decide)
64     parameterOnly (fun _ => 0) (fun _ => 0) zero_residual (fun _ => 1)).symm y⟩
65 
66 /-- The unobstructed digit has exactly two actual residue lifts modulo four. -/
67 theorem prescribed_zero_actual_card :
68     Nat.card (PrescribedLifts 2 1 parameterOnly (fun _ => 0) (fun _ => 0)) = 2 := by
69   rw [← Nat.card_congr (prescribedDigitEquivLifts 2 1 (by decide) (by decide)
70     parameterOnly (fun _ => 0) (fun _ => 0) zero_residual (fun _ => 0))]
71   exact zero_digit_card
72 
73 /-- An odd-prime control distinguishes the required plus sign from a minus sign. -/
74 def parameterPlusThree : Fin 1 → MvPolynomial (Fin (1 + 1)) ℤ := fun _ => X 1 + 1 + 1 + 1
75 
76 theorem three_residual :
77     evalSystem parameterPlusThree (fun _ => 0) = (3 : ℤ)^1 • (fun _ => 1) := by
78   ext i
79   norm_num [evalSystem, parameterPlusThree]
80 
81 theorem digit_one_for_three_empty :
82     ¬ Nonempty (PrescribedDigits 3 parameterPlusThree (fun _ => 0) (fun _ => 1)
83       (fun _ => 1)) := by
84   rintro ⟨u, hu⟩
85   have hi := congrFun hu 0
86   norm_num [parameterResidual, reduction, parameterJacobian,
87     PolynomialPrescribedSystem.solvedJacobian, parameterPlusThree,
88     Pi.single_apply, Fin.ext_iff, MvPolynomial.pderiv_one] at hi
89   exact (by decide : (2 : ZMod 3) ≠ 0) hi
90 
91 theorem digit_two_for_three_exists :
92     Nonempty (PrescribedDigits 3 parameterPlusThree (fun _ => 0) (fun _ => 1)
93       (fun _ => 2)) := by
94   refine ⟨⟨fun _ => 0, ?_⟩⟩
95   ext i
96   norm_num [parameterResidual, reduction, parameterJacobian,
97     PolynomialPrescribedSystem.solvedJacobian, parameterPlusThree,
98     Pi.single_apply, Fin.ext_iff, Fin.eq_zero i, MvPolynomial.pderiv_one]
99   exact (by decide : (3 : ZMod 3) = 0)
100 
101 theorem prescribed_one_for_three_no_actual_lift :
102     ¬ Nonempty (PrescribedLifts 3 1 parameterPlusThree (fun _ => 0) (fun _ => 1)) := by
103   rintro ⟨y⟩
104   exact digit_one_for_three_empty ⟨(prescribedDigitEquivLifts 3 1 (by decide) (by decide)
105     parameterPlusThree (fun _ => 0) (fun _ => 1) three_residual (fun _ => 1)).symm y⟩
106 
107 theorem prescribed_two_for_three_actual_lift :
108     Nonempty (PrescribedLifts 3 1 parameterPlusThree (fun _ => 0) (fun _ => 2)) := by
109   obtain ⟨u⟩ := digit_two_for_three_exists
110   exact ⟨prescribedDigitEquivLifts 3 1 (by decide) (by decide)
111     parameterPlusThree (fun _ => 0) (fun _ => 1) three_residual (fun _ => 2) u⟩
112 
113 end Komorebi.PolynomialPrescribedControls

Back to source controls