PolynomialPrescribedIntegerTower.lean

1 module
2 public import PolynomialPrescribedStep
3 public import PolynomialIntegerTower
4 
5 @[expose] public section
6 noncomputable section
7 set_option autoImplicit false
8 
9 namespace Komorebi.PolynomialPrescribedIntegerTower
10 
11 open Komorebi.PolynomialObstruction Komorebi.PolynomialDigitBridge
12 open Komorebi.PolynomialIntegerTower
13 open Komorebi.PolynomialPrescribedSystem
14 open Komorebi.PolynomialParameterSystem (freePart join)
15 
16 variable {m k e : ℕ}
17 
18 /-- Every compatible integer parameter path extends to an actual polynomial
19 solution tower. Its parameter coordinates agree with the supplied integers
20 exactly, and only the initial solved-coordinate Jacobian must be surjective. -/
21 theorem exists_prescribed_tower (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L)
22     (F : Fin e → MvPolynomial (Fin (m + k)) ℤ) (x : Fin (m + k) → ℤ)
23     (hx : ∀ i, (q : ℤ)^L ∣ evalSystem F x i)
24     (hJ : Function.Surjective (solvedJacobian q F x))
25     (t : ℕ → Fin k → ℤ) (ht0 : t 0 = freePart x)
26     (ht : ∀ n j, (q : ℤ)^(L+n) ∣ t (n+1) j - t n j) :
27     ∃ z : ℕ → Fin (m + k) → ℤ,
28       z 0 = x ∧
29       (∀ n, freePart (z n) = t n) ∧
30       (∀ n i, (q : ℤ)^(L+n) ∣ evalSystem F (z n) i) ∧
31       (∀ n i, (q : ℤ)^(L+n) ∣ (z (n+1) - z n) i) ∧
32       (∀ n, solvedJacobian q F (z n) = solvedJacobian q F x) := by
33   let State (n : ℕ) :=
34     {y : Fin (m + k) → ℤ //
35       (∀ i, (q : ℤ)^(L+n) ∣ evalSystem F y i) ∧
36       freePart y = t n ∧ solvedJacobian q F y = solvedJacobian q F x}
37   have advance (n : ℕ) (y : State n) :
38       ∃ w : State (n+1), ∀ i, (q : ℤ)^(L+n) ∣ (w.val - y.val) i := by
39     have hyJ : Function.Surjective (solvedJacobian q F y.val) := by
40       rw [y.property.2.2]
41       exact hJ
42     have hparams : ∀ j, (q : ℤ)^(L+n) ∣ t (n+1) j - freePart y.val j := by
43       rw [y.property.2.1]
44       exact ht n
45     obtain ⟨w, hcong, hroot, hfree, hfixed⟩ :=
46       PolynomialPrescribedStep.one_step_lift q (L+n) hq (by omega)
47         F y.val y.property.1 hyJ (t (n+1)) hparams
48     refine ⟨⟨w, ?_, hfree, hfixed.trans y.property.2.2⟩, hcong⟩
49     simpa only [Nat.add_assoc] using hroot
50   let next (n : ℕ) (y : State n) : State (n+1) := Classical.choose (advance n y)
51   let initial : State 0 := ⟨x, by simpa only [Nat.add_zero] using hx, ht0.symm, rfl⟩
52   let state : (n : ℕ) → State n := fun n => Nat.rec initial (fun j y => next j y) n
53   refine ⟨fun n => (state n).val, rfl, ?_, ?_, ?_, ?_⟩
54   · exact fun n => (state n).property.2.1
55   · exact fun n => (state n).property.1
56   · intro n
57     exact Classical.choose_spec (advance n (state n))
58   · exact fun n => (state n).property.2.2
59 
60 /-- The solved block itself is fixed along any compatible positive-depth
61 integer tower; this does not require surjectivity. -/
62 theorem tower_solvedJacobian_eq (q L : ℕ) (hL : 1 ≤ L)
63     (F : Fin e → MvPolynomial (Fin (m + k)) ℤ)
64     (z : ℕ → Fin (m + k) → ℤ)
65     (hstep : ∀ n i, (q : ℤ)^(L+n) ∣ (z (n+1) - z n) i)
66     (n : ℕ) : solvedJacobian q F (z n) = solvedJacobian q F (z 0) := by
67   apply LinearMap.ext
68   intro u
69   have h := congrArg (fun A : (Fin (m + k) → ZMod q) →ₗ[ZMod q] (Fin e → ZMod q) =>
70     A (join u 0)) (tower_digitJacobian_eq q L hL F z hstep n)
71   simpa only [digitJacobian_join, map_zero, add_zero] using h
72 
73 /-- The prescribed tower retains every earlier residue and both the full and
74 solved reduced Jacobians. In particular, solved-block surjectivity persists
75 without an additional hypothesis at later levels. -/
76 theorem exists_prescribed_tower_strong (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L)
77     (F : Fin e → MvPolynomial (Fin (m + k)) ℤ) (x : Fin (m + k) → ℤ)
78     (hx : ∀ i, (q : ℤ)^L ∣ evalSystem F x i)
79     (hJ : Function.Surjective (solvedJacobian q F x))
80     (t : ℕ → Fin k → ℤ) (ht0 : t 0 = freePart x)
81     (ht : ∀ n j, (q : ℤ)^(L+n) ∣ t (n+1) j - t n j) :
82     ∃ z : ℕ → Fin (m + k) → ℤ,
83       z 0 = x ∧
84       (∀ n, freePart (z n) = t n) ∧
85       (∀ n i, (q : ℤ)^(L+n) ∣ evalSystem F (z n) i) ∧
86       (∀ n i, (q : ℤ)^(L+n) ∣ (z (n+1) - z n) i) ∧
87       (∀ a b, a ≤ b → ∀ i, (q : ℤ)^(L+a) ∣ (z b - z a) i) ∧
88       (∀ n, digitJacobian q F (z n) = digitJacobian q F x) ∧
89       (∀ n, solvedJacobian q F (z n) = solvedJacobian q F x) ∧
90       (∀ n, Function.Surjective (solvedJacobian q F (z n))) := by
91   obtain ⟨z, hz0, hfree, hroot, hstep, hfixed⟩ :=
92     exists_prescribed_tower q L hq hL F x hx hJ t ht0 ht
93   refine ⟨z, hz0, hfree, hroot, hstep, ?_, ?_, hfixed, ?_⟩
94   · exact fun a b hab => tower_pairwise_congruent q L z hstep a b hab
95   · intro n
96     rw [← hz0]
97     exact tower_digitJacobian_eq q L hL F z hstep n
98   · intro n
99     rw [hfixed n]
100     exact hJ
101 
102 end Komorebi.PolynomialPrescribedIntegerTower

Back to source controls