Imports
/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module
public import Physlib.StringTheory.FTheory.SU5.Fluxes.NoExotics.ChiralIndices
public import Physlib.StringTheory.FTheory.SU5.Fluxes.NoExotics.Elems
Completeness of Elems with regard to the NoExotics condition
i. Overview
In the module:
Physlib.StringTheory.FTheory.SU5.Fluxes.NoExotics.Elems
we define finite sets of elements of FluxesFive and FluxesTen which satisfy the
NoExotics and HasNoZero conditions.
In this module we prove that these sets are complete, in the sense that every
element of FluxesFive or FluxesTen which satisfies the NoExotics and
HasNoZero conditions is contained in them.
Our proof follows by building allowed subsets of fluxes by their cardinality, and heavily relies
on the decide tactic.
Note that the 10d fluxes are much more constrained than the 5-bar fluxes. This is because
they are constrained by 3 SM representations Q, U, and E, whereas the 5-bar fluxes
are only constrained by 2 SM representations D and L.
ii. Key results
FluxesFive.noExotics_iff_mem_elemsNoExotics : An element of FluxesFive satisfies NoExotics
and HasNoZero if and only if it is an element of elemsNoExotics.
FluxesTen.noExotics_iff_mem_elemsNoExotics : An element of FluxesTen satisfies NoExotics
and HasNoZero if and only if it is an element of elemsNoExotics.
iii. Table of contents
A. All terms of FluxesFive obeying NoExotics and HasNoZero
A.1. The allowed fluxes in a FluxesFive which obeys NoExotics and HasNoZero
A.2. Sufficient condition for a set to contain allowed subsets of card n.succ based on n
A.3. Statement of the allowed subsets of each cardinality
A.4. Lemma that stated allowed subsets are complete
A.5. Terms of FluxesFive obeying NoExotics and HasNoZero have card ≤ 6
A.6. Terms of FluxesFive obeying NoExotics and HasNoZero are in elemsNoExotics
A.7. Terms of FluxesFive obey NoExotics and HasNoZero if and only if in elemsNoExotics
B. All terms of FluxesTen obeying NoExotics and HasNoZero
B.1. The allowed fluxes in a FluxesTen which obeys NoExotics and HasNoZero
B.2. Sufficient condition for a set to contain allowed subsets of card n.succ based on n
B.3. Statement of the allowed subsets of each cardinality
B.4. Lemma that stated allowed subsets are complete
B.5. Terms of FluxesTen obeying NoExotics and HasNoZero have card ≤ 3
B.6. Terms of FluxesTen obeying NoExotics and HasNoZero are in elemsNoExotics
B.7. Terms of FluxesTen obey NoExotics and HasNoZero if and only if in elemsNoExotics
iv. References
There are no known references for the material in this module.
@[expose] public section
A. All terms of FluxesFive obeying NoExotics and HasNoZero
A.1. The allowed fluxes in a FluxesFive which obeys NoExotics and HasNoZero
F:FluxesFivehF:F.NoExoticshnZ:F.HasNoZerox:Fluxeshx:x ∈ FhL1:x.M + x.N ∈ {0, 1, 2, 3}hD1:x.M ∈ {0, 1, 2, 3}h0:¬x = 0hd:x.N = x.M + x.N - x.M⊢ x = { M := 0, N := 1 } ∨
x = { M := 0, N := 2 } ∨
x = { M := 0, N := 3 } ∨
x = { M := 1, N := -1 } ∨
x = { M := 1, N := 0 } ∨
x = { M := 1, N := 1 } ∨
x = { M := 1, N := 2 } ∨
x = { M := 2, N := -2 } ∨
x = { M := 2, N := -1 } ∨
x = { M := 2, N := 0 } ∨
x = { M := 2, N := 1 } ∨
x = { M := 3, N := -3 } ∨
x = { M := 3, N := -2 } ∨ x = { M := 3, N := -1 } ∨ x = { M := 3, N := 0 }
F:FluxesFivehF:F.NoExoticshnZ:F.HasNoZerox:Fluxeshx:x ∈ FhD1:x.M ∈ {0, 1, 2, 3}h0:¬x = 0D':ℤhL1:D' ∈ {0, 1, 2, 3}hd:x.N = D' - x.M⊢ x = { M := 0, N := 1 } ∨
x = { M := 0, N := 2 } ∨
x = { M := 0, N := 3 } ∨
x = { M := 1, N := -1 } ∨
x = { M := 1, N := 0 } ∨
x = { M := 1, N := 1 } ∨
x = { M := 1, N := 2 } ∨
x = { M := 2, N := -2 } ∨
x = { M := 2, N := -1 } ∨
x = { M := 2, N := 0 } ∨
x = { M := 2, N := 1 } ∨
x = { M := 3, N := -3 } ∨
x = { M := 3, N := -2 } ∨ x = { M := 3, N := -1 } ∨ x = { M := 3, N := 0 }
F:FluxesFivehF:F.NoExoticshnZ:F.HasNoZeroD':ℤhL1:D' ∈ {0, 1, 2, 3}M:ℤN:ℤhx:{ M := M, N := N } ∈ FhD1:{ M := M, N := N }.M ∈ {0, 1, 2, 3}h0:¬{ M := M, N := N } = 0hd:{ M := M, N := N }.N = D' - { M := M, N := N }.M⊢ { M := M, N := N } = { M := 0, N := 1 } ∨
{ M := M, N := N } = { M := 0, N := 2 } ∨
{ M := M, N := N } = { M := 0, N := 3 } ∨
{ M := M, N := N } = { M := 1, N := -1 } ∨
{ M := M, N := N } = { M := 1, N := 0 } ∨
{ M := M, N := N } = { M := 1, N := 1 } ∨
{ M := M, N := N } = { M := 1, N := 2 } ∨
{ M := M, N := N } = { M := 2, N := -2 } ∨
{ M := M, N := N } = { M := 2, N := -1 } ∨
{ M := M, N := N } = { M := 2, N := 0 } ∨
{ M := M, N := N } = { M := 2, N := 1 } ∨
{ M := M, N := N } = { M := 3, N := -3 } ∨
{ M := M, N := N } = { M := 3, N := -2 } ∨
{ M := M, N := N } = { M := 3, N := -1 } ∨ { M := M, N := N } = { M := 3, N := 0 }
F:FluxesFivehF:F.NoExoticshnZ:F.HasNoZeroD':ℤhL1:D' ∈ {0, 1, 2, 3}M:ℤN:ℤhx:{ M := M, N := D' - M } ∈ FhD1:M ∈ {0, 1, 2, 3}h0:¬{ M := M, N := D' - M } = 0hd:N = D' - M⊢ M = 0 ∧ D' - M = 1 ∨
M = 0 ∧ D' - M = 2 ∨
M = 0 ∧ D' - M = 3 ∨
M = 1 ∧ D' - M = -1 ∨
M = 1 ∧ D' - M = 0 ∨
M = 1 ∧ D' - M = 1 ∨
M = 1 ∧ D' - M = 2 ∨
M = 2 ∧ D' - M = -2 ∨
M = 2 ∧ D' - M = -1 ∨
M = 2 ∧ D' - M = 0 ∨
M = 2 ∧ D' - M = 1 ∨
M = 3 ∧ D' - M = -3 ∨ M = 3 ∧ D' - M = -2 ∨ M = 3 ∧ D' - M = -1 ∨ M = 3 ∧ D' - M = 0
F:FluxesFivehF:F.NoExoticshnZ:F.HasNoZeroD':ℤhL1:D' ∈ {0, 1, 2, 3}M:ℤhx:{ M := M, N := D' - M } ∈ FhD1:M ∈ {0, 1, 2, 3}h0:¬{ M := M, N := D' - M } = 0⊢ M = 0 ∧ D' - M = 1 ∨
M = 0 ∧ D' - M = 2 ∨
M = 0 ∧ D' - M = 3 ∨
M = 1 ∧ D' - M = -1 ∨
M = 1 ∧ D' - M = 0 ∨
M = 1 ∧ D' - M = 1 ∨
M = 1 ∧ D' - M = 2 ∨
M = 2 ∧ D' - M = -2 ∨
M = 2 ∧ D' - M = -1 ∨
M = 2 ∧ D' - M = 0 ∨
M = 2 ∧ D' - M = 1 ∨
M = 3 ∧ D' - M = -3 ∨ M = 3 ∧ D' - M = -2 ∨ M = 3 ∧ D' - M = -1 ∨ M = 3 ∧ D' - M = 0
F:FluxesFivehF:F.NoExoticshnZ:F.HasNoZeroD':ℤhL1:D' ∈ {0, 1, 2, 3}M:ℤhD1:M ∈ {0, 1, 2, 3}h0:¬{ M := M, N := D' - M } = 0⊢ M = 0 ∧ D' - M = 1 ∨
M = 0 ∧ D' - M = 2 ∨
M = 0 ∧ D' - M = 3 ∨
M = 1 ∧ D' - M = -1 ∨
M = 1 ∧ D' - M = 0 ∨
M = 1 ∧ D' - M = 1 ∨
M = 1 ∧ D' - M = 2 ∨
M = 2 ∧ D' - M = -2 ∨
M = 2 ∧ D' - M = -1 ∨
M = 2 ∧ D' - M = 0 ∨
M = 2 ∧ D' - M = 1 ∨
M = 3 ∧ D' - M = -3 ∨ M = 3 ∧ D' - M = -2 ∨ M = 3 ∧ D' - M = -1 ∨ M = 3 ∧ D' - M = 0
F:FluxesFivehF:F.NoExoticshnZ:F.HasNoZeroD':ℤhL1:D' ∈ {0, 1, 2, 3}M:ℤhD1:M ∈ {0, 1, 2, 3}⊢ ¬{ M := M, N := D' - M } = 0 →
M = 0 ∧ D' - M = 1 ∨
M = 0 ∧ D' - M = 2 ∨
M = 0 ∧ D' - M = 3 ∨
M = 1 ∧ D' - M = -1 ∨
M = 1 ∧ D' - M = 0 ∨
M = 1 ∧ D' - M = 1 ∨
M = 1 ∧ D' - M = 2 ∨
M = 2 ∧ D' - M = -2 ∨
M = 2 ∧ D' - M = -1 ∨
M = 2 ∧ D' - M = 0 ∨
M = 2 ∧ D' - M = 1 ∨
M = 3 ∧ D' - M = -3 ∨ M = 3 ∧ D' - M = -2 ∨ M = 3 ∧ D' - M = -1 ∨ M = 3 ∧ D' - M = 0
F:FluxesFivehF:F.NoExoticshnZ:F.HasNoZero⊢ ∀ D' ∈ {0, 1, 2, 3},
∀ M ∈ {0, 1, 2, 3},
¬{ M := M, N := D' - M } = 0 →
M = 0 ∧ D' - M = 1 ∨
M = 0 ∧ D' - M = 2 ∨
M = 0 ∧ D' - M = 3 ∨
M = 1 ∧ D' - M = -1 ∨
M = 1 ∧ D' - M = 0 ∨
M = 1 ∧ D' - M = 1 ∨
M = 1 ∧ D' - M = 2 ∨
M = 2 ∧ D' - M = -2 ∨
M = 2 ∧ D' - M = -1 ∨
M = 2 ∧ D' - M = 0 ∨
M = 2 ∧ D' - M = 1 ∨
M = 3 ∧ D' - M = -3 ∨ M = 3 ∧ D' - M = -2 ∨ M = 3 ∧ D' - M = -1 ∨ M = 3 ∧ D' - M = 0
All goals completed! 🐙
A.2. Sufficient condition for a set to contain allowed subsets of card n.succ based on n
n:ℕF:FluxesFivehF:F.NoExoticshnZ:F.HasNoZeroY:Finset (Multiset Fluxes)X:Finset (Multiset Fluxes)hY:∀ (S : Multiset Fluxes), S.card = n → S ≤ F → S ∈ YhX:∀
a ∈
{{ M := 0, N := 1 }, { M := 0, N := 2 }, { M := 0, N := 3 }, { M := 1, N := -1 }, { M := 1, N := 0 },
{ M := 1, N := 1 }, { M := 1, N := 2 }, { M := 2, N := -2 }, { M := 2, N := -1 }, { M := 2, N := 0 },
{ M := 2, N := 1 }, { M := 3, N := -3 }, { M := 3, N := -2 }, { M := 3, N := -1 }, { M := 3, N := 0 }},
∀ y ∈ Y,
(Multiset.map (fun x => x.M + x.N) (a ::ₘ y)).sum ≤ 3 →
(Multiset.map (fun x => x.M) (a ::ₘ y)).sum ≤ 3 → a ::ₘ y ∈ Xa:FluxesS:Multiset Fluxesih:S.card = n.succ →
S ≤ F → (Multiset.map (fun x => x.M + x.N) S).sum ≤ 3 → (Multiset.map (fun x => x.M) S).sum ≤ 3 → S ∈ Xhcard:S.card + 1 = n.succhle:a ::ₘ S ≤ Fhsum1:(Multiset.map (fun x => x.M + x.N) (a ::ₘ S)).sum ≤ 3hsum2:(Multiset.map (fun x => x.M) (a ::ₘ S)).sum ≤ 3hsub:S ≤ Fha:a ∈ F⊢ a ::ₘ S ∈ X
n:ℕF:FluxesFivehF:F.NoExoticshnZ:F.HasNoZeroY:Finset (Multiset Fluxes)X:Finset (Multiset Fluxes)hY:∀ (S : Multiset Fluxes), S.card = n → S ≤ F → S ∈ YhX:∀
a ∈
{{ M := 0, N := 1 }, { M := 0, N := 2 }, { M := 0, N := 3 }, { M := 1, N := -1 }, { M := 1, N := 0 },
{ M := 1, N := 1 }, { M := 1, N := 2 }, { M := 2, N := -2 }, { M := 2, N := -1 }, { M := 2, N := 0 },
{ M := 2, N := 1 }, { M := 3, N := -3 }, { M := 3, N := -2 }, { M := 3, N := -1 }, { M := 3, N := 0 }},
∀ y ∈ Y,
(Multiset.map (fun x => x.M + x.N) (a ::ₘ y)).sum ≤ 3 →
(Multiset.map (fun x => x.M) (a ::ₘ y)).sum ≤ 3 → a ::ₘ y ∈ Xa:FluxesS:Multiset Fluxesih:S.card = n.succ →
S ≤ F → (Multiset.map (fun x => x.M + x.N) S).sum ≤ 3 → (Multiset.map (fun x => x.M) S).sum ≤ 3 → S ∈ Xhle:a ::ₘ S ≤ Fhsum1:(Multiset.map (fun x => x.M + x.N) (a ::ₘ S)).sum ≤ 3hsum2:(Multiset.map (fun x => x.M) (a ::ₘ S)).sum ≤ 3hsub:S ≤ Fha:a ∈ Fhcard:S.card = n⊢ a ::ₘ S ∈ X
All goals completed! 🐙A.3. Statement of the allowed subsets of each cardinality
The allowed subsets of a FluxesFive which has no exotics or zeros.
def noExoticsSubsets : (n : ℕ) → Finset (Multiset Fluxes)
| 0 => {{}}
| 1 => {{⟨0, 1⟩}, {⟨0, 2⟩}, {⟨0, 3⟩}, {⟨1, -1⟩}, {⟨1, 0⟩}, {⟨1, 1⟩}, {⟨1, 2⟩},
{⟨2, -2⟩}, {⟨2, -1⟩}, {⟨2, 0⟩}, {⟨2, 1⟩}, {⟨3, -3⟩}, {⟨3, -2⟩}, {⟨3, -1⟩}, {⟨3, 0⟩}}
| 2 => {{⟨0, 1⟩, ⟨0, 1⟩}, {⟨0, 1⟩, ⟨1, -1⟩}, {⟨0, 1⟩, ⟨1, 0⟩}, {⟨0, 1⟩, ⟨0, 2⟩},
{⟨0, 1⟩, ⟨1, 1⟩}, {⟨0, 1⟩, ⟨2, -2⟩}, {⟨0, 1⟩, ⟨2, -1⟩}, {⟨0, 1⟩, ⟨2, 0⟩},
{⟨0, 1⟩, ⟨3, -3⟩}, {⟨0, 1⟩, ⟨3, -2⟩}, {⟨0, 1⟩, ⟨3, -1⟩},
{⟨0, 2⟩, ⟨1, -1⟩}, {⟨0, 2⟩, ⟨1, 0⟩}, {⟨0, 2⟩, ⟨2, -2⟩}, {⟨0, 2⟩, ⟨2, -1⟩},
{⟨0, 2⟩, ⟨3, -3⟩}, {⟨0, 2⟩, ⟨3, -2⟩}, {⟨0, 3⟩, ⟨1, -1⟩}, {⟨0, 3⟩, ⟨2, -2⟩},
{⟨0, 3⟩, ⟨3, -3⟩}, {⟨1, -1⟩, ⟨1, -1⟩}, {⟨1, -1⟩, ⟨1, 0⟩}, {⟨1, -1⟩, ⟨1, 1⟩},
{⟨1, -1⟩, ⟨1, 2⟩}, {⟨1, -1⟩, ⟨2, -2⟩}, {⟨1, -1⟩, ⟨2, -1⟩}, {⟨1, -1⟩, ⟨2, 0⟩},
{⟨1, 0⟩, ⟨1, 0⟩}, {⟨1, -1⟩, ⟨2, 1⟩}, {⟨1, 0⟩, ⟨1, 1⟩}, {⟨1, 0⟩, ⟨2, -2⟩},
{⟨1, 0⟩, ⟨2, -1⟩}, {⟨1, 0⟩, ⟨2, 0⟩}, {⟨1, 1⟩, ⟨2, -2⟩}, {⟨1, 1⟩, ⟨2, -1⟩},
{⟨1, 2⟩, ⟨2, -2⟩}}
| 3 => {{⟨0, 1⟩, ⟨0, 1⟩, ⟨0, 1⟩}, {⟨0, 1⟩, ⟨0, 1⟩, ⟨1, -1⟩},
{⟨0, 1⟩, ⟨0, 1⟩, ⟨1, 0⟩}, {⟨0, 1⟩, ⟨0, 1⟩, ⟨2, -2⟩},
{⟨0, 1⟩, ⟨0, 1⟩, ⟨2, -1⟩}, {⟨0, 1⟩, ⟨0, 1⟩, ⟨3, -3⟩}, {⟨0, 1⟩, ⟨0, 1⟩, ⟨3, -2⟩},
{⟨0, 1⟩, ⟨0, 2⟩, ⟨1, -1⟩}, {⟨0, 1⟩, ⟨0, 2⟩, ⟨2, -2⟩}, {⟨0, 1⟩, ⟨0, 2⟩, ⟨3, -3⟩},
{⟨0, 1⟩, ⟨1, -1⟩, ⟨1, -1⟩}, {⟨0, 1⟩, ⟨1, -1⟩, ⟨1, 0⟩}, {⟨0, 1⟩, ⟨1, -1⟩, ⟨1, 1⟩},
{⟨0, 1⟩, ⟨1, -1⟩, ⟨2, -2⟩}, {⟨0, 1⟩, ⟨1, -1⟩, ⟨2, -1⟩}, {⟨0, 1⟩, ⟨1, -1⟩, ⟨2, 0⟩},
{⟨0, 1⟩, ⟨1, 0⟩, ⟨1, 0⟩}, {⟨0, 1⟩, ⟨1, 0⟩, ⟨2, -2⟩}, {⟨0, 1⟩, ⟨1, 0⟩, ⟨2, -1⟩},
{⟨0, 1⟩, ⟨1, 1⟩, ⟨2, -2⟩}, {⟨0, 2⟩, ⟨1, -1⟩, ⟨1, -1⟩}, {⟨0, 2⟩, ⟨1, -1⟩, ⟨1, 0⟩},
{⟨0, 2⟩, ⟨1, -1⟩, ⟨2, -2⟩}, {⟨0, 2⟩, ⟨1, -1⟩, ⟨2, -1⟩}, {⟨0, 2⟩, ⟨1, 0⟩, ⟨2, -2⟩},
{⟨0, 3⟩, ⟨1, -1⟩, ⟨1, -1⟩}, {⟨0, 3⟩, ⟨1, -1⟩, ⟨2, -2⟩}, {⟨1, -1⟩, ⟨1, -1⟩, ⟨1, -1⟩},
{⟨1, -1⟩, ⟨1, -1⟩, ⟨1, 0⟩}, {⟨1, -1⟩, ⟨1, -1⟩, ⟨1, 1⟩}, {⟨1, -1⟩, ⟨1, -1⟩, ⟨1, 2⟩},
{⟨1, -1⟩, ⟨1, 0⟩, ⟨1, 0⟩}, {⟨1, -1⟩, ⟨1, 0⟩, ⟨1, 1⟩}, {⟨1, 0⟩, ⟨1, 0⟩, ⟨1, 0⟩}}
| 4 => {{⟨0, 1⟩, ⟨0, 1⟩, ⟨0, 1⟩, ⟨1, -1⟩},
{⟨0, 1⟩, ⟨0, 1⟩, ⟨0, 1⟩, ⟨2, -2⟩}, {⟨0, 1⟩, ⟨0, 1⟩, ⟨0, 1⟩, ⟨3, -3⟩},
{⟨0, 1⟩, ⟨0, 1⟩, ⟨1, -1⟩, ⟨1, -1⟩}, {⟨0, 1⟩, ⟨0, 1⟩, ⟨1, -1⟩, ⟨1, 0⟩},
{⟨0, 1⟩, ⟨0, 1⟩, ⟨1, -1⟩, ⟨2, -2⟩}, {⟨0, 1⟩, ⟨0, 1⟩, ⟨1, -1⟩, ⟨2, -1⟩},
{⟨0, 1⟩, ⟨0, 1⟩, ⟨1, 0⟩, ⟨2, -2⟩}, {⟨0, 1⟩, ⟨0, 2⟩, ⟨1, -1⟩, ⟨1, -1⟩},
{⟨0, 1⟩, ⟨0, 2⟩, ⟨1, -1⟩, ⟨2, -2⟩}, {⟨0, 1⟩, ⟨1, -1⟩, ⟨1, -1⟩, ⟨1, -1⟩},
{⟨0, 1⟩, ⟨1, -1⟩, ⟨1, -1⟩, ⟨1, 0⟩}, {⟨0, 1⟩, ⟨1, -1⟩, ⟨1, -1⟩, ⟨1, 1⟩},
{⟨0, 1⟩, ⟨1, -1⟩, ⟨1, 0⟩, ⟨1, 0⟩}, {⟨0, 2⟩, ⟨1, -1⟩, ⟨1, -1⟩, ⟨1, -1⟩},
{⟨0, 2⟩, ⟨1, -1⟩, ⟨1, -1⟩, ⟨1, 0⟩}, {⟨0, 3⟩, ⟨1, -1⟩, ⟨1, -1⟩, ⟨1, -1⟩}}
| 5 => {{⟨0, 1⟩, ⟨0, 1⟩, ⟨0, 1⟩, ⟨1, -1⟩, ⟨1, -1⟩},
{⟨0, 1⟩, ⟨0, 1⟩, ⟨0, 1⟩, ⟨1, -1⟩, ⟨2, -2⟩},
{⟨0, 1⟩, ⟨0, 1⟩, ⟨1, -1⟩, ⟨1, -1⟩, ⟨1, -1⟩},
{⟨0, 1⟩, ⟨0, 1⟩, ⟨1, -1⟩, ⟨1, -1⟩, ⟨1, 0⟩},
{⟨0, 1⟩, ⟨0, 2⟩, ⟨1, -1⟩, ⟨1, -1⟩, ⟨1, -1⟩}}
| 6 => {{⟨0, 1⟩, ⟨0, 1⟩, ⟨0, 1⟩, ⟨1, -1⟩, ⟨1, -1⟩, ⟨1, -1⟩}}
| _ + 7 => ∅A.4. Lemma that stated allowed subsets are complete
F:FluxesFivehF:F.NoExoticshnZ:F.HasNoZeroS✝:Multiset FluxeshS✝:S✝ ≤ FS:Multiset Fluxeshcard:S = 0hS:S ≤ F⊢ S ∈ noExoticsSubsets 0
F:FluxesFivehF:F.NoExoticshnZ:F.HasNoZeroS:Multiset FluxeshS✝:S✝ ≤ FhS:0 ≤ F⊢ 0 ∈ noExoticsSubsets 0
All goals completed! 🐙
| 1, S, hcard, hS => subset_le_mem_of_card_eq_succ hF hnZ S hcard hS
(fun S hc => recS 0 S hc) <| F:FluxesFivehF:F.NoExoticshnZ:F.HasNoZeroS✝:Multiset FluxeshS✝:S✝ ≤ FS:Multiset Fluxeshcard:S.card = 1hS:S ≤ F⊢ ∀
a ∈
{{ M := 0, N := 1 }, { M := 0, N := 2 }, { M := 0, N := 3 }, { M := 1, N := -1 }, { M := 1, N := 0 },
{ M := 1, N := 1 }, { M := 1, N := 2 }, { M := 2, N := -2 }, { M := 2, N := -1 }, { M := 2, N := 0 },
{ M := 2, N := 1 }, { M := 3, N := -3 }, { M := 3, N := -2 }, { M := 3, N := -1 }, { M := 3, N := 0 }},
∀ y ∈ noExoticsSubsets 0,
(Multiset.map (fun x => x.M + x.N) (a ::ₘ y)).sum ≤ 3 →
(Multiset.map (fun x => x.M) (a ::ₘ y)).sum ≤ 3 → a ::ₘ y ∈ noExoticsSubsets 1 All goals completed! 🐙
| 2, S, hcard, hS => subset_le_mem_of_card_eq_succ hF hnZ S hcard hS
(fun S hc => recS 1 S hc) <| F:FluxesFivehF:F.NoExoticshnZ:F.HasNoZeroS✝:Multiset FluxeshS✝:S✝ ≤ FS:Multiset Fluxeshcard:S.card = 2hS:S ≤ F⊢ ∀
a ∈
{{ M := 0, N := 1 }, { M := 0, N := 2 }, { M := 0, N := 3 }, { M := 1, N := -1 }, { M := 1, N := 0 },
{ M := 1, N := 1 }, { M := 1, N := 2 }, { M := 2, N := -2 }, { M := 2, N := -1 }, { M := 2, N := 0 },
{ M := 2, N := 1 }, { M := 3, N := -3 }, { M := 3, N := -2 }, { M := 3, N := -1 }, { M := 3, N := 0 }},
∀ y ∈ noExoticsSubsets 1,
(Multiset.map (fun x => x.M + x.N) (a ::ₘ y)).sum ≤ 3 →
(Multiset.map (fun x => x.M) (a ::ₘ y)).sum ≤ 3 → a ::ₘ y ∈ noExoticsSubsets 2 All goals completed! 🐙
| 3, S, hcard, hS => subset_le_mem_of_card_eq_succ hF hnZ S hcard hS
(fun S hc => recS 2 S hc) <| F:FluxesFivehF:F.NoExoticshnZ:F.HasNoZeroS✝:Multiset FluxeshS✝:S✝ ≤ FS:Multiset Fluxeshcard:S.card = 3hS:S ≤ F⊢ ∀
a ∈
{{ M := 0, N := 1 }, { M := 0, N := 2 }, { M := 0, N := 3 }, { M := 1, N := -1 }, { M := 1, N := 0 },
{ M := 1, N := 1 }, { M := 1, N := 2 }, { M := 2, N := -2 }, { M := 2, N := -1 }, { M := 2, N := 0 },
{ M := 2, N := 1 }, { M := 3, N := -3 }, { M := 3, N := -2 }, { M := 3, N := -1 }, { M := 3, N := 0 }},
∀ y ∈ noExoticsSubsets 2,
(Multiset.map (fun x => x.M + x.N) (a ::ₘ y)).sum ≤ 3 →
(Multiset.map (fun x => x.M) (a ::ₘ y)).sum ≤ 3 → a ::ₘ y ∈ noExoticsSubsets 3 All goals completed! 🐙
| 4, S, hcard, hS => subset_le_mem_of_card_eq_succ hF hnZ S hcard hS
(fun S hc => recS 3 S hc) <| F:FluxesFivehF:F.NoExoticshnZ:F.HasNoZeroS✝:Multiset FluxeshS✝:S✝ ≤ FS:Multiset Fluxeshcard:S.card = 4hS:S ≤ F⊢ ∀
a ∈
{{ M := 0, N := 1 }, { M := 0, N := 2 }, { M := 0, N := 3 }, { M := 1, N := -1 }, { M := 1, N := 0 },
{ M := 1, N := 1 }, { M := 1, N := 2 }, { M := 2, N := -2 }, { M := 2, N := -1 }, { M := 2, N := 0 },
{ M := 2, N := 1 }, { M := 3, N := -3 }, { M := 3, N := -2 }, { M := 3, N := -1 }, { M := 3, N := 0 }},
∀ y ∈ noExoticsSubsets 3,
(Multiset.map (fun x => x.M + x.N) (a ::ₘ y)).sum ≤ 3 →
(Multiset.map (fun x => x.M) (a ::ₘ y)).sum ≤ 3 → a ::ₘ y ∈ noExoticsSubsets 4 All goals completed! 🐙
| 5, S, hcard, hS => subset_le_mem_of_card_eq_succ hF hnZ S hcard hS
(fun S hc => recS 4 S hc) <| F:FluxesFivehF:F.NoExoticshnZ:F.HasNoZeroS✝:Multiset FluxeshS✝:S✝ ≤ FS:Multiset Fluxeshcard:S.card = 5hS:S ≤ F⊢ ∀
a ∈
{{ M := 0, N := 1 }, { M := 0, N := 2 }, { M := 0, N := 3 }, { M := 1, N := -1 }, { M := 1, N := 0 },
{ M := 1, N := 1 }, { M := 1, N := 2 }, { M := 2, N := -2 }, { M := 2, N := -1 }, { M := 2, N := 0 },
{ M := 2, N := 1 }, { M := 3, N := -3 }, { M := 3, N := -2 }, { M := 3, N := -1 }, { M := 3, N := 0 }},
∀ y ∈ noExoticsSubsets 4,
(Multiset.map (fun x => x.M + x.N) (a ::ₘ y)).sum ≤ 3 →
(Multiset.map (fun x => x.M) (a ::ₘ y)).sum ≤ 3 → a ::ₘ y ∈ noExoticsSubsets 5 All goals completed! 🐙
| 6, S, hcard, hS => subset_le_mem_of_card_eq_succ hF hnZ S hcard hS
(fun S hc => recS 5 S hc) <| F:FluxesFivehF:F.NoExoticshnZ:F.HasNoZeroS✝:Multiset FluxeshS✝:S✝ ≤ FS:Multiset Fluxeshcard:S.card = 6hS:S ≤ F⊢ ∀
a ∈
{{ M := 0, N := 1 }, { M := 0, N := 2 }, { M := 0, N := 3 }, { M := 1, N := -1 }, { M := 1, N := 0 },
{ M := 1, N := 1 }, { M := 1, N := 2 }, { M := 2, N := -2 }, { M := 2, N := -1 }, { M := 2, N := 0 },
{ M := 2, N := 1 }, { M := 3, N := -3 }, { M := 3, N := -2 }, { M := 3, N := -1 }, { M := 3, N := 0 }},
∀ y ∈ noExoticsSubsets 5,
(Multiset.map (fun x => x.M + x.N) (a ::ₘ y)).sum ≤ 3 →
(Multiset.map (fun x => x.M) (a ::ₘ y)).sum ≤ 3 → a ::ₘ y ∈ noExoticsSubsets 6 All goals completed! 🐙
| 7, S, hcard, hS => subset_le_mem_of_card_eq_succ hF hnZ S hcard hS
(fun S hc => recS 6 S hc) <| F:FluxesFivehF:F.NoExoticshnZ:F.HasNoZeroS✝:Multiset FluxeshS✝:S✝ ≤ FS:Multiset Fluxeshcard:S.card = 7hS:S ≤ F⊢ ∀
a ∈
{{ M := 0, N := 1 }, { M := 0, N := 2 }, { M := 0, N := 3 }, { M := 1, N := -1 }, { M := 1, N := 0 },
{ M := 1, N := 1 }, { M := 1, N := 2 }, { M := 2, N := -2 }, { M := 2, N := -1 }, { M := 2, N := 0 },
{ M := 2, N := 1 }, { M := 3, N := -3 }, { M := 3, N := -2 }, { M := 3, N := -1 }, { M := 3, N := 0 }},
∀ y ∈ noExoticsSubsets 6,
(Multiset.map (fun x => x.M + x.N) (a ::ₘ y)).sum ≤ 3 →
(Multiset.map (fun x => x.M) (a ::ₘ y)).sum ≤ 3 → a ::ₘ y ∈ noExoticsSubsets 7 All goals completed! 🐙
| (n + 1) + 7, S, hcard, hS => subset_le_mem_of_card_eq_succ hF hnZ S hcard hS
(fun S hc => recS (n + 7) S hc) <| F:FluxesFivehF:F.NoExoticshnZ:F.HasNoZeroS✝:Multiset FluxeshS✝:S✝ ≤ Fn:ℕS:Multiset Fluxeshcard:S.card = n + 1 + 7hS:S ≤ F⊢ ∀
a ∈
{{ M := 0, N := 1 }, { M := 0, N := 2 }, { M := 0, N := 3 }, { M := 1, N := -1 }, { M := 1, N := 0 },
{ M := 1, N := 1 }, { M := 1, N := 2 }, { M := 2, N := -2 }, { M := 2, N := -1 }, { M := 2, N := 0 },
{ M := 2, N := 1 }, { M := 3, N := -3 }, { M := 3, N := -2 }, { M := 3, N := -1 }, { M := 3, N := 0 }},
∀ y ∈ noExoticsSubsets (n + 7),
(Multiset.map (fun x => x.M + x.N) (a ::ₘ y)).sum ≤ 3 →
(Multiset.map (fun x => x.M) (a ::ₘ y)).sum ≤ 3 → a ::ₘ y ∈ noExoticsSubsets (n + 1 + 7)
All goals completed! 🐙
A.5. Terms of FluxesFive obeying NoExotics and HasNoZero have card ≤ 6
lemma card_le_six_of_noExotics {F : FluxesFive} (hF : F.NoExotics) (hnZ : F.HasNoZero) :
F.card ≤ 6 := F:FluxesFivehF:F.NoExoticshnZ:F.HasNoZero⊢ Multiset.card F ≤ 6
F:FluxesFivehF:F.NoExoticshnZ:F.HasNoZerohx:F ∈ noExoticsSubsets (Multiset.card F)⊢ Multiset.card F ≤ 6
F:FluxesFivehF:F.NoExoticshnZ:F.HasNoZeron:ℕhx:F ∈ noExoticsSubsets n⊢ n ≤ 6
match n with
F:FluxesFivehF:F.NoExoticshnZ:F.HasNoZeron:ℕhx:F ∈ noExoticsSubsets 0⊢ 0 ≤ 6 All goals completed! 🐙
F:FluxesFivehF:F.NoExoticshnZ:F.HasNoZeron:ℕhx:F ∈ noExoticsSubsets 1⊢ 1 ≤ 6 All goals completed! 🐙
F:FluxesFivehF:F.NoExoticshnZ:F.HasNoZeron:ℕhx:F ∈ noExoticsSubsets 2⊢ 2 ≤ 6 All goals completed! 🐙
F:FluxesFivehF:F.NoExoticshnZ:F.HasNoZeron:ℕhx:F ∈ noExoticsSubsets 3⊢ 3 ≤ 6 All goals completed! 🐙
F:FluxesFivehF:F.NoExoticshnZ:F.HasNoZeron:ℕhx:F ∈ noExoticsSubsets 4⊢ 4 ≤ 6 All goals completed! 🐙
F:FluxesFivehF:F.NoExoticshnZ:F.HasNoZeron:ℕhx:F ∈ noExoticsSubsets 5⊢ 5 ≤ 6 All goals completed! 🐙
F:FluxesFivehF:F.NoExoticshnZ:F.HasNoZeron:ℕhx:F ∈ noExoticsSubsets 6⊢ 6 ≤ 6 All goals completed! 🐙
F:FluxesFivehF:F.NoExoticshnZ:F.HasNoZeron:ℕn✝:ℕhx:F ∈ noExoticsSubsets (n✝ + 7)⊢ n✝ + 7 ≤ 6 All goals completed! 🐙F:FluxesFivehF:F.NoExoticshnZ:F.HasNoZero⊢ Multiset.card F ≤ 6
All goals completed! 🐙
A.6. Terms of FluxesFive obeying NoExotics and HasNoZero are in elemsNoExotics
F:FluxesFivehNE:F.NoExoticshnZ:F.HasNoZerohF:F ∈ noExoticsSubsets 0hr:Multiset.card F = 0⊢ F ∈ elemsNoExotics
F:FluxesFivehNE:F.NoExoticshF:F ∈ noExoticsSubsets 0⊢ F ∈ elemsNoExotics
F:FluxesFivehF:F ∈ noExoticsSubsets 0⊢ F.NoExotics → F ∈ elemsNoExotics
⊢ ∀ F ∈ noExoticsSubsets 0, F.NoExotics → F ∈ elemsNoExotics
All goals completed! 🐙
A.7. Terms of FluxesFive obey NoExotics and HasNoZero if and only if in elemsNoExotics
Completeness of elemsNoExotics, that is, every element of FluxesFive
which obeys NoExotics is an element of elemsNoExotics, and every
element of elemsNoExotics obeys NoExotics.
lemma noExotics_iff_mem_elemsNoExotics (F : FluxesFive) :
F.NoExotics ∧ F.HasNoZero ↔ F ∈ elemsNoExotics := F:FluxesFive⊢ F.NoExotics ∧ F.HasNoZero ↔ F ∈ elemsNoExotics
F:FluxesFive⊢ F.NoExotics ∧ F.HasNoZero → F ∈ elemsNoExoticsF:FluxesFive⊢ F ∈ elemsNoExotics → F.NoExotics ∧ F.HasNoZero
F:FluxesFive⊢ F.NoExotics ∧ F.HasNoZero → F ∈ elemsNoExotics All goals completed! 🐙
F:FluxesFive⊢ F ∈ elemsNoExotics → F.NoExotics ∧ F.HasNoZero All goals completed! 🐙
B. All terms of FluxesTen obeying NoExotics and HasNoZero
B.1. The allowed fluxes in a FluxesTen which obeys NoExotics and HasNoZero
F:FluxesTenhF:F.NoExoticshnZ:F.HasNoZeroM:ℤN:ℤhx:{ M := M, N := N } ∈ FhQ1:{ M := M, N := N }.M ∈ {0, 1, 2, 3}hU1:{ M := M, N := N }.M - { M := M, N := N }.N ∈ {0, 1, 2, 3}hE1:{ M := M, N := N }.M + { M := M, N := N }.N ∈ {0, 1, 2, 3}h0:¬{ M := M, N := N } = 0D:ℤ := M + Nhd:N = D - M⊢ { M := M, N := N } = { M := 1, N := -1 } ∨
{ M := M, N := N } = { M := 1, N := 0 } ∨
{ M := M, N := N } = { M := 1, N := 1 } ∨
{ M := M, N := N } = { M := 2, N := -1 } ∨
{ M := M, N := N } = { M := 2, N := 0 } ∨
{ M := M, N := N } = { M := 2, N := 1 } ∨ { M := M, N := N } = { M := 3, N := 0 }
F:FluxesTenhF:F.NoExoticshnZ:F.HasNoZeroM:ℤN:ℤhx:{ M := M, N := N } ∈ FhQ1:{ M := M, N := N }.M ∈ {0, 1, 2, 3}hU1:{ M := M, N := N }.M - { M := M, N := N }.N ∈ {0, 1, 2, 3}hE1:{ M := M, N := N }.M + { M := M, N := N }.N ∈ {0, 1, 2, 3}h0:¬{ M := M, N := N } = 0D:ℤ := M + ND':ℤhd:N = D' - M⊢ { M := M, N := N } = { M := 1, N := -1 } ∨
{ M := M, N := N } = { M := 1, N := 0 } ∨
{ M := M, N := N } = { M := 1, N := 1 } ∨
{ M := M, N := N } = { M := 2, N := -1 } ∨
{ M := M, N := N } = { M := 2, N := 0 } ∨
{ M := M, N := N } = { M := 2, N := 1 } ∨ { M := M, N := N } = { M := 3, N := 0 }
F:FluxesTenhF:F.NoExoticshnZ:F.HasNoZeroM:ℤD':ℤhx:{ M := M, N := D' - M } ∈ FhQ1:{ M := M, N := D' - M }.M ∈ {0, 1, 2, 3}hU1:{ M := M, N := D' - M }.M - { M := M, N := D' - M }.N ∈ {0, 1, 2, 3}hE1:{ M := M, N := D' - M }.M + { M := M, N := D' - M }.N ∈ {0, 1, 2, 3}h0:¬{ M := M, N := D' - M } = 0D:ℤ := M + (D' - M)⊢ { M := M, N := D' - M } = { M := 1, N := -1 } ∨
{ M := M, N := D' - M } = { M := 1, N := 0 } ∨
{ M := M, N := D' - M } = { M := 1, N := 1 } ∨
{ M := M, N := D' - M } = { M := 2, N := -1 } ∨
{ M := M, N := D' - M } = { M := 2, N := 0 } ∨
{ M := M, N := D' - M } = { M := 2, N := 1 } ∨ { M := M, N := D' - M } = { M := 3, N := 0 }
F:FluxesTenhF:F.NoExoticshnZ:F.HasNoZeroM:ℤD':ℤhx:{ M := M, N := D' - M } ∈ FhQ1:{ M := M, N := D' - M }.M ∈ {0, 1, 2, 3}hU1:{ M := M, N := D' - M }.M - { M := M, N := D' - M }.N ∈ {0, 1, 2, 3}h0:¬{ M := M, N := D' - M } = 0D:ℤ := M + (D' - M)hE1:D' ∈ {0, 1, 2, 3}⊢ { M := M, N := D' - M } = { M := 1, N := -1 } ∨
{ M := M, N := D' - M } = { M := 1, N := 0 } ∨
{ M := M, N := D' - M } = { M := 1, N := 1 } ∨
{ M := M, N := D' - M } = { M := 2, N := -1 } ∨
{ M := M, N := D' - M } = { M := 2, N := 0 } ∨
{ M := M, N := D' - M } = { M := 2, N := 1 } ∨ { M := M, N := D' - M } = { M := 3, N := 0 }
F:FluxesTenhF:F.NoExoticshnZ:F.HasNoZeroM:ℤD':ℤhx:{ M := M, N := D' - M } ∈ FD:ℤ := M + (D' - M)hQ1:M ∈ {0, 1, 2, 3}hU1:M - (D' - M) ∈ {0, 1, 2, 3}h0:¬{ M := M, N := D' - M } = 0hE1:D' ∈ {0, 1, 2, 3}⊢ M = 1 ∧ D' - M = -1 ∨
M = 1 ∧ D' - M = 0 ∨
M = 1 ∧ D' - M = 1 ∨ M = 2 ∧ D' - M = -1 ∨ M = 2 ∧ D' - M = 0 ∨ M = 2 ∧ D' - M = 1 ∨ M = 3 ∧ D' - M = 0
F:FluxesTenhF:F.NoExoticshnZ:F.HasNoZeroM:ℤD':ℤhQ1:M ∈ {0, 1, 2, 3}hU1:M - (D' - M) ∈ {0, 1, 2, 3}h0:¬{ M := M, N := D' - M } = 0hE1:D' ∈ {0, 1, 2, 3}⊢ M = 1 ∧ D' - M = -1 ∨
M = 1 ∧ D' - M = 0 ∨
M = 1 ∧ D' - M = 1 ∨ M = 2 ∧ D' - M = -1 ∨ M = 2 ∧ D' - M = 0 ∨ M = 2 ∧ D' - M = 1 ∨ M = 3 ∧ D' - M = 0
F:FluxesTenhF:F.NoExoticshnZ:F.HasNoZeroM:ℤD':ℤhQ1:M ∈ {0, 1, 2, 3}hE1:D' ∈ {0, 1, 2, 3}⊢ M - (D' - M) ∈ {0, 1, 2, 3} →
¬{ M := M, N := D' - M } = 0 →
M = 1 ∧ D' - M = -1 ∨
M = 1 ∧ D' - M = 0 ∨
M = 1 ∧ D' - M = 1 ∨ M = 2 ∧ D' - M = -1 ∨ M = 2 ∧ D' - M = 0 ∨ M = 2 ∧ D' - M = 1 ∨ M = 3 ∧ D' - M = 0
F:FluxesTenhF:F.NoExoticshnZ:F.HasNoZeroM:ℤhQ1:M ∈ {0, 1, 2, 3}⊢ ∀ D' ∈ {0, 1, 2, 3},
M - (D' - M) ∈ {0, 1, 2, 3} →
¬{ M := M, N := D' - M } = 0 →
M = 1 ∧ D' - M = -1 ∨
M = 1 ∧ D' - M = 0 ∨
M = 1 ∧ D' - M = 1 ∨ M = 2 ∧ D' - M = -1 ∨ M = 2 ∧ D' - M = 0 ∨ M = 2 ∧ D' - M = 1 ∨ M = 3 ∧ D' - M = 0
F:FluxesTenhF:F.NoExoticshnZ:F.HasNoZero⊢ ∀ M ∈ {0, 1, 2, 3},
∀ D' ∈ {0, 1, 2, 3},
M - (D' - M) ∈ {0, 1, 2, 3} →
¬{ M := M, N := D' - M } = 0 →
M = 1 ∧ D' - M = -1 ∨
M = 1 ∧ D' - M = 0 ∨
M = 1 ∧ D' - M = 1 ∨ M = 2 ∧ D' - M = -1 ∨ M = 2 ∧ D' - M = 0 ∨ M = 2 ∧ D' - M = 1 ∨ M = 3 ∧ D' - M = 0
All goals completed! 🐙
B.2. Sufficient condition for a set to contain allowed subsets of card n.succ based on n
n:ℕF:FluxesTenhF:F.NoExoticshnZ:F.HasNoZeroY:Finset (Multiset Fluxes)X:Finset (Multiset Fluxes)hY:∀ (S : Multiset Fluxes), S.card = n → S ≤ F → S ∈ YhX:∀
a ∈
{{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 1, N := 1 }, { M := 2, N := -1 }, { M := 2, N := 0 },
{ M := 2, N := 1 }, { M := 3, N := 0 }},
∀ y ∈ Y,
(Multiset.map (fun x => x.M) (a ::ₘ y)).sum ≤ 3 →
(Multiset.map (fun x => x.M - x.N) (a ::ₘ y)).sum ≤ 3 →
(Multiset.map (fun x => x.M + x.N) (a ::ₘ y)).sum ≤ 3 → a ::ₘ y ∈ Xa:FluxesS:Multiset Fluxesih:S.card = n.succ →
S ≤ F →
(Multiset.map (fun x => x.M) S).sum ≤ 3 →
(Multiset.map (fun x => x.M - x.N) S).sum ≤ 3 → (Multiset.map (fun x => x.M + x.N) S).sum ≤ 3 → S ∈ Xhcard:S.card + 1 = n.succhle:a ::ₘ S ≤ Fhsum1:(Multiset.map (fun x => x.M) (a ::ₘ S)).sum ≤ 3hsum2:(Multiset.map (fun x => x.M - x.N) (a ::ₘ S)).sum ≤ 3hsum3:(Multiset.map (fun x => x.M + x.N) (a ::ₘ S)).sum ≤ 3hsub:S ≤ Fha:a ∈ F⊢ a ::ₘ S ∈ X
n:ℕF:FluxesTenhF:F.NoExoticshnZ:F.HasNoZeroY:Finset (Multiset Fluxes)X:Finset (Multiset Fluxes)hY:∀ (S : Multiset Fluxes), S.card = n → S ≤ F → S ∈ YhX:∀
a ∈
{{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 1, N := 1 }, { M := 2, N := -1 }, { M := 2, N := 0 },
{ M := 2, N := 1 }, { M := 3, N := 0 }},
∀ y ∈ Y,
(Multiset.map (fun x => x.M) (a ::ₘ y)).sum ≤ 3 →
(Multiset.map (fun x => x.M - x.N) (a ::ₘ y)).sum ≤ 3 →
(Multiset.map (fun x => x.M + x.N) (a ::ₘ y)).sum ≤ 3 → a ::ₘ y ∈ Xa:FluxesS:Multiset Fluxesih:S.card = n.succ →
S ≤ F →
(Multiset.map (fun x => x.M) S).sum ≤ 3 →
(Multiset.map (fun x => x.M - x.N) S).sum ≤ 3 → (Multiset.map (fun x => x.M + x.N) S).sum ≤ 3 → S ∈ Xhle:a ::ₘ S ≤ Fhsum1:(Multiset.map (fun x => x.M) (a ::ₘ S)).sum ≤ 3hsum2:(Multiset.map (fun x => x.M - x.N) (a ::ₘ S)).sum ≤ 3hsum3:(Multiset.map (fun x => x.M + x.N) (a ::ₘ S)).sum ≤ 3hsub:S ≤ Fha:a ∈ Fhcard:S.card = n⊢ a ::ₘ S ∈ X
All goals completed! 🐙B.3. Statement of the allowed subsets of each cardinality
The allowed subsets of a FluxesTen which has no exotics or zeros.
def noExoticsSubsets : (n : ℕ) → Finset (Multiset Fluxes)
| 0 => {{}}
| 1 => {{⟨1, -1⟩}, {⟨1, 0⟩}, {⟨1, 1⟩}, {⟨2, -1⟩}, {⟨2, 0⟩}, {⟨2, 1⟩}, {⟨3, 0⟩}}
| 2 => {{⟨1, -1⟩, ⟨1, 0⟩}, {⟨1, -1⟩, ⟨1, 1⟩}, {⟨1, -1⟩, ⟨2, 1⟩},
{⟨1, 0⟩, ⟨1, 0⟩}, {⟨1, 0⟩, ⟨1, 1⟩}, {⟨1, 0⟩, ⟨2, 0⟩}, {⟨1, 1⟩, ⟨2, -1⟩}}
| 3 => {{⟨1, -1⟩, ⟨1, 0⟩, ⟨1, 1⟩}, {⟨1, 0⟩, ⟨1, 0⟩, ⟨1, 0⟩}}
| _ + 4 => ∅B.4. Lemma that stated allowed subsets are complete
F:FluxesTenhF:F.NoExoticshnZ:F.HasNoZeroS✝:Multiset FluxeshS✝:S✝ ≤ FS:Multiset Fluxeshcard:S = 0hS:S ≤ F⊢ S ∈ noExoticsSubsets 0
F:FluxesTenhF:F.NoExoticshnZ:F.HasNoZeroS:Multiset FluxeshS✝:S✝ ≤ FhS:0 ≤ F⊢ 0 ∈ noExoticsSubsets 0
All goals completed! 🐙
| 1, S, hcard, hS => subset_le_mem_of_card_eq_succ hF hnZ S hcard hS
(fun S hc => recS 0 S hc) <| F:FluxesTenhF:F.NoExoticshnZ:F.HasNoZeroS✝:Multiset FluxeshS✝:S✝ ≤ FS:Multiset Fluxeshcard:S.card = 1hS:S ≤ F⊢ ∀
a ∈
{{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 1, N := 1 }, { M := 2, N := -1 }, { M := 2, N := 0 },
{ M := 2, N := 1 }, { M := 3, N := 0 }},
∀ y ∈ noExoticsSubsets 0,
(Multiset.map (fun x => x.M) (a ::ₘ y)).sum ≤ 3 →
(Multiset.map (fun x => x.M - x.N) (a ::ₘ y)).sum ≤ 3 →
(Multiset.map (fun x => x.M + x.N) (a ::ₘ y)).sum ≤ 3 → a ::ₘ y ∈ noExoticsSubsets 1 All goals completed! 🐙
| 2, S, hcard, hS => subset_le_mem_of_card_eq_succ hF hnZ S hcard hS
(fun S hc => recS 1 S hc) <| F:FluxesTenhF:F.NoExoticshnZ:F.HasNoZeroS✝:Multiset FluxeshS✝:S✝ ≤ FS:Multiset Fluxeshcard:S.card = 2hS:S ≤ F⊢ ∀
a ∈
{{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 1, N := 1 }, { M := 2, N := -1 }, { M := 2, N := 0 },
{ M := 2, N := 1 }, { M := 3, N := 0 }},
∀ y ∈ noExoticsSubsets 1,
(Multiset.map (fun x => x.M) (a ::ₘ y)).sum ≤ 3 →
(Multiset.map (fun x => x.M - x.N) (a ::ₘ y)).sum ≤ 3 →
(Multiset.map (fun x => x.M + x.N) (a ::ₘ y)).sum ≤ 3 → a ::ₘ y ∈ noExoticsSubsets 2 All goals completed! 🐙
| 3, S, hcard, hS => subset_le_mem_of_card_eq_succ hF hnZ S hcard hS
(fun S hc => recS 2 S hc) <| F:FluxesTenhF:F.NoExoticshnZ:F.HasNoZeroS✝:Multiset FluxeshS✝:S✝ ≤ FS:Multiset Fluxeshcard:S.card = 3hS:S ≤ F⊢ ∀
a ∈
{{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 1, N := 1 }, { M := 2, N := -1 }, { M := 2, N := 0 },
{ M := 2, N := 1 }, { M := 3, N := 0 }},
∀ y ∈ noExoticsSubsets 2,
(Multiset.map (fun x => x.M) (a ::ₘ y)).sum ≤ 3 →
(Multiset.map (fun x => x.M - x.N) (a ::ₘ y)).sum ≤ 3 →
(Multiset.map (fun x => x.M + x.N) (a ::ₘ y)).sum ≤ 3 → a ::ₘ y ∈ noExoticsSubsets 3 All goals completed! 🐙
| 4, S, hcard, hS => subset_le_mem_of_card_eq_succ hF hnZ S hcard hS
(fun S hc => recS 3 S hc) <| F:FluxesTenhF:F.NoExoticshnZ:F.HasNoZeroS✝:Multiset FluxeshS✝:S✝ ≤ FS:Multiset Fluxeshcard:S.card = 4hS:S ≤ F⊢ ∀
a ∈
{{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 1, N := 1 }, { M := 2, N := -1 }, { M := 2, N := 0 },
{ M := 2, N := 1 }, { M := 3, N := 0 }},
∀ y ∈ noExoticsSubsets 3,
(Multiset.map (fun x => x.M) (a ::ₘ y)).sum ≤ 3 →
(Multiset.map (fun x => x.M - x.N) (a ::ₘ y)).sum ≤ 3 →
(Multiset.map (fun x => x.M + x.N) (a ::ₘ y)).sum ≤ 3 → a ::ₘ y ∈ noExoticsSubsets 4 All goals completed! 🐙
| (n + 1) + 4, S, hcard, hS => subset_le_mem_of_card_eq_succ hF hnZ S hcard hS
(fun S hc => recS (n + 4) S hc) <| F:FluxesTenhF:F.NoExoticshnZ:F.HasNoZeroS✝:Multiset FluxeshS✝:S✝ ≤ Fn:ℕS:Multiset Fluxeshcard:S.card = n + 1 + 4hS:S ≤ F⊢ ∀
a ∈
{{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 1, N := 1 }, { M := 2, N := -1 }, { M := 2, N := 0 },
{ M := 2, N := 1 }, { M := 3, N := 0 }},
∀ y ∈ noExoticsSubsets (n + 4),
(Multiset.map (fun x => x.M) (a ::ₘ y)).sum ≤ 3 →
(Multiset.map (fun x => x.M - x.N) (a ::ₘ y)).sum ≤ 3 →
(Multiset.map (fun x => x.M + x.N) (a ::ₘ y)).sum ≤ 3 → a ::ₘ y ∈ noExoticsSubsets (n + 1 + 4)
All goals completed! 🐙
B.5. Terms of FluxesTen obeying NoExotics and HasNoZero have card ≤ 3
lemma card_le_three_of_noExotics {F : FluxesTen} (hF : F.NoExotics) (hnZ : F.HasNoZero) :
F.card ≤ 3 := F:FluxesTenhF:F.NoExoticshnZ:F.HasNoZero⊢ Multiset.card F ≤ 3
F:FluxesTenhF:F.NoExoticshnZ:F.HasNoZerohx:F ∈ noExoticsSubsets (Multiset.card F)⊢ Multiset.card F ≤ 3
F:FluxesTenhF:F.NoExoticshnZ:F.HasNoZeron:ℕhx:F ∈ noExoticsSubsets n⊢ n ≤ 3
match n with
F:FluxesTenhF:F.NoExoticshnZ:F.HasNoZeron:ℕhx:F ∈ noExoticsSubsets 0⊢ 0 ≤ 3 All goals completed! 🐙
F:FluxesTenhF:F.NoExoticshnZ:F.HasNoZeron:ℕhx:F ∈ noExoticsSubsets 1⊢ 1 ≤ 3 All goals completed! 🐙
F:FluxesTenhF:F.NoExoticshnZ:F.HasNoZeron:ℕhx:F ∈ noExoticsSubsets 2⊢ 2 ≤ 3 All goals completed! 🐙
F:FluxesTenhF:F.NoExoticshnZ:F.HasNoZeron:ℕhx:F ∈ noExoticsSubsets 3⊢ 3 ≤ 3 All goals completed! 🐙
F:FluxesTenhF:F.NoExoticshnZ:F.HasNoZeron:ℕn✝:ℕhx:F ∈ noExoticsSubsets (n✝ + 4)⊢ n✝ + 4 ≤ 3 All goals completed! 🐙F:FluxesTenhF:F.NoExoticshnZ:F.HasNoZero⊢ Multiset.card F ≤ 3
All goals completed! 🐙
B.6. Terms of FluxesTen obeying NoExotics and HasNoZero are in elemsNoExotics
F:FluxesTenhNE:F.NoExoticshnZ:F.HasNoZerohF:F ∈ noExoticsSubsets 0hr:Multiset.card F = 0⊢ F ∈ elemsNoExotics
F:FluxesTenhNE:F.NoExoticshF:F ∈ noExoticsSubsets 0⊢ F ∈ elemsNoExotics
F:FluxesTenhF:F ∈ noExoticsSubsets 0⊢ F.NoExotics → F ∈ elemsNoExotics
⊢ ∀ F ∈ noExoticsSubsets 0, F.NoExotics → F ∈ elemsNoExotics
All goals completed! 🐙
B.7. Terms of FluxesTen obey NoExotics and HasNoZero if and only if in elemsNoExotics
Completeness of elemsNoExotics, that is, every element of FluxesTen
which obeys NoExotics is an element of elemsNoExotics, and every
element of elemsNoExotics obeys NoExotics.
lemma noExotics_iff_mem_elemsNoExotics (F : FluxesTen) :
F.NoExotics ∧ F.HasNoZero ↔ F ∈ elemsNoExotics := F:FluxesTen⊢ F.NoExotics ∧ F.HasNoZero ↔ F ∈ elemsNoExotics
F:FluxesTen⊢ F.NoExotics ∧ F.HasNoZero → F ∈ elemsNoExoticsF:FluxesTen⊢ F ∈ elemsNoExotics → F.NoExotics ∧ F.HasNoZero
F:FluxesTen⊢ F.NoExotics ∧ F.HasNoZero → F ∈ elemsNoExotics All goals completed! 🐙
F:FluxesTen⊢ F ∈ elemsNoExotics → F.NoExotics ∧ F.HasNoZero All goals completed! 🐙