AtomicReconstruction.lean

1 import PaperXI.AtomicMultiset
2 
3 /-! Paper XI, Theorem 2.5: choice-independent conditional reconstruction.
4 External interfaces here are exactly (1) existence and intrinsic uniqueness of
5 indecomposable source displays and (2) existence and uniqueness of irreducible
6 Langlands quotients of ordered target factors. They do not contain the final
7 candidate map. Sorting, atomic replacement, descent, and that map are constructed.
8 The theorem is conditional on these classical interfaces; it does not formalize
9 the construction/classification of local Weil groups or p-adic representations. -/
10 set_option autoImplicit false
11 noncomputable section
12 namespace PaperXI.AtomicReconstruction
13 open PaperXI.AtomicMultiset
14 
15 /-- The imported block decomposition, expressed on raw source representatives.
16 `parameterIso` is the declared isomorphism relation, not equality of displays. -/
17 structure Decomposition {P : Type*} (parameterIso : Setoid P) (A : Type*) where
18   displays : P → List (Block A) → Prop
19   exists_display : ∀ p, ∃ xs, displays p xs
20   intrinsic : ∀ p q xs ys, parameterIso.r p q →
21     displays p xs → displays q ys → xs.Perm ys
22 
23 variable {P A B T : Type*} {sP : Setoid P}
24 
25 def rawBlocks (D : Decomposition sP A) (p : P) : Multiset (Block A) :=
26   (Classical.choose (D.exists_display p) : List (Block A))
27 
28 theorem rawBlocks_eq (D : Decomposition sP A) (p : P)
29     (xs : List (Block A)) (hxs : D.displays p xs) : rawBlocks D p = xs := by
30   apply Multiset.coe_eq_coe.mpr
31   exact D.intrinsic p p _ xs (sP.refl p) (Classical.choose_spec (D.exists_display p)) hxs
32 
33 theorem rawBlocks_iso (D : Decomposition sP A) {p q : P} (h : sP.r p q) :
34     rawBlocks D p = rawBlocks D q := by
35   apply Multiset.coe_eq_coe.mpr
36   exact D.intrinsic p q _ _ h (Classical.choose_spec (D.exists_display p))
37     (Classical.choose_spec (D.exists_display q))
38 
39 /-- The intrinsic multiset is derived from the display theorem and descends to
40 actual source isomorphism classes. No decomposition map is supplied as a field. -/
41 def blocks (D : Decomposition sP A) : Quotient sP → Multiset (Block A) :=
42   Quotient.lift (rawBlocks D) (fun _ _ h => rawBlocks_iso D h)
43 
44 theorem blocks_of_display (D : Decomposition sP A) (p : P)
45     (xs : List (Block A)) (hxs : D.displays p xs) :
46     blocks D (Quotient.mk sP p) = xs := rawBlocks_eq D p xs hxs
47 
48 /-- The target classical input. T denotes isomorphism classes of irreducible
49 outputs. `quotient xs t` means t is the irreducible quotient of normalized
50 induction of the generalized Steinberg factors recorded by xs.
51 Only Langlands-ordered displays are used. Ties need not be ordered uniquely. -/
52 structure OrderedQuotient (B T : Type*) where
53   precedes : Block B → Block B → Prop
54   total : ∀ a b, precedes a b ∨ precedes b a
55   transitive : ∀ a b c, precedes a b → precedes b c → precedes a c
56   quotient : List (Block B) → T → Prop
57   exists_quotient : ∀ xs, xs.Pairwise precedes → ∃ t, quotient xs t
58   unique_quotient : ∀ xs ys t u, xs.Pairwise precedes → ys.Pairwise precedes →
59     xs.Perm ys → quotient xs t → quotient ys u → t = u
60 
61 /-- Sort a representative by the declared total preorder. Tied factors are not
62 forced into a fictitious canonical linear order. `realize_eq` removes this choice. -/
63 def ordered (L : OrderedQuotient B T) (s : Multiset (Block B)) : List (Block B) := by
64   classical
65   exact s.toList.mergeSort (fun a b => decide (L.precedes a b))
66 
67 theorem ordered_pairwise (L : OrderedQuotient B T) (s : Multiset (Block B)) :
68     (ordered L s).Pairwise L.precedes := by
69   classical
70   let : Std.Total L.precedes := ⟨L.total⟩
71   let : IsTrans (Block B) L.precedes := ⟨L.transitive⟩
72   exact List.pairwise_mergeSort' L.precedes s.toList
73 
74 theorem ordered_multiset (L : OrderedQuotient B T) (s : Multiset (Block B)) :
75     (ordered L s : Multiset (Block B)) = s := by
76   classical
77   change ((s.toList.mergeSort (fun a b => decide (L.precedes a b))) : Multiset (Block B)) = s
78   calc
79     _ = (s.toList : Multiset (Block B)) :=
80       Multiset.coe_eq_coe.mpr (List.mergeSort_perm _ _)
81     _ = s := Multiset.coe_toList s
82 
83 def realize (L : OrderedQuotient B T) (s : Multiset (Block B)) : T :=
84   Classical.choose (L.exists_quotient (ordered L s) (ordered_pairwise L s))
85 
86 theorem realize_eq (L : OrderedQuotient B T) (s : Multiset (Block B))
87     (ys : List (Block B)) (hs : ys.Pairwise L.precedes)
88     (hy : (ys : Multiset (Block B)) = s) (t : T) (ht : L.quotient ys t) :
89     realize L s = t := by
90   exact L.unique_quotient (ordered L s) ys _ t (ordered_pairwise L s) hs
91     (Multiset.coe_eq_coe.mp ((ordered_multiset L s).trans hy.symm))
92     (Classical.choose_spec (L.exists_quotient (ordered L s) (ordered_pairwise L s))) ht
93 
94 /-- Any valid ordering, including arbitrary choices inside ties, gives the same output. -/
95 theorem realize_spec (L : OrderedQuotient B T) (s : Multiset (Block B))
96     (ys : List (Block B)) (hs : ys.Pairwise L.precedes)
97     (hy : (ys : Multiset (Block B)) = s) : L.quotient ys (realize L s) := by
98   obtain ⟨t, ht⟩ := L.exists_quotient ys hs
99   rw [realize_eq L s ys hs hy t ht]
100   exact ht
101 
102 /-- The candidate is constructed, rather than included among the external inputs. -/
103 def candidate (f : A → B) (D : Decomposition sP A) (L : OrderedQuotient B T) :
104     Quotient sP → T := fun p => realize L (extend f (blocks D p))
105 
106 /-- Operational specification of Theorem 2.5, for all source displays and all
107 valid target orderings of the mapped blocks. -/
108 def Reconstructs (f : A → B) (D : Decomposition sP A) (L : OrderedQuotient B T)
109     (F : Quotient sP → T) : Prop :=
110   ∀ (p : P) (xs : List (Block A)) (ys : List (Block B)), D.displays p xs → ys.Pairwise L.precedes →
111     (ys : Multiset (Block B)) = extend f (xs : Multiset (Block A)) →
112       L.quotient ys (F (Quotient.mk sP p))
113 
114 theorem candidate_spec (f : A → B) (D : Decomposition sP A)
115     (L : OrderedQuotient B T) : Reconstructs f D L (candidate f D L) := by
116   intro p xs ys hd hs hy
117   apply realize_spec L _ ys hs
118   simpa only [blocks_of_display D p xs hd] using hy
119 
120 /-- Evaluation against a supplied decomposition and quotient witness. -/
121 theorem candidate_eq (f : A → B) (D : Decomposition sP A) (L : OrderedQuotient B T)
122     (p : P) (xs : List (Block A)) (ys : List (Block B))
123     (hd : D.displays p xs) (hs : ys.Pairwise L.precedes)
124     (hy : (ys : Multiset (Block B)) = extend f (xs : Multiset (Block A)))
125     (t : T) (ht : L.quotient ys t) : candidate f D L (Quotient.mk sP p) = t := by
126   apply realize_eq L _ ys hs _ t ht
127   simpa only [blocks_of_display D p xs hd] using hy
128 
129 /-- Uniqueness is derived from the pointwise classical quotient theorem. -/
130 theorem candidate_unique (f : A → B) (D : Decomposition sP A) (L : OrderedQuotient B T)
131     (F : Quotient sP → T) (hF : Reconstructs f D L F) : F = candidate f D L := by
132   funext p
133   refine Quotient.inductionOn p ?_
134   intro p
135   obtain ⟨xs, hd⟩ := D.exists_display p
136   let s := extend f (xs : Multiset (Block A))
137   exact (candidate_eq f D L p xs (ordered L s) hd (ordered_pairwise L s)
138     (ordered_multiset L s) _ (hF p xs _ hd (ordered_pairwise L s)
139       (ordered_multiset L s))).symm
140 
141 /-- Source-facing formal atomic reconstruction. It constructs a unique candidate,
142 not a bijection, and does not prove local-factor identities. -/
143 theorem formal_atomic_reconstruction (f : A → B) (D : Decomposition sP A)
144     (L : OrderedQuotient B T) : ∃! F : Quotient sP → T, Reconstructs f D L F := by
145   exact ⟨candidate f D L, candidate_spec f D L, fun F hF => candidate_unique f D L F hF⟩
146 
147 /-- Changing the raw parameter representative cannot change the output class. -/
148 theorem candidate_isomorphism (f : A → B) (D : Decomposition sP A)
149     (L : OrderedQuotient B T) {p q : P} (h : sP.r p q) :
150     candidate f D L (Quotient.mk sP p) = candidate f D L (Quotient.mk sP q) := by
151   exact congrArg (candidate f D L) (Quotient.sound h)
152 
153 end PaperXI.AtomicReconstruction

Back to source controls