ReleasePrecision.lean

1 import KomorebiVerification.PaperII.ResultantSeparation
2 
3 /-!
4 # Necessary and sufficient uniform precision delay
5 
6 The input and output congruences are the actual scalar-lattice congruences
7 already defined in ResultantSeparation.  The witnesses below belong to the
8 specified lattice.  Nonvanishing of the uniformizer is used only to cancel
9 its output-depth power, and lattice stability is needed to keep the input
10 witnesses inside the lattice.
11 -/
12 
13 set_option autoImplicit false
14 
15 namespace Komorebi.PaperII.ResultantSeparation
16 
17 universe u v
18 variable {K : Type u} {M : Type v}
19 variable [Field K] [AddCommGroup M] [Module K M]
20 
21 theorem exists_uncleared_vector_of_lt_separationWeight
22     {pi : K} {E : End (K := K) (M := M)} {lattice : AddSubgroup M}
23     (finite : HasFiniteSeparationWeight pi E lattice) {d : ℕ}
24     (hd : d < separationWeight finite) :
25     ∃ z : M, z ∈ lattice ∧ (pi ^ d) • E z ∉ lattice := by
26   classical
27   by_contra! h
28   have hclear : IsSeparationWeight pi E lattice d := by
29     intro z hz
30     exact h z hz
31   exact (Nat.not_le_of_lt hd) (separationWeight_le_of_clears finite hclear)
32 
33 /-- Every smaller delay fails at every output depth, with both inputs in the lattice. -/
34 theorem projector_precision_delay_necessary
35     {pi : K} {E : End (K := K) (M := M)} {lattice : AddSubgroup M}
36     (finite : HasFiniteSeparationWeight pi E lattice)
37     (hpi : pi ≠ 0) (hstable : ScalarPreservesLattice pi lattice)
38     {d : ℕ} (hd : d < separationWeight finite) (m : ℕ) :
39     ∃ x y : M, x ∈ lattice ∧ y ∈ lattice ∧
40       CongruentModLattice pi lattice (m + d) x y ∧
41       ¬ CongruentModLattice pi lattice m (E x) (E y) := by
42   obtain ⟨z, hz, hbad⟩ := exists_uncleared_vector_of_lt_separationWeight finite hd
43   refine ⟨(pi ^ (m + d)) • z, 0, hstable.pow (m + d) z hz,
44     lattice.zero_mem, ⟨z, hz, by simp⟩, ?_⟩
45   rintro ⟨w, hw, heq⟩
46   have heq' : (pi ^ m) • ((pi ^ d) • E z) = (pi ^ m) • w := by
47     simpa only [map_zero, sub_zero, map_smul, pow_add, mul_smul] using heq
48   have hw' : (pi ^ d) • E z = w :=
49     (smul_right_injective M (pow_ne_zero m hpi)) heq'
50   exact hbad (hw' ▸ hw)
51 
52 /-- A uniform delay, with the domain restricted to the chosen lattice. -/
53 def UniformPrecisionDelay (pi : K) (E : End (K := K) (M := M))
54     (lattice : AddSubgroup M) (d : ℕ) : Prop :=
55   ∀ (m : ℕ) (x y : M), x ∈ lattice → y ∈ lattice →
56     CongruentModLattice pi lattice (m + d) x y →
57     CongruentModLattice pi lattice m (E x) (E y)
58 
59 /-- The least clearing exponent is exactly the least uniform precision delay. -/
60 theorem uniformPrecisionDelay_iff_separationWeight_le
61     {pi : K} {E : End (K := K) (M := M)} {lattice : AddSubgroup M}
62     (finite : HasFiniteSeparationWeight pi E lattice)
63     (hpi : pi ≠ 0) (hstable : ScalarPreservesLattice pi lattice) (d : ℕ) :
64     UniformPrecisionDelay pi E lattice d ↔ separationWeight finite ≤ d := by
65   constructor
66   · intro h
67     by_contra! hd
68     obtain ⟨x, y, hx, hy, hxy, hbad⟩ :=
69       projector_precision_delay_necessary finite hpi hstable hd 0
70     exact hbad (h 0 x y hx hy hxy)
71   · intro hd m x y _hx _hy hxy
72     exact projector_precision_delay
73       ((separationWeight_clears finite).mono hd hstable) hxy
74 
75 end Komorebi.PaperII.ResultantSeparation

Back to source controls