SeedOrbit.lean

1 module
2 public import Mathlib.LinearAlgebra.Matrix.Rank
3 public import Mathlib.LinearAlgebra.Dimension.Constructions
4 public import Mathlib.LinearAlgebra.Pi
5 public import Mathlib.Analysis.Complex.Basic
6 public import Mathlib.Algebra.Order.Floor.Div
7 public import Mathlib.LinearAlgebra.Matrix.Kronecker
8 public import Mathlib.Analysis.Matrix.PosDef
9 public import Mathlib.Tactic
10 
11 /-! Author: Komorebi P. Paper VII, checked third block.
12 This module is independently compilable using the pinned portable Lean kit. -/
13 public section
14 set_option autoImplicit false
15 set_option linter.unusedSectionVars false
16 set_option backward.isDefEq.respectTransparency false
17 set_option backward.isDefEq.respectTransparency.types false
18 namespace KomorebiPaperVII.SeedOrbit
19 open Matrix Module
20 open scoped Kronecker
21 variable {d m : Type*} [Fintype d] [Fintype m]
22 
23 /-- The row space is the actual image of right multiplication by C. -/
24 noncomputable def rowSpace (C : Matrix d m ℂ) : Submodule ℂ (m → ℂ) :=
25   LinearMap.range C.vecMulLinear
26 
27 /-- Actual algebra orbit. It is already a linear subspace. -/
28 noncomputable def orbitSpace (C : Matrix d m ℂ) : Submodule ℂ (Matrix d m ℂ) :=
29   LinearMap.range (C.vecMulLinear.compLeft d)
30 
31 theorem mem_orbit_iff (C X : Matrix d m ℂ) :
32     X ∈ orbitSpace C ↔ ∃ A : Matrix d d ℂ, A * C = X := by
33   rfl
34 
35 theorem mem_orbit_iff_rows (C X : Matrix d m ℂ) :
36     X ∈ orbitSpace C ↔ ∀ i, X i ∈ rowSpace C := by
37   constructor
38   · rintro ⟨A, rfl⟩ i
39     exact ⟨A i, rfl⟩
40   · intro h
41     have h' : ∀ i, ∃ a : d → ℂ, a ᵥ* C = X i := h
42     choose A hA using h'
43     exact ⟨A, funext hA⟩
44 
45 noncomputable def orbitRowEquiv (C : Matrix d m ℂ) :
46     orbitSpace C ≃ₗ[ℂ] (d → rowSpace C) where
47   toFun X i := ⟨X.val i, (mem_orbit_iff_rows C X.val).mp X.property i⟩
48   invFun f := ⟨fun i => (f i).val, (mem_orbit_iff_rows C _).mpr (fun i => (f i).property)⟩
49   left_inv _ := rfl
50   right_inv _ := rfl
51   map_add' _ _ := rfl
52   map_smul' _ _ := rfl
53 
54 theorem row_dimension (C : Matrix d m ℂ) :
55     finrank ℂ (rowSpace C) = C.rank := by
56   rw [rowSpace, range_vecMulLinear, ← Matrix.rank_eq_finrank_span_row]
57 
58 theorem orbit_dimension (C : Matrix d m ℂ) :
59     finrank ℂ (orbitSpace C) = Fintype.card d * C.rank := by
60   rw [(orbitRowEquiv C).finrank_eq, Module.finrank_pi_fintype]
61   simp [row_dimension]
62 
63 theorem orbit_span (C : Matrix d m ℂ) :
64     Submodule.span ℂ (Set.range fun A : Matrix d d ℂ => A * C) = orbitSpace C := by
65   change Submodule.span ℂ (orbitSpace C : Set (Matrix d m ℂ)) = orbitSpace C
66   exact Submodule.span_eq _
67 
68 theorem span_orbit_dimension (C : Matrix d m ℂ) :
69     finrank ℂ (Submodule.span ℂ (Set.range fun A : Matrix d d ℂ => A * C)) =
70       Fintype.card d * C.rank := by
71   rw [orbit_span, orbit_dimension]
72 
73 theorem cyclic_iff_full_rank [Nonempty d] (C : Matrix d m ℂ) :
74     orbitSpace C = ⊤ ↔ C.rank = Fintype.card m := by
75   rw [Submodule.eq_top_iff_finrank_eq, orbit_dimension]
76   have hdim : finrank ℂ (Matrix d m ℂ) = Fintype.card d * Fintype.card m := by
77     change finrank ℂ (d → m → ℂ) = _
78     simp [Module.finrank_pi_fintype]
79   rw [hdim]
80   exact Nat.mul_left_cancel_iff (Fintype.card_pos)
81 
82 theorem cyclic_multiplicity_bound [Nonempty d] (C : Matrix d m ℂ)
83     (h : orbitSpace C = ⊤) : Fintype.card m ≤ Fintype.card d := by
84   rw [← (cyclic_iff_full_rank C).mp h]
85   exact C.rank_le_card_height
86 
87 
88 /-! Actual multi-seed matrix action and the sharp generator count. -/
89 variable {o k : Type*} [Fintype o] [Fintype k]
90 noncomputable def rowOrbit (C : Matrix d m ℂ) (o : Type*) : Submodule ℂ (o → m → ℂ) :=
91   LinearMap.range (C.vecMulLinear.compLeft o)
92 
93 theorem rowOrbit_mem (C : Matrix d m ℂ) (X : o → m → ℂ) :
94     X ∈ rowOrbit C o ↔ ∀ i, X i ∈ rowSpace C := by
95   constructor
96   · rintro ⟨A, rfl⟩ i
97     exact ⟨A i, rfl⟩
98   · intro h
99     have h' : ∀ i, ∃ a : d → ℂ, a ᵥ* C = X i := h
100     choose A hA using h'
101     exact ⟨A, funext hA⟩
102 
103 noncomputable def rowOrbitEquiv (C : Matrix d m ℂ) :
104     rowOrbit C o ≃ₗ[ℂ] (o → rowSpace C) where
105   toFun X i := ⟨X.val i, (rowOrbit_mem C X.val).mp X.property i⟩
106   invFun f := ⟨fun i => (f i).val, (rowOrbit_mem C _).mpr (fun i => (f i).property)⟩
107   left_inv _ := rfl
108   right_inv _ := rfl
109   map_add' _ _ := rfl
110   map_smul' _ _ := rfl
111 
112 theorem rowOrbit_dimension (C : Matrix d m ℂ) :
113     finrank ℂ (rowOrbit C o) = Fintype.card o * C.rank := by
114   rw [(rowOrbitEquiv (o := o) C).finrank_eq, Module.finrank_pi_fintype]
115   simp [row_dimension]
116 
117 theorem rowOrbit_full [Nonempty o] (C : Matrix d m ℂ) :
118     rowOrbit C o = ⊤ ↔ C.rank = Fintype.card m := by
119   rw [Submodule.eq_top_iff_finrank_eq, rowOrbit_dimension]
120   simp only [Module.finrank_pi_fintype, Finset.sum_const,
121     Finset.card_univ, smul_eq_mul, Module.finrank_self, mul_one]
122   exact Nat.mul_left_cancel_iff (Fintype.card_pos (α := o))
123 
124 def stackSeeds (C : k → Matrix d m ℂ) : Matrix (k × d) m ℂ := fun q j => C q.1 q.2 j
125 
126 /-- The explicit k-seed action, allowing a different algebra element on each seed. -/
127 def Generates (C : k → Matrix d m ℂ) : Prop :=
128   ∀ X : Matrix d m ℂ, ∃ A : k → Matrix d d ℂ, ∑ a, A a * C a = X
129 
130 theorem stacked_action (C : k → Matrix d m ℂ) (A : k → Matrix d d ℂ) :
131     (show Matrix d (k × d) ℂ from fun i q => A q.1 i q.2) * stackSeeds C = ∑ a, A a * C a := by
132   ext i j
133   simp [Matrix.sum_apply, Matrix.mul_apply, stackSeeds, Fintype.sum_prod_type]
134 
135 theorem generates_iff_rowOrbit (C : k → Matrix d m ℂ) :
136     Generates C ↔ rowOrbit (stackSeeds C) d = ⊤ := by
137   rw [Submodule.eq_top_iff']
138   constructor
139   · intro h X
140     obtain ⟨A, hA⟩ := h X
141     exact ⟨fun i q => A q.1 i q.2, (stacked_action C A).trans hA⟩
142   · intro h X
143     obtain ⟨A, hA⟩ := h X
144     refine ⟨fun a i r => A i (a,r), ?_⟩
145     rw [← stacked_action]
146     exact hA
147 
148 theorem generates_iff_rank [Nonempty d] (C : k → Matrix d m ℂ) :
149     Generates C ↔ (stackSeeds C).rank = Fintype.card m := by
150   rw [generates_iff_rowOrbit, rowOrbit_full]
151 
152 theorem seed_count_lower [Nonempty d] (C : k → Matrix d m ℂ) (h : Generates C) :
153     Fintype.card m ≤ Fintype.card k * Fintype.card d := by
154   rw [← (generates_iff_rank C).mp h, ← Fintype.card_prod]
155   exact (stackSeeds C).rank_le_card_height
156 
157 /-- Realizes every attainable full column rank by an explicit coordinate embedding. -/
158 theorem exists_full_column_rank (h : Fintype.card m ≤ Fintype.card d) :
159     ∃ C : Matrix d m ℂ, C.rank = Fintype.card m := by
160   classical
161   obtain ⟨f⟩ := Function.Embedding.nonempty_of_card_le h
162   let C : Matrix d m ℂ := fun i j => if i=f j then 1 else 0
163   have hC (x : m → ℂ) (j : m) : (C *ᵥ x) (f j) = x j := by
164     simp [C, Matrix.mulVec, dotProduct, f.injective.eq_iff]
165   have hi : Function.Injective C.mulVecLin := by
166     intro x y hxy
167     funext j
168     have h := congrFun hxy (f j)
169     simpa only [Matrix.mulVecLin_apply, hC] using h
170   refine ⟨C, ?_⟩
171   rw [Matrix.rank, LinearMap.finrank_range_of_inj hi, Module.finrank_pi]
172 
173 theorem exists_generating_seeds_iff [Nonempty d] :
174     (∃ C : k → Matrix d m ℂ, Generates C) ↔
175       Fintype.card m ≤ Fintype.card k * Fintype.card d := by
176   constructor
177   · rintro ⟨C, hC⟩
178     exact seed_count_lower C hC
179   · intro h
180     obtain ⟨D, hD⟩ := exists_full_column_rank (d := k × d) (m := m)
181       (by simpa using h)
182     refine ⟨fun a i j => D (a,i) j, (generates_iff_rank _).mpr ?_⟩
183     exact hD
184 
185 /-! Direct sums: actual simultaneous block action and its minimum seed cardinality. -/
186 section Blocks
187 variable {I : Type*} [Fintype I]
188 
189 def BlockGenerates (dd mm : I → ℕ) {s : ℕ}
190     (C : Fin s → (i : I) → Matrix (Fin (dd i)) (Fin (mm i)) ℂ) : Prop :=
191   ∀ X : (i : I) → Matrix (Fin (dd i)) (Fin (mm i)) ℂ,
192     ∃ A : Fin s → (i : I) → Matrix (Fin (dd i)) (Fin (dd i)) ℂ,
193       ∀ i, ∑ a, A a i * C a i = X i
194 
195 theorem block_generates_iff (dd mm : I → ℕ) {s : ℕ}
196     (C : Fin s → (i : I) → Matrix (Fin (dd i)) (Fin (mm i)) ℂ) :
197     BlockGenerates dd mm C ↔ ∀ i, Generates (fun a => C a i) := by
198   classical
199   constructor
200   · intro h i Y
201     let X : (j : I) → Matrix (Fin (dd j)) (Fin (mm j)) ℂ :=
202       fun j => if hji : j=i then hji.symm ▸ Y else 0
203     obtain ⟨A, hA⟩ := h X
204     exact ⟨fun a => A a i, by simpa [X] using hA i⟩
205   · intro h X
206     have hi := fun i => h i (X i)
207     choose A hA using hi
208     exact ⟨fun a i => A i a, hA⟩
209 
210 theorem exists_block_seeds_iff (dd mm : I → ℕ) (hd : ∀ i, 0 < dd i) (s : ℕ) :
211     (∃ C : Fin s → (i : I) → Matrix (Fin (dd i)) (Fin (mm i)) ℂ,
212       BlockGenerates dd mm C) ↔ ∀ i, mm i ≤ s * dd i := by
213   classical
214   constructor
215   · rintro ⟨C, hC⟩ i
216     let : Nonempty (Fin (dd i)) := Fin.pos_iff_nonempty.mp (hd i)
217     simpa using seed_count_lower (fun a => C a i) ((block_generates_iff dd mm C).mp hC i)
218   · intro h
219     have hi (i : I) : ∃ C : Fin s → Matrix (Fin (dd i)) (Fin (mm i)) ℂ,
220         Generates C := by
221       let : Nonempty (Fin (dd i)) := Fin.pos_iff_nonempty.mp (hd i)
222       exact exists_generating_seeds_iff.mpr (by simpa using h i)
223     choose C hC using hi
224     exact ⟨fun a i => C i a, (block_generates_iff dd mm _).mpr hC⟩
225 
226 noncomputable def seedRankFormula (dd mm : I → ℕ) : ℕ :=
227   Finset.univ.sup (fun i => mm i ⌈/⌉ dd i)
228 
229 theorem seed_formula_le_iff (dd mm : I → ℕ) (hd : ∀ i, 0 < dd i) (s : ℕ) :
230     seedRankFormula dd mm ≤ s ↔ ∀ i, mm i ≤ s * dd i := by
231   simp only [seedRankFormula, Finset.sup_le_iff, Finset.mem_univ, forall_true_left]
232   constructor
233   · intro h i
234     simpa only [Nat.mul_comm] using (ceilDiv_le_iff_le_mul (hd i)).mp (h i)
235   · intro h i
236     exact (ceilDiv_le_iff_le_mul (hd i)).mpr (by simpa only [Nat.mul_comm] using h i)
237 
238 /-- Sharp minimum, with existence witnessed by explicit matrix seeds. -/
239 theorem quantum_seed_rank (dd mm : I → ℕ) (hd : ∀ i, 0 < dd i) :
240     IsLeast {s : ℕ | ∃ C : Fin s → (i : I) → Matrix (Fin (dd i)) (Fin (mm i)) ℂ,
241       BlockGenerates dd mm C} (seedRankFormula dd mm) := by
242   constructor
243   · exact (exists_block_seeds_iff dd mm hd _).mpr
244       ((seed_formula_le_iff dd mm hd _).mp le_rfl)
245   · intro s hs
246     exact (seed_formula_le_iff dd mm hd s).mpr ((exists_block_seeds_iff dd mm hd s).mp hs)
247 end Blocks
248 
249 
250 /-! Bipartite tensor coefficients, minimum product length, and actual partial trace. -/
251 
252 /-- Coefficients in the product of the two standard orthonormal bases. -/
253 def coefficientEquiv : (d × m → ℂ) ≃ₗ[ℂ] Matrix d m ℂ where
254   toFun psi i j := psi (i,j)
255   invFun C q := C q.1 q.2
256   left_inv _ := rfl
257   right_inv _ := rfl
258   map_add' _ _ := rfl
259   map_smul' _ _ := rfl
260 
261 theorem local_tensor_action [DecidableEq m] (A : Matrix d d ℂ) (psi : d × m → ℂ) :
262     coefficientEquiv ((A ⊗ₖ (1 : Matrix m m ℂ)) *ᵥ psi) = A * coefficientEquiv psi := by
263   ext i j
264   simp [coefficientEquiv, Matrix.mulVec, dotProduct,
265     Fintype.sum_prod_type, Matrix.one_apply, Matrix.mul_apply]
266 
267 /-- A sum of s genuine product vectors, not a rank assumption. -/
268 def HasProductDecomposition (C : Matrix d m ℂ) (s : ℕ) : Prop :=
269   ∃ u : Fin s → d → ℂ, ∃ v : Fin s → m → ℂ,
270     ∀ i j, C i j = ∑ a, u a i * v a j
271 
272 theorem product_decomposition_rank_bound (C : Matrix d m ℂ) {s : ℕ}
273     (h : HasProductDecomposition C s) : C.rank ≤ s := by
274   obtain ⟨u, v, h⟩ := h
275   let U : Matrix d (Fin s) ℂ := fun i a => u a i
276   let V : Matrix (Fin s) m ℂ := v
277   have hc : C = U * V := by ext i j; exact h i j
278   rw [hc]
279   exact (Matrix.rank_mul_le_right U V).trans (by simpa using V.rank_le_card_height)
280 
281 noncomputable def rowVector (C : Matrix d m ℂ) (i : d) : rowSpace C := by
282   classical
283   refine ⟨C i, Pi.single i 1, ?_⟩
284   change Pi.single i 1 ᵥ* C = C i
285   rw [Matrix.single_vecMul, one_smul]
286   rfl
287 
288 /-- Constructs a minimum-length product decomposition using a row-space basis. -/
289 theorem product_decomposition_at_rank (C : Matrix d m ℂ) : HasProductDecomposition C C.rank := by
290   classical
291   let b := Module.finBasisOfFinrankEq ℂ (rowSpace C) (row_dimension C)
292   refine ⟨fun a i => b.repr (rowVector C i) a, fun a j => (b a).val j, ?_⟩
293   intro i j
294   have h := congrArg (fun x : rowSpace C => x.val j) (b.sum_repr (rowVector C i))
295   simpa only [rowVector, Submodule.coe_sum, Submodule.coe_smul, Finset.sum_apply, Pi.smul_apply,
296     smul_eq_mul] using h.symm
297 
298 theorem product_length_minimum (C : Matrix d m ℂ) :
299     IsLeast {s : ℕ | HasProductDecomposition C s} C.rank := by
300   exact ⟨product_decomposition_at_rank C, fun _ h => product_decomposition_rank_bound C h⟩
301 
302 /-- Schmidt rank defined independently as the least number of product-vector summands. -/
303 noncomputable def schmidtRank (psi : d × m → ℂ) : ℕ := by
304   classical
305   exact Nat.find (show ∃ s, HasProductDecomposition (coefficientEquiv psi) s from
306     ⟨_, product_decomposition_at_rank _⟩)
307 
308 theorem schmidt_rank_eq_matrix_rank (psi : d × m → ℂ) :
309     schmidtRank psi = (coefficientEquiv psi).rank := by
310   classical
311   unfold schmidtRank
312   apply le_antisymm
313   · exact Nat.find_min' _ (product_decomposition_at_rank _)
314   · exact product_decomposition_rank_bound _ (Nat.find_spec _)
315 
316 noncomputable def localOrbit (psi : d × m → ℂ) : Submodule ℂ (d × m → ℂ) :=
317   (orbitSpace (coefficientEquiv psi)).map coefficientEquiv.symm.toLinearMap
318 
319 theorem local_orbit_is_tensor_span [DecidableEq m] (psi : d × m → ℂ) :
320     localOrbit psi = Submodule.span ℂ
321       (Set.range fun A : Matrix d d ℂ => (A ⊗ₖ (1 : Matrix m m ℂ)) *ᵥ psi) := by
322   rw [localOrbit, ← orbit_span, Submodule.map_span, ← Set.range_comp]
323   congr 2
324   funext A
325   apply coefficientEquiv.injective
326   simpa using (local_tensor_action A psi).symm
327 
328 theorem local_orbit_schmidt_dimension (psi : d × m → ℂ) :
329     finrank ℂ (localOrbit psi) = Fintype.card d * schmidtRank psi := by
330   rw [localOrbit, LinearEquiv.finrank_map_eq, orbit_dimension, schmidt_rank_eq_matrix_rank]
331 
332 /-- The actual B-reduced matrix obtained by tracing the A-index of |psi><psi|. -/
333 def reducedB (psi : d × m → ℂ) : Matrix m m ℂ :=
334   fun j l => ∑ i, psi (i,j) * star (psi (i,l))
335 
336 theorem partial_trace_gram (psi : d × m → ℂ) :
337     reducedB psi = (coefficientEquiv psi)ᵀ * ((coefficientEquiv psi)ᵀ)ᴴ := by
338   ext j l
339   rfl
340 
341 open scoped ComplexOrder
342 
343 theorem reduced_rank_eq_schmidt (psi : d × m → ℂ) :
344     (reducedB psi).rank = schmidtRank psi := by
345   rw [partial_trace_gram, Matrix.rank_self_mul_conjTranspose,
346     Matrix.rank_transpose, schmidt_rank_eq_matrix_rank]
347 
348 theorem reduced_positive (psi : d × m → ℂ) : (reducedB psi).PosSemidef := by
349   rw [partial_trace_gram]
350   exact Matrix.posSemidef_self_mul_conjTranspose _
351 
352 theorem reduced_full_support_iff (psi : d × m → ℂ) :
353     LinearMap.range (reducedB psi).mulVecLin = ⊤ ↔ schmidtRank psi = Fintype.card m := by
354   rw [Submodule.eq_top_iff_finrank_eq, ← Matrix.rank, reduced_rank_eq_schmidt,
355     Module.finrank_pi]
356 
357 theorem local_orbit_full_iff [Nonempty d] (psi : d × m → ℂ) :
358     localOrbit psi = ⊤ ↔ schmidtRank psi = Fintype.card m := by
359   rw [Submodule.eq_top_iff_finrank_eq, local_orbit_schmidt_dimension, Module.finrank_pi,
360     Fintype.card_prod]
361   exact Nat.mul_left_cancel_iff (Fintype.card_pos (α := d))
362 
363 /-- Full local controllability of the state orbit iff the actual reduced state has full support. -/
364 theorem local_orbit_reduced_support [Nonempty d] (psi : d × m → ℂ) :
365     localOrbit psi = ⊤ ↔ LinearMap.range (reducedB psi).mulVecLin = ⊤ := by
366   rw [local_orbit_full_iff, reduced_full_support_iff]
367 
368 end KomorebiPaperVII.SeedOrbit
369 
370 /-! Complete declaration-level trust audit. -/
371 #print axioms KomorebiPaperVII.SeedOrbit.mem_orbit_iff
372 #print axioms KomorebiPaperVII.SeedOrbit.mem_orbit_iff_rows
373 #print axioms KomorebiPaperVII.SeedOrbit.row_dimension
374 #print axioms KomorebiPaperVII.SeedOrbit.orbit_dimension
375 #print axioms KomorebiPaperVII.SeedOrbit.orbit_span
376 #print axioms KomorebiPaperVII.SeedOrbit.span_orbit_dimension
377 #print axioms KomorebiPaperVII.SeedOrbit.cyclic_iff_full_rank
378 #print axioms KomorebiPaperVII.SeedOrbit.cyclic_multiplicity_bound
379 #print axioms KomorebiPaperVII.SeedOrbit.rowOrbit_mem
380 #print axioms KomorebiPaperVII.SeedOrbit.rowOrbit_dimension
381 #print axioms KomorebiPaperVII.SeedOrbit.rowOrbit_full
382 #print axioms KomorebiPaperVII.SeedOrbit.stacked_action
383 #print axioms KomorebiPaperVII.SeedOrbit.generates_iff_rowOrbit
384 #print axioms KomorebiPaperVII.SeedOrbit.generates_iff_rank
385 #print axioms KomorebiPaperVII.SeedOrbit.seed_count_lower
386 #print axioms KomorebiPaperVII.SeedOrbit.exists_full_column_rank
387 #print axioms KomorebiPaperVII.SeedOrbit.exists_generating_seeds_iff
388 #print axioms KomorebiPaperVII.SeedOrbit.block_generates_iff
389 #print axioms KomorebiPaperVII.SeedOrbit.exists_block_seeds_iff
390 #print axioms KomorebiPaperVII.SeedOrbit.seed_formula_le_iff
391 #print axioms KomorebiPaperVII.SeedOrbit.quantum_seed_rank
392 #print axioms KomorebiPaperVII.SeedOrbit.local_tensor_action
393 #print axioms KomorebiPaperVII.SeedOrbit.product_decomposition_rank_bound
394 #print axioms KomorebiPaperVII.SeedOrbit.product_decomposition_at_rank
395 #print axioms KomorebiPaperVII.SeedOrbit.product_length_minimum
396 #print axioms KomorebiPaperVII.SeedOrbit.schmidt_rank_eq_matrix_rank
397 #print axioms KomorebiPaperVII.SeedOrbit.local_orbit_is_tensor_span
398 #print axioms KomorebiPaperVII.SeedOrbit.local_orbit_schmidt_dimension
399 #print axioms KomorebiPaperVII.SeedOrbit.partial_trace_gram
400 #print axioms KomorebiPaperVII.SeedOrbit.reduced_rank_eq_schmidt
401 #print axioms KomorebiPaperVII.SeedOrbit.reduced_positive
402 #print axioms KomorebiPaperVII.SeedOrbit.reduced_full_support_iff
403 #print axioms KomorebiPaperVII.SeedOrbit.local_orbit_full_iff
404 #print axioms KomorebiPaperVII.SeedOrbit.local_orbit_reduced_support

Back to source controls