TraceRecovery.lean

1 import PaperX.DenseTraceSeparation
2 
3 /-! Exact trace recovery and scalar-field descent. The finite matrix comes from
4 actual trace values. Nonnegative capacity constraints are separate from solving
5 the linear equations. No compatible arithmetic system is constructed here. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperX.TraceRecovery
9 
10 open scoped BigOperators Matrix
11 open PaperX.FiniteSeparation PaperX.DenseTraceSeparation
12 universe u v w z
13 variable {E : Type u} [Field E] {I : Type v} [Fintype I] [DecidableEq I]
14 
15 /-- Exact recovery by the inverse of a certified square separator. -/
16 def recover (C : Matrix I I E) (t : I → E) : I → E := C⁻¹ *ᵥ t
17 
18 theorem recover_trace (C : Matrix I I E) (h : C.det ≠ 0) (m : I → E) :
19     recover C (C *ᵥ m) = m := by
20   rw [recover, Matrix.mulVec_mulVec, C.nonsing_inv_mul (isUnit_iff_ne_zero.mpr h),
21     Matrix.one_mulVec]
22 
23 theorem recover_solves (C : Matrix I I E) (h : C.det ≠ 0) (t : I → E) :
24     C *ᵥ recover C t = t := by
25   rw [recover, Matrix.mulVec_mulVec, C.mul_nonsing_inv (isUnit_iff_ne_zero.mpr h),
26     Matrix.one_mulVec]
27 
28 theorem unique_recovery (C : Matrix I I E) (h : C.det ≠ 0) (m n : I → E)
29     (ht : C *ᵥ m = C *ᵥ n) : m = n := by
30   simpa [recover_trace C h] using congrArg (recover C) ht
31 
32 /-- Multiplicities are natural numbers, with upper bounds from a given carrier. -/
33 def Admissible (capacity m : I → ℕ) : Prop := ∀ i, m i ≤ capacity i
34 
35 theorem natural_multiplicity_unique [CharZero E] (C : Matrix I I E) (h : C.det ≠ 0)
36     (m n : I → ℕ)
37     (ht : C *ᵥ (fun i => (m i : E)) = C *ᵥ (fun i => (n i : E))) : m = n := by
38   have hh := unique_recovery C h _ _ ht
39   funext i
40   exact Nat.cast_injective (congrFun hh i)
41 
42 /-- Linear solvability does not enforce integrality, positivity, or capacities.
43 This equivalence keeps the carrier membership test explicit. -/
44 theorem admissible_trace_iff [CharZero E] (C : Matrix I I E) (h : C.det ≠ 0)
45     (capacity : I → ℕ) (t : I → E) :
46     (∃ m : I → ℕ, Admissible capacity m ∧ C *ᵥ (fun i => (m i : E)) = t) ↔
47     ∃ m : I → ℕ, Admissible capacity m ∧ recover C t = (fun i => (m i : E)) := by
48   constructor
49   · rintro ⟨m, hm, rfl⟩
50     exact ⟨m, hm, recover_trace C h _⟩
51   · rintro ⟨m, hm, ht⟩
52     exact ⟨m, hm, by rw [← ht, recover_solves C h]⟩
53 
54 /-- A field embedding preserves and reflects the separator determinant. -/
55 theorem determinant_transport {K : Type w} [Field K] (σ : E →+* K)
56     (C : Matrix I I E) : (σ.mapMatrix C).det ≠ 0 ↔ C.det ≠ 0 := by
57   rw [← σ.map_det C]
58   exact not_congr (by constructor
59                       · intro h; exact σ.injective (by simpa using h)
60                       · intro h; simp [h])
61 
62 theorem mapped_trace {K : Type w} [Field K] (σ : E →+* K)
63     (C : Matrix I I E) (m : I → E) :
64     (σ.mapMatrix C) *ᵥ (fun i => σ (m i)) = fun j => σ ((C *ᵥ m) j) := by
65   funext j
66   simp [Matrix.mulVec, dotProduct]
67 
68 theorem recovery_transport {K : Type w} [Field K] (σ : E →+* K)
69     (C : Matrix I I E) (h : C.det ≠ 0) (t : I → E) :
70     recover (σ.mapMatrix C) (fun j => σ (t j)) = fun i => σ (recover C t i) := by
71   apply unique_recovery (σ.mapMatrix C) ((determinant_transport σ C).2 h)
72   rw [recover_solves _ ((determinant_transport σ C).2 h), mapped_trace,
73     recover_solves C h]
74 
75 /-- The common algebraic trace matrix is certified over E using one coefficient
76 field, then stays invertible at every field embedding. No unramifiedness is inferred
77 for the places excluded by the arithmetic compatibility convention. -/
78 theorem common_trace_separator {K : Type w} [Field K] [TopologicalSpace K]
79     [IsTopologicalRing K] [T2Space K]
80     {G : Type z} [Group G] [TopologicalSpace G] {X : Type*}
81     (σ : E →+* K) (τ : I → X → E) (f : I → G → K)
82     (hc : ∀ i, Continuous (f i)) (hi : LinearIndependent K f) (s : X → G)
83     (hd : DenseRange (fun p : X × G => p.2 * s p.1 * p.2⁻¹))
84     (hconj : ∀ i g x, f i (g * s x * g⁻¹) = f i (s x))
85     (hτ : ∀ i x, σ (τ i x) = f i (s x)) :
86     ∃ v : I → X, Function.Injective v ∧ (sampleMatrix τ v).det ≠ 0 := by
87   obtain ⟨v, hv, hdet⟩ := finite_conjugacy_separator f hc hi s hd hconj
88   refine ⟨v, hv, (determinant_transport σ _).1 ?_⟩
89   have hmat : σ.mapMatrix (sampleMatrix τ v) =
90       sampleMatrix (fun i x => f i (s x)) v := by
91     ext j i
92     exact hτ i (v j)
93   rw [hmat]
94   exact hdet
95 
96 end PaperX.TraceRecovery

Back to source controls