IndexedExistenceBoundary.lean

1 import PaperX.CompletionAssembly
2 
3 /-! Source-faithful quantifiers for every required packet. Carriers and local
4 closure are supplied. Completion never forces their independent occupancy. -/
5 set_option autoImplicit false
6 namespace PaperX.IndexedExistenceBoundary
7 open PaperX.RepresentationLimits PaperX.RepresentationTopology PaperX.RepresentationForests
8 open PaperX.SystemCompletion PaperX.CompletionAssembly PaperX.JointOccupancy
9 
10 variable {Λ G ι P : Type} [Group G] [TopologicalSpace G] [Fintype ι] [DecidableEq ι]
11 variable (O : Λ → Type) [∀ l, CommRing (O l)] (I : (l : Λ) → Ideal (O l))
12 variable [∀ l, IsAdicComplete (I l) (O l)]
13 variable (C : (l : Λ) → Conditions (G := G) (ι := ι) (I l))
14 variable (finite : ∀ l k, Finite {ρ : MatrixRep (O l ⧸ (I l)^k) G ι // (C l).allowed k ρ})
15 variable (continuous : ∀ l k ρ, (C l).allowed k ρ → FiniteRepContinuous ρ)
16 variable (Local : (l : Λ) → MatrixRep (O l) G ι → Prop)
17 variable (stable : ∀ l ρ, Realizes (I l) (C l) ρ → Local l ρ)
18 variable (K V J : P → Type) [∀ p, Field (K p)] [∀ p, CharZero (K p)]
19 variable [∀ p, AddCommGroup (V p)] [∀ p, Module (K p) (V p)]
20 variable [∀ p, FiniteDimensional (K p) (V p)]
21 variable (T : (p : P) → J p → Module.End (K p) (V p))
22 variable (a : (p : P) → J p → K p) (indices : (p : P) → List (J p))
23 variable (hs : ∀ p j, PaperX.SpectralProjectors.Split (T p j))
24 variable (hc : ∀ p i j, Commute (T p i) (T p j))
25 
26 include finite continuous stable hs hc in
27 /-- Residual companions, every higher depth, and every supplied required packet
28 are separate and jointly necessary/sufficient under the stated closure input. -/
29 theorem all_required_packets_iff :
30     (∃ ρ : (l : Λ) → MatrixRep (O l) G ι,
31       SystemRealizes O I C ρ ∧
32       (∀ l, AdicRepContinuous (I l) (ρ l) ∧ Local l (ρ l)) ∧
33       ∀ p, Occupied (T p) (a p) (indices p)) ↔
34     (∀ l, ∃ τ, (C l).allowed 1 τ) ∧
35     (∀ l k, 2 ≤ k → ∃ τ, (C l).allowed k τ) ∧
36     ∀ p, LinearMap.trace (K p) (V p) (joint (T p) (a p) (indices p)) ≠ 0 := by
37   constructor
38   · rintro ⟨ρ, hρ, _, hp⟩
39     refine ⟨fun l => ⟨reduce (I l) (ρ l) 1, hρ l 1⟩,
40       fun l k _ => ⟨reduce (I l) (ρ l) k, hρ l k⟩, ?_⟩
41     intro p
42     exact (occupied_iff_trace_ne_zero (T p) (a p) (hs p) (hc p) (indices p)).mp (hp p)
43   · rintro ⟨h1, hh, hp⟩
44     have hall : ∀ l k, ∃ τ, (C l).allowed k τ := fun l =>
45       (residual_and_higher_iff_all (I l) (C l)).mp ⟨h1 l, hh l⟩
46     obtain ⟨ρ, hρ, hl⟩ := continuous_system_completion O I C finite hall continuous Local stable
47     refine ⟨ρ, hρ, hl, ?_⟩
48     intro p
49     exact (occupied_iff_trace_ne_zero (T p) (a p) (hs p) (hc p) (indices p)).mpr (hp p)
50 
51 end PaperX.IndexedExistenceBoundary

Back to source controls