Reachability.lean

1 import Mathlib.Algebra.Group.Subgroup.Basic
2 import Mathlib.Algebra.BigOperators.Group.Finset.Basic
3 import Mathlib.Data.Set.Countable
4 import Mathlib.Data.Set.Finite.Basic
5 import Mathlib.SetTheory.Cardinal.Basic
6 import Mathlib.Topology.Algebra.Group.ClosedSubgroup
7 
8 /-!
9 # Finite descriptions and graph reachability
10 
11 The finite-code result permits arbitrary single-valued semantics. The graph
12 result uses the actual dependent direct sum of abelian packets, transfer blocks
13 of primitive endomorphisms, and finite operator words.
14 -/
15 set_option autoImplicit false
16 noncomputable section
17 open scoped BigOperators
18 
19 namespace RealizationBoundaries
20 universe u v w
21 
22 /-- A grammar has finite strings, an arbitrary validity predicate, and a single
23 semantic value per valid string. No computability hypothesis is imposed. -/
24 structure FiniteDescriptionGrammar (Alphabet : Type u) (Target : Type v) where
25   valid : Set (List Alphabet)
26   realize : valid → Target
27 
28 def FiniteDescriptionGrammar.outputs {Alphabet : Type u} {Target : Type v}
29     (g : FiniteDescriptionGrammar Alphabet Target) : Set Target := Set.range g.realize
30 
31 /-- Monograph 1.5: single-valued finite-string semantics has countable image. -/
32 theorem finite_description_outputs_countable {Alphabet : Type u} {Target : Type v}
33     [Countable Alphabet] (g : FiniteDescriptionGrammar Alphabet Target) :
34     g.outputs.Countable := Set.countable_range g.realize
35 
36 /-- The same theorem as a cardinal bound on the actual realized-value subtype. -/
37 theorem finite_description_cardinal_bound {Alphabet : Type u} {Target : Type v}
38     [Countable Alphabet] (g : FiniteDescriptionGrammar Alphabet Target) :
39     Cardinal.mk g.outputs ≤ Cardinal.aleph0 := by
40   exact Cardinal.le_aleph0_iff_set_countable.mpr (finite_description_outputs_countable g)
41 
42 section Packets
43 variable {I : Type u} (M : I → Type v) [∀ i, AddCommGroup (M i)]
44 
45 /-- The genuine dependent direct sum, represented by finite-support vectors. -/
46 def packetSum : AddSubgroup (∀ i, M i) where
47   carrier := {x | {i | x i ≠ 0}.Finite}
48   zero_mem' := by simp
49   add_mem' := by
50     intro x y hx hy
51     apply (hx.union hy).subset
52     intro i hi
53     by_contra hn
54     have hxy : x i = 0 ∧ y i = 0 := by simpa using hn
55     exact hi (by simp [hxy.1, hxy.2])
56   neg_mem' := by intro x hx; simpa using hx
57 
58 def packetSupport (x : packetSum M) : Set I := {i | x.val i ≠ 0}
59 
60 def packetProjection (i : I) : packetSum M →+ M i where
61   toFun x := x.val i
62   map_zero' := rfl
63   map_add' _ _ := rfl
64 
65 /-- The actual packet injection, interpreted as a finite-support vector. -/
66 def packetSingle (i : I) (a : M i) : packetSum M := by
67   classical
68   refine ⟨Pi.single i a, (Set.finite_singleton i).subset ?_⟩
69   intro j hj
70   by_contra h
71   have hji : j ≠ i := by simpa only [Set.mem_singleton_iff] using h
72   exact hj (Pi.single_eq_of_ne hji a)
73 
74 @[simp] theorem packetSingle_same (i : I) (a : M i) :
75     (packetSingle M i a).val i = a := by
76   classical
77   simp [packetSingle]
78 
79 @[simp] theorem packetSingle_other (i j : I) (a : M i) (h : j ≠ i) :
80     (packetSingle M i a).val j = 0 := by
81   classical
82   exact Pi.single_eq_of_ne h a
83 
84 /-- Finite decomposition is derived from finite support, rather than assumed as
85 an extra transfer hypothesis. -/
86 theorem packet_decomposition (x : packetSum M) :
87     x = ∑ i ∈ x.property.toFinset, packetSingle M i (x.val i) := by
88   classical
89   apply Subtype.ext
90   funext j
91   change packetProjection M j x =
92     packetProjection M j (∑ i ∈ x.property.toFinset, packetSingle M i (x.val i))
93   rw [map_sum]
94   by_cases hj : j ∈ x.property.toFinset
95   · rw [Finset.sum_eq_single j]
96     · exact (packetSingle_same M j (x.val j)).symm
97     · intro i _ hij
98       exact packetSingle_other M i j (x.val i) (Ne.symm hij)
99     · exact fun hn => False.elim (hn hj)
100   · have hxj : x.val j = 0 := by
101       by_contra hn
102       exact hj ((Set.Finite.mem_toFinset x.property).mpr hn)
103     change x.val j = _
104     rw [hxj]
105     symm
106     apply Finset.sum_eq_zero
107     intro i hi
108     exact packetSingle_other M i j (x.val i) (by intro h; exact hj (h ▸ hi))
109 
110 /-- A finite directed path from the initial set. The reflexive constructor
111 includes the empty operator word. -/
112 inductive GraphReach (E : I → I → Prop) (F : Set I) : I → Prop
113   | start {i : I} : i ∈ F → GraphReach E F i
114   | step {i j : I} : GraphReach E F i → E i j → GraphReach E F j
115 
116 /-- The inductive reachability predicate is exactly finite-path reachability
117 in the usual reflexive transitive closure of the directed graph. -/
118 theorem graphReach_iff_finite_path (E : I → I → Prop) (F : Set I) (j : I) :
119     GraphReach E F j ↔ ∃ i ∈ F, Relation.ReflTransGen E i j := by
120   constructor
121   · intro h
122     induction h with
123     | start hi => exact ⟨_, hi, Relation.ReflTransGen.refl⟩
124     | step _ hij ih =>
125       obtain ⟨i, hi, hpath⟩ := ih
126       exact ⟨i, hi, hpath.tail hij⟩
127   · rintro ⟨i, hi, hpath⟩
128     induction hpath with
129     | refl => exact GraphReach.start hi
130     | tail _ hij ih => exact GraphReach.step ih hij
131 
132 /-- Vectors supported on a prescribed packet set form an actual subgroup. -/
133 def supportedPackets (R : Set I) : AddSubgroup (packetSum M) where
134   carrier := {x | ∀ i, i ∉ R → x.val i = 0}
135   zero_mem' := by intro i _; rfl
136   add_mem' := by intro x y hx hy i hi; change x.val i + y.val i = 0; rw [hx i hi, hy i hi, add_zero]
137   neg_mem' := by intro x hx i hi; change -x.val i = 0; rw [hx i hi, neg_zero]
138 
139 /-- The transfer block from packet `i` to packet `j`, applied to one vector. -/
140 def packetTransfer (T : AddMonoid.End (packetSum M)) (i j : I) (a : M i) : M j :=
141   (T (packetSingle M i a)).val j
142 
143 /-- Vanishing transfer blocks give the one-step support implication. -/
144 theorem packet_operator_support (E : I → I → Prop) (R : Set I)
145     (hR : ∀ i j, i ∈ R → E i j → j ∈ R)
146     (T : AddMonoid.End (packetSum M))
147     (hT : ∀ i j, ¬ E i j → ∀ a : M i, packetTransfer M T i j a = 0)
148     (x : packetSum M) (hx : x ∈ supportedPackets M R) :
149     T x ∈ supportedPackets M R := by
150   classical
151   intro j hj
152   have he := congrArg (fun y : packetSum M => (T y).val j) (packet_decomposition M x)
153   change (T x).val j = 0
154   rw [he]
155   change packetProjection M j (T (∑ i ∈ x.property.toFinset, packetSingle M i (x.val i))) = 0
156   rw [map_sum, map_sum]
157   apply Finset.sum_eq_zero
158   intro i hi
159   have hxi : x.val i ≠ 0 := (Set.Finite.mem_toFinset x.property).mp hi
160   have hiR : i ∈ R := by by_contra hn; exact hxi (hx i hn)
161   exact hT i j (fun hij => hj (hR i j hiR hij)) (x.val i)
162 
163 end Packets
164 
165 section OperatorWords
166 variable {G : Type w} [AddCommGroup G]
167 
168 /-- Only the declared primitive operators may appear in a word. -/
169 def operatorWord (O : Set (AddMonoid.End G)) : List O → AddMonoid.End G
170   | [] => AddMonoidHom.id G
171   | f :: word => f.val.comp (operatorWord O word)
172 
173 def primitiveOperatorOrbit (O : Set (AddMonoid.End G)) (S : Set G) : Set G :=
174   {x | ∃ word : List O, ∃ s ∈ S, operatorWord O word s = x}
175 
176 def primitiveOperatorHull (O : Set (AddMonoid.End G)) (S : Set G) : AddSubgroup G :=
177   AddSubgroup.closure (primitiveOperatorOrbit O S)
178 
179 /-- An invariant subgroup containing the seeds contains every finite word and
180 then its algebraic operator hull. -/
181 theorem primitiveOperatorHull_le (O : Set (AddMonoid.End G)) (S : Set G)
182     (H : AddSubgroup G) (hS : S ⊆ H)
183     (hH : ∀ T ∈ O, ∀ x ∈ H, T x ∈ H) : primitiveOperatorHull O S ≤ H := by
184   apply (AddSubgroup.closure_le _).mpr
185   rintro x ⟨word, s, hs, rfl⟩
186   induction word with
187   | nil => exact hS hs
188   | cons T word ih => exact hH T.val T.property _ ih
189 
190 end OperatorWords
191 
192 section Reachability
193 variable {I : Type u} (M : I → Type v) [∀ i, AddCommGroup (M i)]
194 
195 /-- The initial packet set is exactly the union of the supports of the seeds. -/
196 def seedPackets (S : Set (packetSum M)) : Set I := ⋃ s ∈ S, packetSupport M s
197 
198 /-- Monograph 1.8, for the actual direct sum, actual primitive transfer blocks,
199 and the hull of all finite primitive-operator words. -/
200 theorem operator_hull_reachable (E : I → I → Prop)
201     (O : Set (AddMonoid.End (packetSum M))) (S : Set (packetSum M))
202     (hO : ∀ T ∈ O, ∀ i j, ¬ E i j → ∀ a : M i, packetTransfer M T i j a = 0) :
203     primitiveOperatorHull O S ≤ supportedPackets M {j | GraphReach E (seedPackets M S) j} := by
204   apply primitiveOperatorHull_le
205   · intro s hs j hj
206     by_contra hn
207     exact hj (GraphReach.start (Set.mem_iUnion.mpr ⟨s, Set.mem_iUnion.mpr ⟨hs, hn⟩⟩))
208   · intro T hT x hx
209     exact packet_operator_support M E _ (fun _ _ hi hij => GraphReach.step hi hij)
210       T (hO T hT) x hx
211 
212 /-- An omitted nonzero packet is an explicit certificate of non-generation. -/
213 theorem unreachable_packet_obstructs (E : I → I → Prop)
214     (O : Set (AddMonoid.End (packetSum M))) (S : Set (packetSum M))
215     (hO : ∀ T ∈ O, ∀ i j, ¬ E i j → ∀ a : M i, packetTransfer M T i j a = 0)
216     (j : I) (hj : ¬ GraphReach E (seedPackets M S) j) [Nontrivial (M j)] :
217     (∀ x ∈ primitiveOperatorHull O S, x.val j = 0) ∧ primitiveOperatorHull O S ≠ ⊤ := by
218   have hz : ∀ x ∈ primitiveOperatorHull O S, x.val j = 0 :=
219     fun x hx => operator_hull_reachable M E O S hO hx j hj
220   refine ⟨hz, ?_⟩
221   intro heq
222   obtain ⟨a, ha⟩ := exists_ne (0 : M j)
223   have hsingle := hz (packetSingle M j a) (heq ▸ AddSubgroup.mem_top _)
224   exact ha ((packetSingle_same M j a).symm.trans hsingle)
225 
226 /-- If the omitted coordinate projection is continuous into a Hausdorff
227 packet, its closed kernel also contains the topological operator hull. -/
228 theorem unreachable_packet_obstructs_topological (E : I → I → Prop)
229     (O : Set (AddMonoid.End (packetSum M))) (S : Set (packetSum M))
230     (hO : ∀ T ∈ O, ∀ i j, ¬ E i j → ∀ a : M i, packetTransfer M T i j a = 0)
231     (j : I) (hj : ¬ GraphReach E (seedPackets M S) j)
232     [Nontrivial (M j)] [TopologicalSpace (packetSum M)]
233     [IsTopologicalAddGroup (packetSum M)] [TopologicalSpace (M j)] [T2Space (M j)]
234     (hcontinuous : Continuous (packetProjection M j)) :
235     (∀ x ∈ (primitiveOperatorHull O S).topologicalClosure, x.val j = 0) ∧
236       (primitiveOperatorHull O S).topologicalClosure ≠ ⊤ := by
237   have hle : primitiveOperatorHull O S ≤ (packetProjection M j).ker := by
238     intro x hx
239     exact (unreachable_packet_obstructs M E O S hO j hj).1 x hx
240   have hclosed : IsClosed ((packetProjection M j).ker : Set (packetSum M)) :=
241     isClosed_eq hcontinuous continuous_const
242   have hclosure : (primitiveOperatorHull O S).topologicalClosure ≤
243       (packetProjection M j).ker := closure_minimal hle hclosed
244   have hz : ∀ x ∈ (primitiveOperatorHull O S).topologicalClosure, x.val j = 0 := hclosure
245   refine ⟨hz, ?_⟩
246   intro heq
247   obtain ⟨a, ha⟩ := exists_ne (0 : M j)
248   have hsingle := hz (packetSingle M j a) (heq ▸ AddSubgroup.mem_top _)
249   exact ha ((packetSingle_same M j a).symm.trans hsingle)
250 
251 end Reachability
252 end RealizationBoundaries

Back to source controls