TopologicalCompletion.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 
6 import KomorebiVerification.MathlibImports
7 
8 /-!
9 # Paper I: topological completion and Hilbert-space packets
10 
11 This module formalizes the analytic branch of *Projector-Resolved Seed
12 Calculus I*.  It covers finite bounded packet decompositions, passage of a
13 packet split to a completion, adjoint reversal, closed-hull obstructions,
14 dense realizations, completion of a dense isometric presentation, and the
15 dense orbit certificate used by the bilateral-shift example.
16 -/
17 
18 noncomputable section
19 
20 open scoped BigOperators InnerProduct lp
21 open Set Function UniformSpace
22 
23 namespace KomorebiVerification.TopologicalCompletion
24 
25 /-! ## Finite bounded packet systems -/
26 
27 /-- A finite family of bounded projectors which is pairwise annihilating and
28 sums pointwise to the identity. -/
29 structure BoundedProjectorFamily
30     (𝕜 : Type*) (X : Type*) (ι : Type*)
31     [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X]
32     [Fintype ι] where
33   proj : ι → X →L[𝕜] X
34   idempotent : ∀ i x, proj i (proj i x) = proj i x
35   annihilate : ∀ {i j}, i ≠ j → ∀ x, proj i (proj j x) = 0
36   complete : ∀ x, (∑ i, proj i x) = x
37 
38 namespace BoundedProjectorFamily
39 
40 variable {𝕜 X ι : Type*}
41 variable [NontriviallyNormedField 𝕜]
42 variable [NormedAddCommGroup X] [NormedSpace 𝕜 X]
43 variable [Fintype ι]
44 
45 /-- The `i`th packet is the range of its bounded projector. -/
46 def packet (P : BoundedProjectorFamily 𝕜 X ι) (i : ι) : Submodule 𝕜 X :=
47   (P.proj i).range
48 
49 /-- Every packet range is closed. -/
50 theorem isClosed_packet (P : BoundedProjectorFamily 𝕜 X ι) (i : ι) :
51     IsClosed (P.packet i : Set X) := by
52   apply ContinuousLinearMap.IsIdempotentElem.isClosed_range
53   apply ContinuousLinearMap.ext
54   intro x
55   exact P.idempotent i x
56 
57 /-- Analysis into the finite product of packet ranges. -/
58 def analysis (P : BoundedProjectorFamily 𝕜 X ι) :
59     X →L[𝕜] ∀ i, P.packet i :=
60   ContinuousLinearMap.pi fun i ↦
61     (P.proj i).codRestrict (P.packet i) fun x ↦ by
62       change P.proj i x ∈ (P.proj i).range
63       exact ⟨x, rfl⟩
64 
65 @[simp]
66 theorem analysis_apply_coe (P : BoundedProjectorFamily 𝕜 X ι) (x : X) (i : ι) :
67     ((P.analysis x i : P.packet i) : X) = P.proj i x :=
68   by simp [analysis]
69 
70 /-- Synthesis is the finite sum of the packet inclusions. -/
71 def synthesis (P : BoundedProjectorFamily 𝕜 X ι) :
72     (∀ i, P.packet i) →L[𝕜] X :=
73   ∑ i, (P.packet i).subtypeL.comp (ContinuousLinearMap.proj i)
74 
75 @[simp]
76 theorem synthesis_apply (P : BoundedProjectorFamily 𝕜 X ι)
77     (x : ∀ i, P.packet i) :
78     P.synthesis x = ∑ i, (x i : X) := by
79   simp [synthesis]
80 
81 @[simp]
82 theorem synthesis_analysis (P : BoundedProjectorFamily 𝕜 X ι) (x : X) :
83     P.synthesis (P.analysis x) = x := by
84   simpa [synthesis] using P.complete x
85 
86 @[simp]
87 theorem analysis_synthesis (P : BoundedProjectorFamily 𝕜 X ι)
88     (x : ∀ i, P.packet i) :
89     P.analysis (P.synthesis x) = x := by
90   classical
91   ext i
92   rw [analysis_apply_coe, synthesis_apply]
93   change P.proj i (∑ j, (x j : X)) = (x i : X)
94   rw [map_sum, Finset.sum_eq_single i]
95   · rcases (x i).property with ⟨y, hy⟩
96     rw [← hy]
97     exact P.idempotent i y
98   · intro j _ hji
99     rcases (x j).property with ⟨y, hy⟩
100     rw [← hy]
101     exact P.annihilate hji.symm y
102   · simp
103 
104 /-- The topological packet isomorphism: bounded analysis and synthesis are
105 mutually inverse.  A finite product is the finite direct sum as a vector
106 space, and carries one of its equivalent finite-product norms. -/
107 def packetEquiv (P : BoundedProjectorFamily 𝕜 X ι) :
108     X ≃L[𝕜] ∀ i, P.packet i :=
109   ContinuousLinearEquiv.equivOfInverse P.analysis P.synthesis
110     P.synthesis_analysis P.analysis_synthesis
111 
112 @[simp]
113 theorem packetEquiv_apply (P : BoundedProjectorFamily 𝕜 X ι) (x : X) :
114     P.packetEquiv x = P.analysis x :=
115   rfl
116 
117 /-- Literal Banach-space wrapper for the topological packet theorem.  It
118 packages both manuscript conclusions: every packet is closed and analysis is
119 a bounded linear isomorphism whose forward and inverse maps are the declared
120 analysis and synthesis operators. -/
121 theorem topological_packet_isomorphism [CompleteSpace X]
122     (P : BoundedProjectorFamily 𝕜 X ι) :
123     (∀ i, IsClosed (P.packet i : Set X)) ∧
124       ∃ e : X ≃L[𝕜] ∀ i, P.packet i,
125         e.toContinuousLinearMap = P.analysis ∧
126           e.symm.toContinuousLinearMap = P.synthesis := by
127   refine ⟨P.isClosed_packet, P.packetEquiv, rfl, ?_⟩
128   rfl
129 
130 /-! ## Completion preserves finite packet extraction -/
131 
132 /-- The image of a dense submodule under an arbitrary bounded idempotent is
133 dense in the full range.  This is the literal manuscript completion lemma;
134 it does not require the projector to belong to a finite packet family. -/
135 theorem idempotentRange_eq_closure_map
136     (Q : X →L[𝕜] X) (hQ : ∀ x, Q (Q x) = Q x)
137     (M : Submodule 𝕜 X) (hM : M.topologicalClosure = ⊤) :
138     (M.map Q.toLinearMap).topologicalClosure = Q.range := by
139   have hclosed : IsClosed (Q.range : Set X) := by
140     apply ContinuousLinearMap.IsIdempotentElem.isClosed_range
141     apply ContinuousLinearMap.ext
142     intro x
143     exact hQ x
144   apply le_antisymm
145   · apply Submodule.topologicalClosure_minimal
146     · exact LinearMap.map_le_range
147     · exact hclosed
148   · have h := Submodule.topologicalClosure_map Q M
149     rw [hM] at h
150     simpa using h
151 
152 /-- For a dense submodule `M`, the image of `M` under any bounded idempotent
153 projector is dense in the full packet range.  This is the exact completion
154 claim `P_i X = closure (P_i M)`, stated as equality of submodules.  The result
155 is slightly stronger than the manuscript statement because invariance
156 `P_i M ⊆ M` is not needed for this equality. -/
157 theorem packetRange_eq_closure_map
158     (P : BoundedProjectorFamily 𝕜 X ι) (M : Submodule 𝕜 X)
159     (hM : M.topologicalClosure = ⊤) (i : ι) :
160     (M.map (P.proj i).toLinearMap).topologicalClosure = P.packet i := by
161   simpa [packet] using
162     idempotentRange_eq_closure_map (P.proj i) (P.idempotent i) M hM
163 
164 /-! ## Adjoint reversal -/
165 
166 /-- A packet-to-packet transfer block. -/
167 def transferBlock (Pβ T Pα : X →L[𝕜] X) : X →L[𝕜] X :=
168   Pβ.comp (T.comp Pα)
169 
170 /-- Adjoint reverses the input and output packets:
171 `(Pβ T Pα)† = Pα T† Pβ` for self-adjoint packet projections. -/
172 theorem adjoint_transferBlock
173     {𝕂 E : Type*} [RCLike 𝕂]
174     [NormedAddCommGroup E] [InnerProductSpace 𝕂 E] [CompleteSpace E]
175     (Pα Pβ T : E →L[𝕂] E) (hα : Pα† = Pα) (hβ : Pβ† = Pβ) :
176     (transferBlock Pβ T Pα)† = transferBlock Pα (T†) Pβ := by
177   ext x
178   simp [transferBlock, hα, hβ]
179 
180 /-! ## Closure and reachability obstructions -/
181 
182 /-- If a continuous packet projector annihilates an algebraic generated
183 hull, then it also annihilates its closed topological hull. -/
184 theorem closure_le_ker_of_le_ker
185     (Q : X →L[𝕜] X) (H : Submodule 𝕜 X) (hH : H ≤ Q.ker) :
186     H.topologicalClosure ≤ Q.ker :=
187   Submodule.topologicalClosure_minimal H hH (ContinuousLinearMap.isClosed_ker Q)
188 
189 /-- A nonzero unreachable packet prevents topological generation. -/
190 theorem topological_reachability_obstruction
191     (Q : X →L[𝕜] X) (H : Submodule 𝕜 X)
192     (hQ : Q ≠ 0) (hH : H ≤ Q.ker) :
193     H.topologicalClosure ≠ ⊤ := by
194   intro htop
195   apply hQ
196   apply ContinuousLinearMap.ext
197   intro x
198   have hx : x ∈ H.topologicalClosure := by rw [htop]; trivial
199   exact (closure_le_ker_of_le_ker Q H hH hx : Q x = 0)
200 
201 /-! ## Dense realizations -/
202 
203 variable {Y : Type*}
204 variable [NormedAddCommGroup Y] [NormedSpace 𝕜 Y]
205 
206 /-- The algebraic hull of `S` under a declared family of bounded operators.
207 The manuscript assumes that the family is the carrier of a unital operator
208 algebra; the definition itself only needs its underlying set. -/
209 def operatorHull (A : Set (X →L[𝕜] X)) (S : Set X) : Submodule 𝕜 X :=
210   Submodule.span 𝕜 {x | ∃ T ∈ A, ∃ s ∈ S, T s = x}
211 
212 /-- Intertwining maps carry the source operator hull into the target operator
213 hull.  Algebra-homomorphism laws are not needed for this inclusion. -/
214 theorem map_operatorHull_le
215     (f : X →L[𝕜] Y) (φ : (X →L[𝕜] X) → (Y →L[𝕜] Y))
216     (A : Set (X →L[𝕜] X)) (B : Set (Y →L[𝕜] Y))
217     (S : Set X) (hφ : ∀ T ∈ A, φ T ∈ B)
218     (hintertwine : ∀ T ∈ A, f.comp T = (φ T).comp f) :
219     (operatorHull A S).map f.toLinearMap ≤ operatorHull B (f '' S) := by
220   rw [Submodule.map_le_iff_le_comap]
221   apply Submodule.span_le.2
222   rintro x ⟨T, hTA, s, hs, rfl⟩
223   change f (T s) ∈ operatorHull B (f '' S)
224   have hpoint : f (T s) = φ T (f s) := by
225     simpa using congrArg (fun L : X →L[𝕜] Y ↦ L s) (hintertwine T hTA)
226   rw [hpoint]
227   apply Submodule.subset_span
228   exact ⟨φ T, hφ T hTA, f s, ⟨s, hs, rfl⟩, rfl⟩
229 
230 /-- A continuous surjective realization carries a dense algebraic hull to a
231 dense image hull.  The target `K` can be the hull under the image algebra or
232 under any larger target algebra. -/
233 theorem dense_realization
234     (f : X →L[𝕜] Y) (hf : Surjective f)
235     (H : Submodule 𝕜 X) (K : Submodule 𝕜 Y)
236     (hH : H.topologicalClosure = ⊤)
237     (htransport : H.map f.toLinearMap ≤ K) :
238     K.topologicalClosure = ⊤ := by
239   have himage : (H.map f.toLinearMap).topologicalClosure = ⊤ :=
240     hf.denseRange.topologicalClosure_map_submodule hH
241   apply top_unique
242   rw [← himage]
243   exact Submodule.topologicalClosure_mono htransport
244 
245 /-- Full dense-realization theorem for bounded operator families.  A
246 continuous surjection intertwining source operators with target operators
247 takes a topologically generating seed set to a topologically generating image
248 seed set.  Taking `B` to be the image family proves the first manuscript
249 conclusion; allowing a larger `B` proves the "hence under the target algebra"
250 clause. -/
251 theorem dense_operatorHull_image
252     (f : X →L[𝕜] Y) (hf : Surjective f)
253     (φ : (X →L[𝕜] X) → (Y →L[𝕜] Y))
254     (A : Set (X →L[𝕜] X)) (B : Set (Y →L[𝕜] Y))
255     (S : Set X) (hφ : ∀ T ∈ A, φ T ∈ B)
256     (hintertwine : ∀ T ∈ A, f.comp T = (φ T).comp f)
257     (hgenerate : (operatorHull A S).topologicalClosure = ⊤) :
258     (operatorHull B (f '' S)).topologicalClosure = ⊤ :=
259   dense_realization f hf (operatorHull A S) (operatorHull B (f '' S))
260     hgenerate (map_operatorHull_le f φ A B S hφ hintertwine)
261 
262 /-- Surjective packet-intertwining maps take a source packet onto the
263 corresponding target packet. -/
264 theorem map_packetRange_eq
265     (f : X →L[𝕜] Y) (hf : Surjective f)
266     (P : X →L[𝕜] X) (Q : Y →L[𝕜] Y)
267     (hintertwine : f.comp P = Q.comp f) :
268     P.range.map f.toLinearMap = Q.range := by
269   have hi : ∀ a, f (P a) = Q (f a) := by
270     intro a
271     simpa using congrArg (fun L : X →L[𝕜] Y ↦ L a) hintertwine
272   ext y
273   constructor
274   · rintro ⟨x, ⟨a, rfl⟩, rfl⟩
275     refine ⟨f a, ?_⟩
276     exact (hi a).symm
277   · rintro ⟨b, rfl⟩
278     rcases hf b with ⟨a, rfl⟩
279     refine ⟨P a, ⟨a, rfl⟩, ?_⟩
280     exact hi a
281 
282 /-! ## Completion of an isometric dense presentation -/
283 
284 variable {α : Type*}
285 variable [NormedAddCommGroup α] [NormedSpace 𝕜 α]
286 variable [CompleteSpace Y]
287 
288 /-- A dense linear isometry into a Banach space extends uniquely to a
289 topological linear isomorphism from the completion.  This is the normed-space
290 form of the completion clause in the universal one-seed presentation. -/
291 def completionEquivOfIsometryDense
292     (f : α →L[𝕜] Y) (hiso : Isometry f) (hdense : DenseRange f) :
293     Completion α ≃L[𝕜] Y := by
294   let F : Completion α →L[𝕜] Y := f.fromCompletion
295   have hFiso : Isometry F := by
296     simpa [F, ContinuousLinearMap.coe_fromCompletion] using hiso.completion_extension
297   have hFrange : DenseRange F := by
298     apply hdense.mono
299     rintro y ⟨x, rfl⟩
300     refine ⟨(x : Completion α), ?_⟩
301     simp [F]
302   have hFclosed : IsClosed (Set.range F) :=
303     hFiso.antilipschitzWith.isClosed_range hFiso.uniformContinuous
304   have hFsurj : Surjective F := by
305     rw [← Set.range_eq_univ]
306     calc
307       Set.range F = closure (Set.range F) := hFclosed.closure_eq.symm
308       _ = Set.univ := hFrange.closure_eq
309   let Fi : Completion α →ₗᵢ[𝕜] Y :=
310     { F.toLinearMap with
311       norm_map' := hFiso.norm_map_of_map_zero (map_zero F) }
312   exact (LinearIsometryEquiv.ofSurjective Fi hFsurj).toContinuousLinearEquiv
313 
314 @[simp]
315 theorem completionEquivOfIsometryDense_apply_coe
316     (f : α →L[𝕜] Y) (hiso : Isometry f) (hdense : DenseRange f) (x : α) :
317     completionEquivOfIsometryDense f hiso hdense (x : Completion α) = f x := by
318   simp [completionEquivOfIsometryDense]
319 
320 /-- The completed presentation intertwines every pair of bounded operators
321 that intertwines on the dense presentation space.  This supplies the
322 operator-action clause of the universal one-seed completion statement. -/
323 theorem completionEquivOfIsometryDense_intertwines
324     (f : α →L[𝕜] Y) (hiso : Isometry f) (hdense : DenseRange f)
325     (A : α →L[𝕜] α) (B : Y →L[𝕜] Y)
326     (hintertwine : f.comp A = B.comp f) :
327     (completionEquivOfIsometryDense f hiso hdense).toContinuousLinearMap.comp
328         A.completion =
329       B.comp (completionEquivOfIsometryDense f hiso hdense).toContinuousLinearMap := by
330   apply ContinuousLinearMap.ext
331   intro z
332   induction z using Completion.induction_on with
333   | hp => apply isClosed_eq <;> fun_prop
334   | ih x =>
335       simpa using congrArg (fun L : α →L[𝕜] Y ↦ L x) hintertwine
336 
337 /-- The extension from the preceding theorem is the unique continuous linear
338 extension of the dense presentation map. -/
339 theorem completionEquivOfIsometryDense_unique
340     (f : α →L[𝕜] Y) (hiso : Isometry f) (hdense : DenseRange f)
341     (g : Completion α →L[𝕜] Y) (
342       hg : ∀ x : α, g (x : Completion α) = f x) :
343     g = (completionEquivOfIsometryDense f hiso hdense).toContinuousLinearMap := by
344   have huniq : f.fromCompletion = g :=
345     ContinuousLinearMap.fromCompletion_unique f g fun x ↦ (hg x).symm
346   rw [← huniq]
347   ext x
348   induction x using Completion.induction_on with
349   | hp => apply isClosed_eq <;> fun_prop
350   | ih x => simp
351 
352 /-! ## Bilateral-shift dense orbit -/
353 
354 /-- The canonical delta family in `ℓ²(ℤ; 𝕂)`. -/
355 def delta {𝕂 : Type*} [RCLike 𝕂] (n : ℤ) : ℓ²(ℤ, 𝕂) :=
356   lp.single 2 n 1
357 
358 /-- The delta family has dense linear span in `ℓ²(ℤ; 𝕂)`. -/
359 theorem delta_dense_span {𝕂 : Type*} [RCLike 𝕂] :
360     (Submodule.span 𝕂 (Set.range (delta (𝕂 := 𝕂)))).topologicalClosure = ⊤ := by
361   let b : HilbertBasis ℤ 𝕂 ℓ²(ℤ, 𝕂) :=
362     HilbertBasis.ofRepr (LinearIsometryEquiv.refl 𝕂 ℓ²(ℤ, 𝕂))
363   have hb : (b : ℤ → ℓ²(ℤ, 𝕂)) = delta (𝕂 := 𝕂) := by
364     funext n
365     simpa [b, delta] using b.repr_self n
366   rw [← hb]
367   exact b.dense_span
368 
369 /-! ### Concrete coordinate reindexing on `ℓ²` -/
370 
371 /-- Reindex an `ℓ²` vector along a permutation of its coordinate type. -/
372 def reindexL2 {𝕂 I : Type*} [RCLike 𝕂] (e : I ≃ I)
373     (x : ℓ²(I, 𝕂)) : ℓ²(I, 𝕂) := by
374   refine ⟨fun i ↦ x (e i), ?_⟩
375   change Memℓp (fun i ↦ x (e i)) 2
376   rw [memℓp_gen_iff (by norm_num : 0 < ENNReal.toReal 2)]
377   have hx := (memℓp_gen_iff (by norm_num : 0 < ENNReal.toReal 2)).1 x.property
378   exact e.summable_iff.mpr hx
379 
380 @[simp]
381 theorem reindexL2_apply {𝕂 I : Type*} [RCLike 𝕂]
382     (e : I ≃ I) (x : ℓ²(I, 𝕂)) (i : I) :
383     reindexL2 e x i = x (e i) :=
384   rfl
385 
386 /-- Coordinate reindexing is a linear equivalence, with inverse given by the
387 inverse permutation. -/
388 def reindexL2LinearEquiv {𝕂 I : Type*} [RCLike 𝕂] (e : I ≃ I) :
389     ℓ²(I, 𝕂) ≃ₗ[𝕂] ℓ²(I, 𝕂) where
390   toFun := reindexL2 e
391   invFun := reindexL2 e.symm
392   map_add' x y := by ext i; rfl
393   map_smul' c x := by ext i; rfl
394   left_inv x := by ext i; simp
395   right_inv x := by ext i; simp
396 
397 @[simp]
398 theorem reindexL2LinearEquiv_apply {𝕂 I : Type*} [RCLike 𝕂]
399     (e : I ≃ I) (x : ℓ²(I, 𝕂)) :
400     reindexL2LinearEquiv e x = reindexL2 e x :=
401   rfl
402 
403 /-- Coordinate reindexing preserves the `ℓ²` norm. -/
404 def reindexL2LinearIsometryEquiv {𝕂 I : Type*} [RCLike 𝕂] (e : I ≃ I) :
405     ℓ²(I, 𝕂) ≃ₗᵢ[𝕂] ℓ²(I, 𝕂) where
406   __ := reindexL2LinearEquiv e
407   norm_map' x := by
408     rw [lp.norm_eq_tsum_rpow (by norm_num : 0 < ENNReal.toReal 2)]
409     rw [lp.norm_eq_tsum_rpow (by norm_num : 0 < ENNReal.toReal 2)]
410     congr 1
411     exact e.tsum_eq (fun i ↦ ‖x i‖ ^ ENNReal.toReal 2)
412 
413 @[simp]
414 theorem reindexL2LinearIsometryEquiv_apply {𝕂 I : Type*} [RCLike 𝕂]
415     (e : I ≃ I) (x : ℓ²(I, 𝕂)) (i : I) :
416     reindexL2LinearIsometryEquiv e x i = x (e i) :=
417   rfl
418 
419 /-- A packaged bilateral-shift representation of the additive group `ℤ` on
420 `ℓ²(ℤ; 𝕂)`.  The coordinate formula determines every integer power and fixes
421 the sign convention used in Paper I. -/
422 structure BilateralShiftRepresentation (𝕂 : Type*) [RCLike 𝕂] where
423   power : ℤ → ℓ²(ℤ, 𝕂) →L[𝕂] ℓ²(ℤ, 𝕂)
424   coordinate : ∀ (m n : ℤ) (x : ℓ²(ℤ, 𝕂)), power m x n = x (n - m)
425 
426 namespace BilateralShiftRepresentation
427 
428 /-- The explicit `m`th bilateral-shift power, constructed as the continuous
429 linear isometry induced by the coordinate permutation `n ↦ n-m`. -/
430 def concretePower {𝕂 : Type*} [RCLike 𝕂]
431     (m : ℤ) : ℓ²(ℤ, 𝕂) →L[𝕂] ℓ²(ℤ, 𝕂) :=
432   (reindexL2LinearIsometryEquiv (Equiv.subRight m)).toContinuousLinearEquiv.toContinuousLinearMap
433 
434 @[simp]
435 theorem concretePower_apply {𝕂 : Type*} [RCLike 𝕂]
436     (m n : ℤ) (x : ℓ²(ℤ, 𝕂)) :
437     concretePower m x n = x (n - m) :=
438   rfl
439 
440 /-- The concrete, inhabited bilateral-shift representation on `ℓ²(ℤ;𝕂)`. -/
441 def concrete {𝕂 : Type*} [RCLike 𝕂] : BilateralShiftRepresentation 𝕂 where
442   power := concretePower
443   coordinate := concretePower_apply
444 
445 @[simp]
446 theorem power_zero {𝕂 : Type*} [RCLike 𝕂]
447     (S : BilateralShiftRepresentation 𝕂) :
448     S.power 0 = ContinuousLinearMap.id 𝕂 ℓ²(ℤ, 𝕂) := by
449   ext x n
450   simp [S.coordinate]
451 
452 /-- The packaged powers obey the additive group law. -/
453 theorem power_add {𝕂 : Type*} [RCLike 𝕂]
454     (S : BilateralShiftRepresentation 𝕂) (m k : ℤ) :
455     S.power (m + k) = (S.power m).comp (S.power k) := by
456   ext x n
457   simp only [S.coordinate, ContinuousLinearMap.comp_apply]
458   apply congrArg (fun q : ℤ ↦ x q)
459   ring
460 
461 /-- The negative power is a two-sided inverse to the positive power. -/
462 theorem power_neg_comp {𝕂 : Type*} [RCLike 𝕂]
463     (S : BilateralShiftRepresentation 𝕂) (m : ℤ) :
464     (S.power (-m)).comp (S.power m) = ContinuousLinearMap.id 𝕂 ℓ²(ℤ, 𝕂) := by
465   rw [← S.power_add]
466   simp
467 
468 end BilateralShiftRepresentation
469 
470 /-- A seed is topologically cyclic for `A` when its bounded-operator hull is
471 dense. -/
472 def TopologicallyCyclic {𝕂 E : Type*}
473     [NontriviallyNormedField 𝕂] [NormedAddCommGroup E] [NormedSpace 𝕂 E]
474     (A : Set (E →L[𝕂] E)) (s : E) : Prop :=
475   (operatorHull A ({s} : Set E)).topologicalClosure = ⊤
476 
477 /-- Proposition-level form of "topological seed rank one": a singleton seed
478 generates densely, while the empty seed family does not. -/
479 def HasTopologicalSeedRankOne {𝕂 E : Type*}
480     [NontriviallyNormedField 𝕂] [NormedAddCommGroup E] [NormedSpace 𝕂 E]
481     (A : Set (E →L[𝕂] E)) : Prop :=
482   (∃ s, TopologicallyCyclic A s) ∧
483     (operatorHull A (∅ : Set E)).topologicalClosure ≠ ⊤
484 
485 /-- `GeneratesWithNSeeds A n` records dense generation by an explicitly
486 finite seed set of cardinality `n`. -/
487 def GeneratesWithNSeeds {𝕂 E : Type*}
488     [NontriviallyNormedField 𝕂] [NormedAddCommGroup E] [NormedSpace 𝕂 E]
489     (A : Set (E →L[𝕂] E)) (n : ℕ) : Prop :=
490   ∃ S : Finset E, S.card = n ∧
491     (operatorHull A (S : Set E)).topologicalClosure = ⊤
492 
493 /-- The singleton/empty-set certificate implies the literal finite-cardinality
494 statement: one seed suffices and zero seeds do not. -/
495 theorem HasTopologicalSeedRankOne.cardinality_one_and_not_zero
496     {𝕂 E : Type*}
497     [NontriviallyNormedField 𝕂] [NormedAddCommGroup E] [NormedSpace 𝕂 E]
498     {A : Set (E →L[𝕂] E)} (h : HasTopologicalSeedRankOne A) :
499     GeneratesWithNSeeds A 1 ∧ ¬ GeneratesWithNSeeds A 0 := by
500   classical
501   rcases h.1 with ⟨s, hs⟩
502   constructor
503   · refine ⟨{s}, by simp, ?_⟩
504     simpa [TopologicallyCyclic] using hs
505   · rintro ⟨S, hcard, hgen⟩
506     have hS : S = ∅ := Finset.card_eq_zero.mp hcard
507     subst S
508     exact h.2 (by simpa using hgen)
509 
510 /-- If the integer powers of a bounded bilateral shift send the impulse at
511 zero to the corresponding delta vectors, then that orbit is topologically
512 generating.  This is the dense-orbit conclusion used to prove topological
513 seed rank one. -/
514 theorem bilateralShift_dense_orbit
515     {𝕂 : Type*} [RCLike 𝕂]
516     (S : ℤ → ℓ²(ℤ, 𝕂) →L[𝕂] ℓ²(ℤ, 𝕂))
517     (horbit : ∀ n, S n (delta (𝕂 := 𝕂) 0) = delta (𝕂 := 𝕂) n) :
518     (Submodule.span 𝕂
519       (Set.range fun n ↦ S n (delta (𝕂 := 𝕂) 0))).topologicalClosure = ⊤ := by
520   have hrange :
521       Set.range (fun n ↦ S n (delta (𝕂 := 𝕂) 0)) =
522         Set.range (delta (𝕂 := 𝕂)) := by
523     ext x
524     simp only [Set.mem_range]
525     constructor
526     · rintro ⟨n, rfl⟩
527       exact ⟨n, (horbit n).symm⟩
528     · rintro ⟨n, rfl⟩
529       exact ⟨n, horbit n⟩
530   rw [hrange]
531   exact delta_dense_span
532 
533 /-- Coordinate-form version for the actual bilateral shift powers.  If
534 `S m` acts by `(S^m x)[n] = x[n-m]`, then the orbit of `δ₀` is dense.  In
535 particular, `S 1` has the manuscript convention `(Sx)[n] = x[n-1]`. -/
536 theorem bilateralShift_dense_orbit_of_coordinate_formula
537     {𝕂 : Type*} [RCLike 𝕂]
538     (S : ℤ → ℓ²(ℤ, 𝕂) →L[𝕂] ℓ²(ℤ, 𝕂))
539     (hS : ∀ (m n : ℤ) (x : ℓ²(ℤ, 𝕂)), S m x n = x (n - m)) :
540     (Submodule.span 𝕂
541       (Set.range fun m ↦ S m (delta (𝕂 := 𝕂) 0))).topologicalClosure = ⊤ := by
542   apply bilateralShift_dense_orbit S
543   intro m
544   ext n
545   rw [hS]
546   simp [delta, lp.single_apply, Pi.single_apply, sub_eq_zero, eq_comm]
547 
548 /-- The actual packaged bilateral shift is topologically cyclic at `δ₀`. -/
549 theorem BilateralShiftRepresentation.topologicallyCyclic_delta
550     {𝕂 : Type*} [RCLike 𝕂] (S : BilateralShiftRepresentation 𝕂) :
551     TopologicallyCyclic (Set.range S.power) (delta (𝕂 := 𝕂) 0) := by
552   unfold TopologicallyCyclic operatorHull
553   have hdense := bilateralShift_dense_orbit_of_coordinate_formula S.power S.coordinate
554   apply top_unique
555   rw [← hdense]
556   apply Submodule.topologicalClosure_mono
557   apply Submodule.span_le.2
558   rintro x ⟨m, rfl⟩
559   apply Submodule.subset_span
560   exact ⟨S.power m, ⟨m, rfl⟩, delta (𝕂 := 𝕂) 0, Set.mem_singleton _, rfl⟩
561 
562 /-- Named seed-rank-one wrapper for Paper I's bilateral-shift proposition. -/
563 theorem BilateralShiftRepresentation.hasTopologicalSeedRankOne
564     {𝕂 : Type*} [RCLike 𝕂] (S : BilateralShiftRepresentation 𝕂) :
565     HasTopologicalSeedRankOne (Set.range S.power) := by
566   refine ⟨⟨delta (𝕂 := 𝕂) 0, S.topologicallyCyclic_delta⟩, ?_⟩
567   intro htop
568   have hmem :
569       delta (𝕂 := 𝕂) 0 ∈
570         (operatorHull (Set.range S.power) (∅ : Set ℓ²(ℤ, 𝕂))).topologicalClosure := by
571     rw [htop]
572     trivial
573   have hzero : delta (𝕂 := 𝕂) 0 = 0 := by
574     simpa [operatorHull] using hmem
575   have hcoord := congrArg (fun x : ℓ²(ℤ, 𝕂) ↦ x 0) hzero
576   have hone : (1 : 𝕂) = 0 := by
577     simpa only [delta, lp.coeFn_single, Pi.single_eq_same, lp.coeFn_zero,
578       Pi.zero_apply] using hcoord
579   exact one_ne_zero hone
580 
581 /-- Unconditional concrete bilateral-shift cyclicity theorem.  Unlike the
582 generic wrapper, this theorem has no representation hypothesis: its operator
583 family is the explicit coordinate reindexing construction above. -/
584 theorem concreteBilateralShift_topologicallyCyclic
585     {𝕂 : Type*} [RCLike 𝕂] :
586     TopologicallyCyclic
587       (Set.range (BilateralShiftRepresentation.concrete (𝕂 := 𝕂)).power)
588       (delta (𝕂 := 𝕂) 0) :=
589   BilateralShiftRepresentation.concrete.topologicallyCyclic_delta
590 
591 /-- Unconditional concrete seed-rank-one certificate for the bilateral shift. -/
592 theorem concreteBilateralShift_hasTopologicalSeedRankOne
593     {𝕂 : Type*} [RCLike 𝕂] :
594     HasTopologicalSeedRankOne
595       (Set.range (BilateralShiftRepresentation.concrete (𝕂 := 𝕂)).power) :=
596   BilateralShiftRepresentation.concrete.hasTopologicalSeedRankOne
597 
598 /-- Literal minimal finite-cardinality statement for the concrete bilateral
599 shift: a one-element seed set generates densely, while no zero-element seed
600 set does. -/
601 theorem concreteBilateralShift_minimalCardinality_one
602     {𝕂 : Type*} [RCLike 𝕂] :
603     GeneratesWithNSeeds
604         (Set.range (BilateralShiftRepresentation.concrete (𝕂 := 𝕂)).power) 1 ∧
605       ¬ GeneratesWithNSeeds
606         (Set.range (BilateralShiftRepresentation.concrete (𝕂 := 𝕂)).power) 0 :=
607   concreteBilateralShift_hasTopologicalSeedRankOne.cardinality_one_and_not_zero
608 
609 /-- The genuine minimum-equals-one statement for finite topological seed
610 cardinality of the explicit bilateral-shift grammar. -/
611 theorem concreteBilateralShift_seedCardinality_isLeast
612     {𝕂 : Type*} [RCLike 𝕂] :
613     IsLeast
614       {n : ℕ | GeneratesWithNSeeds
615         (Set.range (BilateralShiftRepresentation.concrete (𝕂 := 𝕂)).power) n}
616       1 := by
617   rcases concreteBilateralShift_minimalCardinality_one (𝕂 := 𝕂) with ⟨hOne, hZero⟩
618   refine ⟨hOne, ?_⟩
619   intro n hn
620   exact Nat.one_le_iff_ne_zero.mpr fun hnZero ↦ hZero (hnZero ▸ hn)
621 
622 end BoundedProjectorFamily
623 
624 end KomorebiVerification.TopologicalCompletion

Back to source controls