SpineExistenceCriterion.lean

1 import PaperX.ConditionalArithmeticSpine
2 import PaperX.RequiredPacketOccupancy
3 
4 /-! The full conditional existence boundary of source Claim 11.2.
5 The system realizes the complete chosen spine. Occupancy means an actual nonzero
6 joint eigenvector for every required supplied packet. These are conjunctive
7 requirements; no system-to-carrier embedding or universal occupancy is inferred.
8 -/
9 set_option autoImplicit false
10 namespace PaperX.SpineExistenceCriterion
11 open PaperX.RepresentationLimits PaperX.RepresentationClasses
12 open PaperX.RepresentationTopology PaperX.ClassCompletion PaperX.ClassInvariants
13 open PaperX.ConditionalArithmeticSpine PaperX.InverseLimitLocalConditions
14 open PaperX.DeterminantSpine PaperX.JointOccupancy
15 open PaperX.RequiredPacketOccupancy
16 
17 variable {Λ G ι V E : Type} [Group G] [TopologicalSpace G]
18   [Fintype ι] [DecidableEq ι] [Field E]
19 variable (O K : Λ → Type) [∀ l, CommRing (O l)] [∀ l, Field (K l)]
20   [∀ l, TopologicalSpace (K l)]
21 variable (I : (l : Λ) → Ideal (O l)) [∀ l, IsAdicComplete (I l) (O l)]
22 variable (hI : ∀ l, (I l).FG) [∀ l, Finite (O l ⧸ I l)]
23 variable (C : (l : Λ) → ClassConditions (G := G) (ι := ι) (I l))
24 variable (finite : ∀ l k, 0 < k → Finite {c // (C l).allowed k c})
25 variable (continuous : ∀ l k c, (C l).allowed k c →
26   ∃ ρ, classOf ρ = c ∧ FiniteRepContinuous ρ)
27 variable (inc : (l : Λ) → O l →+* K l)
28 variable (hinc : ∀ l, @Continuous (O l) (K l) (I l).adicTopology inferInstance (inc l))
29 variable (emb : (l : Λ) → E →+* K l)
30 variable (S : Spine (G := G) (ι := ι) (V := V) (E := E) K)
31 variable (closed : ∀ l, InverseLimitClosed (I l) (C l)
32   (fun ρ => LocalRealizes S l (changeCoefficients (inc l) ρ)))
33 variable (localP : (l : Λ) → V → Polynomial (O l))
34 variable (poly_integral : ∀ l v, S.good l v →
35   (localP l v).map (inc l) = (S.polynomial v).map (emb l))
36 variable (poly_spec : ∀ l k c, (C l).allowed k c → ∀ v, S.good l v →
37   classCharpoly c (S.sample v) = (localP l v).map (Ideal.Quotient.mk ((I l)^k)))
38 variable (localDet : (l : Λ) → G → O l)
39 variable (det_integral : ∀ l g, inc l (localDet l g) = S.determinant l g)
40 variable (det_spec : ∀ l k c, (C l).allowed k c → ∀ g,
41   classDet c g = Ideal.Quotient.mk ((I l)^k) (localDet l g))
42 
43 /-- Actual integral representatives with allowed reductions, continuous field
44 members, and every item of the prescribed common spine. -/
45 def SystemRealization (ρ : (l : Λ) → MatrixRep (O l) G ι) : Prop :=
46   (∀ l k, (C l).allowed k (classOf (reduce (I l) (ρ l) k))) ∧
47   (∀ l, Continuous (changeCoefficients (inc l) (ρ l))) ∧
48   RealizesSpine S emb (fun l => changeCoefficients (inc l) (ρ l))
49 
50 include hI finite continuous hinc closed poly_integral poly_spec det_integral det_spec in
51 /-- Completing the full spine is equivalent to nonemptiness at every positive
52 precision, under the same ambient and closure assumptions as Claim 8.2. -/
53 theorem system_iff_positive_levels :
54     (∃ ρ, SystemRealization O K I C inc emb S ρ) ↔
55       ∀ l k, 0 < k → ∃ c, (C l).allowed k c := by
56   constructor
57   · rintro ⟨ρ, hρ, _, _⟩ l k _
58     exact ⟨classOf (reduce (I l) (ρ l) k), hρ l k⟩
59   · intro occupied
60     exact adelic_finite_depth_completion O I hI C finite occupied continuous inc hinc
61       emb S closed localP poly_integral poly_spec localDet det_integral det_spec
62 
63 include hI finite continuous hinc closed poly_integral poly_spec det_integral det_spec in
64 /-- Residual companions and all higher levels are kept as separate requirements. -/
65 theorem system_iff_residual_and_higher :
66     (∃ ρ, SystemRealization O K I C inc emb S ρ) ↔
67       (∀ l, ∃ c, (C l).allowed 1 c) ∧
68       ∀ l k, 2 ≤ k → ∃ c, (C l).allowed k c := by
69   rw [system_iff_positive_levels O K I hI C finite continuous inc hinc emb S
70     closed localP poly_integral poly_spec localDet det_integral det_spec]
71   constructor
72   · intro h
73     exact ⟨fun l => h l 1 (by decide), fun l k hk => h l k (by omega)⟩
74   · rintro ⟨h1, hh⟩ l k hk
75     by_cases he : k = 1
76     · subst k
77       exact h1 l
78     · exact hh l k (by omega)
79 
80 variable {P : Type} (F A J : P → Type) [∀ p, Field (F p)]
81   [∀ p, CharZero (F p)] [∀ p, AddCommGroup (A p)] [∀ p, Module (F p) (A p)]
82   [∀ p, FiniteDimensional (F p) (A p)]
83 variable (T : (p : P) → J p → Module.End (F p) (A p))
84   (a : (p : P) → J p → F p) (indices : (p : P) → List (J p))
85 variable (hs : ∀ p j, PaperX.SpectralProjectors.Split (T p j))
86   (hc : ∀ p i j, Commute (T p i) (T p j))
87 
88 include hI finite continuous hinc closed poly_integral poly_spec det_integral det_spec hs hc in
89 /-- The full common-spine realization and occupancy of every required supplied
90 packet are equivalent to residual occupancy, all higher depths, and nonzero
91 actual projector trace for every packet. The required packet index may be infinite. -/
92 theorem system_and_every_packet_iff_trace_ne_zero :
93     (∃ ρ, SystemRealization O K I C inc emb S ρ ∧
94       ∀ p, Occupied (T p) (a p) (indices p)) ↔
95     (∀ l, ∃ c, (C l).allowed 1 c) ∧
96     (∀ l k, 2 ≤ k → ∃ c, (C l).allowed k c) ∧
97     ∀ p, LinearMap.trace (F p) (A p) (joint (T p) (a p) (indices p)) ≠ 0 := by
98   have hsystem := system_iff_residual_and_higher O K I hI C finite continuous
99     inc hinc emb S closed localP poly_integral poly_spec localDet det_integral det_spec
100   constructor
101   · rintro ⟨ρ, hρ, hp⟩
102     obtain ⟨h1, hh⟩ := hsystem.mp ⟨ρ, hρ⟩
103     exact ⟨h1, hh, fun p =>
104       (occupied_iff_trace_ne_zero (T p) (a p) (hs p) (hc p) (indices p)).mp (hp p)⟩
105   · rintro ⟨h1, hh, hp⟩
106     obtain ⟨ρ, hρ⟩ := hsystem.mpr ⟨h1, hh⟩
107     exact ⟨ρ, hρ, fun p =>
108       (occupied_iff_trace_ne_zero (T p) (a p) (hs p) (hc p) (indices p)).mpr (hp p)⟩
109 
110 include hI finite continuous hinc closed poly_integral poly_spec det_integral det_spec hs hc in
111 /-- The source's positive trace convention is a positive natural-number preimage
112 of the actual trace. No order on any coefficient field is required. -/
113 theorem system_and_every_packet_iff_positive_trace :
114     (∃ ρ, SystemRealization O K I C inc emb S ρ ∧
115       ∀ p, Occupied (T p) (a p) (indices p)) ↔
116     (∀ l, ∃ c, (C l).allowed 1 c) ∧
117     (∀ l k, 2 ≤ k → ∃ c, (C l).allowed k c) ∧
118     ∀ p, PositiveTrace (T p) (a p) (indices p) := by
119   rw [system_and_every_packet_iff_trace_ne_zero O K I hI C finite continuous
120     inc hinc emb S closed localP poly_integral poly_spec localDet det_integral det_spec
121     F A J T a indices hs hc]
122   constructor
123   · rintro ⟨h1, hh, hp⟩
124     exact ⟨h1, hh, fun p =>
125       (positiveTrace_iff_fieldTrace_ne_zero (T p) (a p) (hs p) (hc p) (indices p)).mpr
126         (hp p)⟩
127   · rintro ⟨h1, hh, hp⟩
128     exact ⟨h1, hh, fun p =>
129       (positiveTrace_iff_fieldTrace_ne_zero (T p) (a p) (hs p) (hc p) (indices p)).mp
130         (hp p)⟩
131 
132 include hI finite continuous hinc closed poly_integral poly_spec det_integral det_spec hs hc in
133 /-- Complete source Claim 11.2 with explicit witnesses: a common-spine system
134 and one nonzero joint eigenvector in each required supplied carrier exist exactly
135 when residual companions, every higher depth, and every positive packet trace do.
136 The witnesses may belong to different vector spaces and are not identified. -/
137 theorem full_existence_boundary :
138     (∃ ρ, ∃ x : (p : P) → A p,
139       SystemRealization O K I C inc emb S ρ ∧
140       ∀ p, x p ≠ 0 ∧ ∀ i ∈ indices p, T p i (x p) = a p i • x p) ↔
141     (∀ l, ∃ c, (C l).allowed 1 c) ∧
142     (∀ l k, 2 ≤ k → ∃ c, (C l).allowed k c) ∧
143     ∀ p, PositiveTrace (T p) (a p) (indices p) := by
144   have h := system_and_every_packet_iff_positive_trace O K I hI C finite continuous
145     inc hinc emb S closed localP poly_integral poly_spec localDet det_integral det_spec
146     F A J T a indices hs hc
147   constructor
148   · rintro ⟨ρ, x, hρ, hx⟩
149     exact h.mp ⟨ρ, hρ, fun p => ⟨x p, hx p⟩⟩
150   · intro hp
151     obtain ⟨ρ, hρ, hpackets⟩ := h.mpr hp
152     obtain ⟨x, hx⟩ := (all_packets_iff_witnesses F A J T a indices).mp hpackets
153     exact ⟨ρ, x, hρ, hx⟩
154 
155 end PaperX.SpineExistenceCriterion

Back to source controls