PolynomialIntegerTower.lean

1 module
2 public import PolynomialSurjectiveStep
3 
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 
8 namespace Komorebi.PolynomialIntegerTower
9 open Komorebi.PolynomialObstruction Komorebi.PolynomialDigitBridge
10 open Komorebi.PolynomialSurjectiveStep
11 variable {d e : ℕ}
12 
13 /-- Surjectivity of the actual reduced Jacobian produces a single compatible
14 sequence of integer polynomial solutions at every higher precision. The initial
15 point is kept exactly, and no primality assumption on the positive base is needed. -/
16 theorem exists_compatible_tower (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L)
17     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
18     (hx : ∀ i, (q : ℤ)^L ∣ evalSystem F x i)
19     (hJ : Function.Surjective (digitJacobian q F x)) :
20     ∃ z : ℕ → Fin d → ℤ,
21       z 0 = x ∧
22       (∀ n i, (q : ℤ)^(L+n) ∣ evalSystem F (z n) i) ∧
23       (∀ n i, (q : ℤ)^(L+n) ∣ (z (n+1) - z n) i) ∧
24       (∀ n, Function.Surjective (digitJacobian q F (z n))) := by
25   let State (n : ℕ) :=
26     {y : Fin d → ℤ // (∀ i, (q : ℤ)^(L+n) ∣ evalSystem F y i) ∧
27       Function.Surjective (digitJacobian q F y)}
28   have advance (n : ℕ) (y : State n) :
29       ∃ w : State (n+1), ∀ i, (q : ℤ)^(L+n) ∣ (w.val - y.val) i := by
30     obtain ⟨w, hcong, hroot, hsurj⟩ :=
31       one_step_lift q (L+n) hq (by omega) F y.val y.property.1 y.property.2
32     refine ⟨⟨w, ?_, hsurj⟩, hcong⟩
33     simpa only [Nat.add_assoc] using hroot
34   let next (n : ℕ) (y : State n) : State (n+1) := Classical.choose (advance n y)
35   let initial : State 0 := ⟨x, by simpa only [Nat.add_zero] using hx, hJ⟩
36   let state : (n : ℕ) → State n := fun n => Nat.rec initial (fun k y => next k y) n
37   refine ⟨fun n => (state n).val, rfl, ?_, ?_, ?_⟩
38   · exact fun n => (state n).property.1
39   · intro n
40     exact Classical.choose_spec (advance n (state n))
41   · exact fun n => (state n).property.2
42 
43 /-- Adjacent compatibility implies compatibility between any two levels,
44 with the modulus at the earlier level. -/
45 theorem tower_pairwise_congruent (q L : ℕ) (z : ℕ → Fin d → ℤ)
46     (hstep : ∀ n i, (q : ℤ)^(L+n) ∣ (z (n+1) - z n) i)
47     (m n : ℕ) (hmn : m ≤ n) :
48     ∀ i, (q : ℤ)^(L+m) ∣ (z n - z m) i := by
49   induction n, hmn using Nat.le_induction with
50   | base =>
51     intro i
52     simp
53   | succ n hmn ih =>
54     intro i
55     have hs : (q : ℤ)^(L+m) ∣ (z (n+1) - z n) i :=
56       dvd_trans (pow_dvd_pow (q : ℤ) (Nat.add_le_add_left hmn L)) (hstep n i)
57     have hsum := dvd_add hs (ih i)
58     simpa only [Pi.sub_apply, sub_add_sub_cancel] using hsum
59 
60 /-- Every level of a compatible integer tower retains the initial residue. -/
61 theorem tower_initial_congruent (q L : ℕ) (z : ℕ → Fin d → ℤ)
62     (hstep : ∀ n i, (q : ℤ)^(L+n) ∣ (z (n+1) - z n) i)
63     (n : ℕ) : ∀ i, (q : ℤ)^L ∣ (z n - z 0) i := by
64   simpa only [Nat.add_zero] using
65     tower_pairwise_congruent q L z hstep 0 n (Nat.zero_le n)
66 
67 /-- Along a positive-depth compatible tower, the finite-ring Jacobian itself
68 is constant, rather than only its rank or its surjectivity. -/
69 theorem tower_digitJacobian_eq (q L : ℕ) (hL : 1 ≤ L)
70     (F : Fin e → MvPolynomial (Fin d) ℤ) (z : ℕ → Fin d → ℤ)
71     (hstep : ∀ n i, (q : ℤ)^(L+n) ∣ (z (n+1) - z n) i)
72     (n : ℕ) : digitJacobian q F (z n) = digitJacobian q F (z 0) := by
73   apply digitJacobian_eq
74   intro i
75   exact dvd_trans (dvd_pow_self (q : ℤ) (by omega : L ≠ 0))
76     (tower_initial_congruent q L z hstep n i)
77 
78 /-- The strengthened tower certificate includes all cross-level congruences
79 and equality to one fixed reduced Jacobian. -/
80 theorem exists_compatible_tower_strong (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L)
81     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
82     (hx : ∀ i, (q : ℤ)^L ∣ evalSystem F x i)
83     (hJ : Function.Surjective (digitJacobian q F x)) :
84     ∃ z : ℕ → Fin d → ℤ,
85       z 0 = x ∧
86       (∀ n i, (q : ℤ)^(L+n) ∣ evalSystem F (z n) i) ∧
87       (∀ n i, (q : ℤ)^(L+n) ∣ (z (n+1) - z n) i) ∧
88       (∀ m n, m ≤ n → ∀ i, (q : ℤ)^(L+m) ∣ (z n - z m) i) ∧
89       (∀ n, digitJacobian q F (z n) = digitJacobian q F x) ∧
90       (∀ n, Function.Surjective (digitJacobian q F (z n))) := by
91   obtain ⟨z, hz0, hroot, hstep, hsurj⟩ := exists_compatible_tower q L hq hL F x hx hJ
92   refine ⟨z, hz0, hroot, hstep, ?_, ?_, hsurj⟩
93   · exact fun m n hmn => tower_pairwise_congruent q L z hstep m n hmn
94   · intro n
95     rw [← hz0]
96     exact tower_digitJacobian_eq q L hL F z hstep n
97 
98 end Komorebi.PolynomialIntegerTower

Back to source controls