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.Charges.AnomalyFree
public import Mathlib.Data.ZMod.DefsViable Quanta with Yukawa
i. Overview
We say a term of a type Quanta is viable
if it satisfies the following properties:
It has a Hd, Hu and at least one matter particle in the 5 and 10 representation.
It has no exotic chiral particles.
It leads to a top Yukawa coupling.
It does not lead to a pheno constraining terms.
It does not lead to a dangerous Yukawa coupling at one insertion of the Yukawa singlets.
It satisfies linear anomaly cancellation.
The charges are allowed by an I configuration.
We also write down the explicit set of viable quanta, and prove that this set is complete.
One can view the dependencies of this module with:
lake exe graph --from
Physlib.StringTheory.FTheory.SU5.Fluxes.Basic,Physlib.Particles.SuperSymmetry.SU5.FieldLabels
my_graph.pdf
ii. Key results
Quanta.IsViable : The proposition on a Quanta that it is viable.
Quanta.viableElems : The multiset of viable quanta.
Quanta.isViable_iff_mem_viableElems : A quanta is viable if and only if it is in the
Quanta.viableElems.
iii. Table of contents
A. The condition for a Quanta to be viable
A.1. Simplification of the prop to use the set of viable charges viableCharges I
A.2. Further simplification of the prop to use the set of viable charges Quanta.liftCharge
A.3. Further simplification of the prop to use the anomaly free set of viable charges
B. The multiset of viable quanta
B.1. Every element of the multiset is viable
B.2. A quanta is viable if and only if it is in the multiset
B.3. Every element of the multiset regenerates Yukawa at two insertions of the Yukawa singlets
B.4. Those quanta which satisfy the quartic anomaly cancellation condition
B.5. Map down to Z2
iv. References
The key reference for the material in this module is: arXiv:1507.05961.
@[expose] public section
A. The condition for a Quanta to be viable
For a given I : CodimensionOneConfig the condition on a Quanta for it to be
phenomenologically viable.
There is a Hd, Hu, 5-bar matter and 10d matter.
The charges do not lead to any phenomenologically constraining terms.
The charges are such that dangerous couplings in the super potential are not regenerated with the Yukawa terms.
The charges are such that they are allowed by a configuration of sections on the co-dimension 1 fiber.
Within the 5-bar matter, there is at most one entry for each charge.
Within the 10d matter, there is at most one entry for each charge.
The charges permit at least one Top-Yukawa coupling.
The fluxes of the 5-bar matter fields do not lead to any exotic chiral particles.
There are 5-bar matter fields where both fluxes are zero (these are not being counted here).
The fluxes of the 10d matter fields do not lead to any exotic chiral particles.
There are 10d matter fields where both fluxes are zero (these are not being counted here).
The quanta satisfy the linear anomaly cancellation conditions.
structure IsViable (x : Quanta) : Prop where has_all_charges : x.toCharges.IsComplete not_pheno_constrained : ¬ x.toCharges.IsPhenoConstrained not_regenerate_dangerous_couplings : ¬ x.toCharges.YukawaGeneratesDangerousAtLevel 1 charges_allowed_by_section_config :
(∃ I : CodimensionOneConfig, x.toCharges ∈ ofFinset I.allowedBarFiveCharges I.allowedTenCharges) no_duplicate_five_bar_charges : x.F.toCharges.Nodup no_duplicate_ten_charges : x.T.toCharges.Nodup allows_top_yukawa : AllowsTerm x.toCharges topYukawa no_exotics_from_five_bar : x.F.toFluxesFive.NoExotics no_five_bar_zero_fluxes : x.F.toFluxesFive.HasNoZero no_exotics_from_ten : x.T.toFluxesTen.NoExotics no_ten_zero_fluxes : x.T.toFluxesTen.HasNoZero linear_anomalies : x.LinearAnomalyCancellationlemma isViable_iff_def (x : Quanta) : IsViable x ↔
x.toCharges.IsComplete ∧
¬ x.toCharges.IsPhenoConstrained ∧
¬ x.toCharges.YukawaGeneratesDangerousAtLevel 1 ∧
(∃ I : CodimensionOneConfig, x.toCharges ∈
ofFinset I.allowedBarFiveCharges I.allowedTenCharges) ∧
x.F.toCharges.Nodup ∧
x.T.toCharges.Nodup ∧
x.toCharges.AllowsTerm topYukawa ∧
x.F.toFluxesFive.NoExotics ∧
x.F.toFluxesFive.HasNoZero ∧
x.T.toFluxesTen.NoExotics ∧
x.T.toFluxesTen.HasNoZero ∧
x.LinearAnomalyCancellation := x:Quanta⊢ x.IsViable ↔
x.toCharges.IsComplete ∧
¬x.toCharges.IsPhenoConstrained ∧
¬x.toCharges.YukawaGeneratesDangerousAtLevel 1 ∧
(∃ I, x.toCharges ∈ ofFinset I.allowedBarFiveCharges I.allowedTenCharges) ∧
(x.F ℤ).toCharges.Nodup ∧
(x.T ℤ).toCharges.Nodup ∧
x.toCharges.AllowsTerm topYukawa ∧
(x.F ℤ).toFluxesFive.NoExotics ∧
(x.F ℤ).toFluxesFive.HasNoZero ∧
(x.T ℤ).toFluxesTen.NoExotics ∧ (x.T ℤ).toFluxesTen.HasNoZero ∧ x.LinearAnomalyCancellation
x:Quanta⊢ x.toCharges.IsComplete ∧
¬x.toCharges.IsPhenoConstrained ∧
¬x.toCharges.YukawaGeneratesDangerousAtLevel 1 ∧
(∃ I, x.toCharges ∈ ofFinset I.allowedBarFiveCharges I.allowedTenCharges) ∧
(x.F ℤ).toCharges.Nodup ∧
(x.T ℤ).toCharges.Nodup ∧
x.toCharges.AllowsTerm topYukawa ∧
(x.F ℤ).toFluxesFive.NoExotics ∧
(x.F ℤ).toFluxesFive.HasNoZero ∧
(x.T ℤ).toFluxesTen.NoExotics ∧ (x.T ℤ).toFluxesTen.HasNoZero ∧ x.LinearAnomalyCancellation →
x.IsViable
All goals completed! 🐙
A.1. Simplification of the prop to use the set of viable charges viableCharges I
lemma isViable_iff_charges_mem_viableCharges (x : Quanta) :
IsViable x ↔
/- 1. Conditions just on the charges. -/
(∃ I, x.toCharges ∈ viableCharges I) ∧
x.F.toCharges.Nodup ∧
x.T.toCharges.Nodup ∧
/- 2. Conditions just on the fluxes -/
x.F.toFluxesFive.NoExotics ∧
x.F.toFluxesFive.HasNoZero ∧
x.T.toFluxesTen.NoExotics ∧
x.T.toFluxesTen.HasNoZero ∧
/- 3. Conditions on the fluxes and the charges. -/
x.LinearAnomalyCancellation := x:Quanta⊢ x.IsViable ↔
(∃ I, x.toCharges ∈ viableCharges I) ∧
(x.F ℤ).toCharges.Nodup ∧
(x.T ℤ).toCharges.Nodup ∧
(x.F ℤ).toFluxesFive.NoExotics ∧
(x.F ℤ).toFluxesFive.HasNoZero ∧
(x.T ℤ).toFluxesTen.NoExotics ∧ (x.T ℤ).toFluxesTen.HasNoZero ∧ x.LinearAnomalyCancellation
x:Quanta⊢ x.toCharges.IsComplete ∧
¬x.toCharges.IsPhenoConstrained ∧
¬x.toCharges.YukawaGeneratesDangerousAtLevel 1 ∧
(∃ I, x.toCharges ∈ ofFinset I.allowedBarFiveCharges I.allowedTenCharges) ∧
(x.F ℤ).toCharges.Nodup ∧
(x.T ℤ).toCharges.Nodup ∧
x.toCharges.AllowsTerm topYukawa ∧
(x.F ℤ).toFluxesFive.NoExotics ∧
(x.F ℤ).toFluxesFive.HasNoZero ∧
(x.T ℤ).toFluxesTen.NoExotics ∧ (x.T ℤ).toFluxesTen.HasNoZero ∧ x.LinearAnomalyCancellation ↔
(∃ I,
x.toCharges ∈ ofFinset I.allowedBarFiveCharges I.allowedTenCharges ∧
x.toCharges.AllowsTerm topYukawa ∧
¬x.toCharges.IsPhenoConstrained ∧ ¬x.toCharges.YukawaGeneratesDangerousAtLevel 1 ∧ x.toCharges.IsComplete) ∧
(x.F ℤ).toCharges.Nodup ∧
(x.T ℤ).toCharges.Nodup ∧
(x.F ℤ).toFluxesFive.NoExotics ∧
(x.F ℤ).toFluxesFive.HasNoZero ∧
(x.T ℤ).toFluxesTen.NoExotics ∧ (x.T ℤ).toFluxesTen.HasNoZero ∧ x.LinearAnomalyCancellation
All goals completed! 🐙
A.2. Further simplification of the prop to use the set of viable charges Quanta.liftCharge
x:Quanta⊢ (∃ I, x.toCharges ∈ viableCharges I) ∧
(x.F ℤ).toCharges.Nodup ∧
(x.T ℤ).toCharges.Nodup ∧
(x.F ℤ).toFluxesFive.NoExotics ∧
(x.F ℤ).toFluxesFive.HasNoZero ∧
(x.T ℤ).toFluxesTen.NoExotics ∧ (x.T ℤ).toFluxesTen.HasNoZero ∧ x.LinearAnomalyCancellation ↔
(∃ I, x.toCharges ∈ viableCharges I) ∧
((((x.F ℤ).toFluxesFive.NoExotics ∧ (x.F ℤ).toFluxesFive.HasNoZero) ∧
(x.F ℤ).toCharges.toFinset = x.toCharges.Q5 ℤ ∧ (x.F ℤ).toCharges.Nodup) ∧
((x.T ℤ).toFluxesTen.NoExotics ∧ (x.T ℤ).toFluxesTen.HasNoZero) ∧
(x.T ℤ).toCharges.toFinset = x.toCharges.Q10 ℤ ∧ (x.T ℤ).toCharges.Nodup) ∧
x.LinearAnomalyCancellation
All goals completed! 🐙A.3. Further simplification of the prop to use the anomaly free set of viable charges
lemma isViable_iff_filter (x : Quanta) :
IsViable x ↔ (∃ I, x.toCharges ∈ (viableCharges I).filter IsAnomalyFree) ∧
x ∈ Quanta.liftCharge x.toCharges
∧ x.LinearAnomalyCancellation := x:Quanta⊢ x.IsViable ↔
(∃ I, x.toCharges ∈ Multiset.filter IsAnomalyFree (viableCharges I)) ∧
x ∈ liftCharge x.toCharges ∧ x.LinearAnomalyCancellation
x:Quanta⊢ x ∈ liftCharge x.toCharges →
x.LinearAnomalyCancellation →
∀ (x_1 : CodimensionOneConfig),
x.toCharges ∈ viableCharges x_1 → ∃ x_2 ∈ liftCharge x.toCharges, x_2.LinearAnomalyCancellation
All goals completed! 🐙B. The multiset of viable quanta
We find all the viable quanta. This can be evaluated with
((((viableCharges .same ∪ viableCharges .nearestNeighbor ∪
viableCharges .nextToNearestNeighbor).filter IsAnomalyFree).bind
Quanta.liftCharge).filter LinearAnomalyCancellation)
Given a CodimensionOneConfig the Quanta which satisfy the condition IsViable.
def viableElems : Multiset Quanta :=
{⟨some 2, some (-2), {(-1, ⟨3, -2⟩), (-3, ⟨0, 2⟩)}, {(-1, ⟨3, 0⟩)}⟩,
⟨some 2, some (-2), {(-1, ⟨3, -2⟩), (-3, ⟨0, 2⟩)}, {(-1, ⟨3, 0⟩)}⟩,
⟨some 2, some (-2), {(-1, ⟨2, -2⟩), (-3, ⟨1, 2⟩)}, {(-1, ⟨3, 0⟩)}⟩,
⟨some 2, some (-2), {(-1, ⟨2, -2⟩), (-3, ⟨1, 2⟩)}, {(-1, ⟨3, 0⟩)}⟩,
⟨some 2, some (-2), {(1, ⟨3, -2⟩), (-1, ⟨0, 2⟩)}, {(-1, ⟨3, 0⟩)}⟩,
⟨some 2, some (-2), {(1, ⟨3, -2⟩), (-1, ⟨0, 2⟩)}, {(-1, ⟨3, 0⟩)}⟩,
⟨some 2, some (-2), {(1, ⟨2, -2⟩), (-1, ⟨1, 2⟩)}, {(-1, ⟨3, 0⟩)}⟩,
⟨some 2, some (-2), {(1, ⟨2, -2⟩), (-1, ⟨1, 2⟩)}, {(-1, ⟨3, 0⟩)}⟩,
⟨some (-2), some 2, {(-1, ⟨3, -2⟩), (1, ⟨0, 2⟩)}, {(1, ⟨3, 0⟩)}⟩,
⟨some (-2), some 2, {(-1, ⟨3, -2⟩), (1, ⟨0, 2⟩)}, {(1, ⟨3, 0⟩)}⟩,
⟨some (-2), some 2, {(-1, ⟨2, -2⟩), (1, ⟨1, 2⟩)}, {(1, ⟨3, 0⟩)}⟩,
⟨some (-2), some 2, {(-1, ⟨2, -2⟩), (1, ⟨1, 2⟩)}, {(1, ⟨3, 0⟩)}⟩,
⟨some (-2), some 2, {(1, ⟨3, -2⟩), (3, ⟨0, 2⟩)}, {(1, ⟨3, 0⟩)}⟩,
⟨some (-2), some 2, {(1, ⟨3, -2⟩), (3, ⟨0, 2⟩)}, {(1, ⟨3, 0⟩)}⟩,
⟨some (-2), some 2, {(1, ⟨2, -2⟩), (3, ⟨1, 2⟩)}, {(1, ⟨3, 0⟩)}⟩,
⟨some (-2), some 2, {(1, ⟨2, -2⟩), (3, ⟨1, 2⟩)}, {(1, ⟨3, 0⟩)}⟩,
⟨some (-4), some (-14), {(11, ⟨3, -2⟩), (6, ⟨0, 2⟩)}, {(-7, ⟨3, 0⟩)}⟩,
⟨some (-4), some (-14), {(11, ⟨3, -2⟩), (6, ⟨0, 2⟩)}, {(-7, ⟨3, 0⟩)}⟩,
⟨some (-4), some (-14), {(11, ⟨2, -2⟩), (6, ⟨1, 2⟩)}, {(-7, ⟨3, 0⟩)}⟩,
⟨some (-4), some (-14), {(11, ⟨2, -2⟩), (6, ⟨1, 2⟩)}, {(-7, ⟨3, 0⟩)}⟩,
⟨some 6, some (-14), {(1, ⟨3, -2⟩), (-9, ⟨0, 2⟩)}, {(-7, ⟨3, 0⟩)}⟩,
⟨some 6, some (-14), {(1, ⟨3, -2⟩), (-9, ⟨0, 2⟩)}, {(-7, ⟨3, 0⟩)}⟩,
⟨some 6, some (-14), {(1, ⟨2, -2⟩), (-9, ⟨1, 2⟩)}, {(-7, ⟨3, 0⟩)}⟩,
⟨some 6, some (-14), {(1, ⟨2, -2⟩), (-9, ⟨1, 2⟩)}, {(-7, ⟨3, 0⟩)}⟩,
⟨some 6, some (-14), {(11, ⟨3, -2⟩), (1, ⟨0, 2⟩)}, {(-7, ⟨3, 0⟩)}⟩,
⟨some 6, some (-14), {(11, ⟨3, -2⟩), (1, ⟨0, 2⟩)}, {(-7, ⟨3, 0⟩)}⟩,
⟨some 6, some (-14), {(11, ⟨2, -2⟩), (1, ⟨1, 2⟩)}, {(-7, ⟨3, 0⟩)}⟩,
⟨some 6, some (-14), {(11, ⟨2, -2⟩), (1, ⟨1, 2⟩)}, {(-7, ⟨3, 0⟩)}⟩,
⟨some (-14), some 6, {(1, ⟨3, -2⟩), (11, ⟨0, 2⟩)}, {(3, ⟨3, 0⟩)}⟩,
⟨some (-14), some 6, {(1, ⟨3, -2⟩), (11, ⟨0, 2⟩)}, {(3, ⟨3, 0⟩)}⟩,
⟨some (-14), some 6, {(1, ⟨2, -2⟩), (11, ⟨1, 2⟩)}, {(3, ⟨3, 0⟩)}⟩,
⟨some (-14), some 6, {(1, ⟨2, -2⟩), (11, ⟨1, 2⟩)}, {(3, ⟨3, 0⟩)}⟩,
⟨some 2, some 12, {(-13, ⟨3, -2⟩), (-8, ⟨0, 2⟩)}, {(6, ⟨3, 0⟩)}⟩,
⟨some 2, some 12, {(-13, ⟨3, -2⟩), (-8, ⟨0, 2⟩)}, {(6, ⟨3, 0⟩)}⟩,
⟨some 2, some 12, {(-13, ⟨2, -2⟩), (-8, ⟨1, 2⟩)}, {(6, ⟨3, 0⟩)}⟩,
⟨some 2, some 12, {(-13, ⟨2, -2⟩), (-8, ⟨1, 2⟩)}, {(6, ⟨3, 0⟩)}⟩}B.1. Every element of the multiset is viable
x:Quantah:x ∈ viableElems⊢ (∃ I, x.toCharges ∈ viableCharges I) ∧ x ∈ liftCharge x.toCharges ∧ x.LinearAnomalyCancellation
⊢ ∀ x ∈ viableElems, (∃ I, x.toCharges ∈ viableCharges I) ∧ x ∈ liftCharge x.toCharges ∧ x.LinearAnomalyCancellation
All goals completed! 🐙B.2. A quanta is viable if and only if it is in the multiset
I:CodimensionOneConfigc:ChargeSpectrumhc:c ∈
match I with
| CodimensionOneConfig.same =>
{{ qHd := some 2, qHu := some (-2), Q5 := {-3, -1}, Q10 := {-1} },
{ qHd := some 2, qHu := some (-2), Q5 := {-1, 1}, Q10 := {-1} },
{ qHd := some (-2), qHu := some 2, Q5 := {-1, 1}, Q10 := {1} },
{ qHd := some (-2), qHu := some 2, Q5 := {1, 3}, Q10 := {1} }}
| CodimensionOneConfig.nearestNeighbor =>
{{ qHd := some (-4), qHu := some (-14), Q5 := {6, 11}, Q10 := {-7} },
{ qHd := some 6, qHu := some (-14), Q5 := {-9, 1}, Q10 := {-7} },
{ qHd := some 6, qHu := some (-14), Q5 := {1, 11}, Q10 := {-7} },
{ qHd := some (-14), qHu := some 6, Q5 := {1, 11}, Q10 := {3} }}
| CodimensionOneConfig.nextToNearestNeighbor => {{ qHd := some 2, qHu := some 12, Q5 := {-13, -8}, Q10 := {6} }}⊢ ∀ x ∈ liftCharge c, x.LinearAnomalyCancellation → x ∈ viableElems
I:CodimensionOneConfig⊢ ∀
c ∈
match I with
| CodimensionOneConfig.same =>
{{ qHd := some 2, qHu := some (-2), Q5 := {-3, -1}, Q10 := {-1} },
{ qHd := some 2, qHu := some (-2), Q5 := {-1, 1}, Q10 := {-1} },
{ qHd := some (-2), qHu := some 2, Q5 := {-1, 1}, Q10 := {1} },
{ qHd := some (-2), qHu := some 2, Q5 := {1, 3}, Q10 := {1} }}
| CodimensionOneConfig.nearestNeighbor =>
{{ qHd := some (-4), qHu := some (-14), Q5 := {6, 11}, Q10 := {-7} },
{ qHd := some 6, qHu := some (-14), Q5 := {-9, 1}, Q10 := {-7} },
{ qHd := some 6, qHu := some (-14), Q5 := {1, 11}, Q10 := {-7} },
{ qHd := some (-14), qHu := some 6, Q5 := {1, 11}, Q10 := {3} }}
| CodimensionOneConfig.nextToNearestNeighbor => {{ qHd := some 2, qHu := some 12, Q5 := {-13, -8}, Q10 := {6} }},
∀ x ∈ liftCharge c, x.LinearAnomalyCancellation → x ∈ viableElems
⊢ ∀ (I : CodimensionOneConfig),
∀
c ∈
match I with
| CodimensionOneConfig.same =>
{{ qHd := some 2, qHu := some (-2), Q5 := {-3, -1}, Q10 := {-1} },
{ qHd := some 2, qHu := some (-2), Q5 := {-1, 1}, Q10 := {-1} },
{ qHd := some (-2), qHu := some 2, Q5 := {-1, 1}, Q10 := {1} },
{ qHd := some (-2), qHu := some 2, Q5 := {1, 3}, Q10 := {1} }}
| CodimensionOneConfig.nearestNeighbor =>
{{ qHd := some (-4), qHu := some (-14), Q5 := {6, 11}, Q10 := {-7} },
{ qHd := some 6, qHu := some (-14), Q5 := {-9, 1}, Q10 := {-7} },
{ qHd := some 6, qHu := some (-14), Q5 := {1, 11}, Q10 := {-7} },
{ qHd := some (-14), qHu := some 6, Q5 := {1, 11}, Q10 := {3} }}
| CodimensionOneConfig.nextToNearestNeighbor => {{ qHd := some 2, qHu := some 12, Q5 := {-13, -8}, Q10 := {6} }},
∀ x ∈ liftCharge c, x.LinearAnomalyCancellation → x ∈ viableElems
All goals completed! 🐙
x:Quanta⊢ x ∈ viableElems → x.IsViable All goals completed! 🐙B.3. Every element of the multiset regenerates Yukawa at two insertions of the Yukawa singlets
Every viable Quanta regenerates a dangerous coupling at two insertions of the Yukawa singlets.
x:Quantah:x ∈ viableElems⊢ x.toCharges.YukawaGeneratesDangerousAtLevel 2
⊢ ∀ x ∈ viableElems, x.toCharges.YukawaGeneratesDangerousAtLevel 2
All goals completed! 🐙B.4. Those quanta which satisfy the quartic anomaly cancellation condition
x:Quantah:x ∈ viableElems⊢ x.QuarticAnomalyCancellation ↔
x ∈
{{ qHd := some 2, qHu := some (-2), F := {(-1, { M := 1, N := 2 }), (1, { M := 2, N := -2 })},
T := {(-1, { M := 3, N := 0 })} },
{ qHd := some 2, qHu := some (-2), F := {(-1, { M := 0, N := 2 }), (1, { M := 3, N := -2 })},
T := {(-1, { M := 3, N := 0 })} },
{ qHd := some (-2), qHu := some 2, F := {(-1, { M := 2, N := -2 }), (1, { M := 1, N := 2 })},
T := {(1, { M := 3, N := 0 })} },
{ qHd := some (-2), qHu := some 2, F := {(-1, { M := 3, N := -2 }), (1, { M := 0, N := 2 })},
T := {(1, { M := 3, N := 0 })} },
{ qHd := some 6, qHu := some (-14), F := {(-9, { M := 1, N := 2 }), (1, { M := 2, N := -2 })},
T := {(-7, { M := 3, N := 0 })} },
{ qHd := some 6, qHu := some (-14), F := {(-9, { M := 0, N := 2 }), (1, { M := 3, N := -2 })},
T := {(-7, { M := 3, N := 0 })} }}
⊢ ∀ x ∈ viableElems,
x.QuarticAnomalyCancellation ↔
x ∈
{{ qHd := some 2, qHu := some (-2), F := {(-1, { M := 1, N := 2 }), (1, { M := 2, N := -2 })},
T := {(-1, { M := 3, N := 0 })} },
{ qHd := some 2, qHu := some (-2), F := {(-1, { M := 0, N := 2 }), (1, { M := 3, N := -2 })},
T := {(-1, { M := 3, N := 0 })} },
{ qHd := some (-2), qHu := some 2, F := {(-1, { M := 2, N := -2 }), (1, { M := 1, N := 2 })},
T := {(1, { M := 3, N := 0 })} },
{ qHd := some (-2), qHu := some 2, F := {(-1, { M := 3, N := -2 }), (1, { M := 0, N := 2 })},
T := {(1, { M := 3, N := 0 })} },
{ qHd := some 6, qHu := some (-14), F := {(-9, { M := 1, N := 2 }), (1, { M := 2, N := -2 })},
T := {(-7, { M := 3, N := 0 })} },
{ qHd := some 6, qHu := some (-14), F := {(-9, { M := 0, N := 2 }), (1, { M := 3, N := -2 })},
T := {(-7, { M := 3, N := 0 })} }}
All goals completed! 🐙B.5. Map down to Z2
x:Quantah:x ∈ viableElems⊢ map (Int.castAddHom (ZMod 2)) x.toCharges ∈
{{ qHd := some 0, qHu := some 0, Q5 := {1}, Q10 := {1} }, { qHd := some 0, qHu := some 0, Q5 := {0, 1}, Q10 := {1} },
{ qHd := some 0, qHu := some 0, Q5 := {0, 1}, Q10 := {0} }}
⊢ ∀ x ∈ viableElems,
map (Int.castAddHom (ZMod 2)) x.toCharges ∈
{{ qHd := some 0, qHu := some 0, Q5 := {1}, Q10 := {1} },
{ qHd := some 0, qHu := some 0, Q5 := {0, 1}, Q10 := {1} },
{ qHd := some 0, qHu := some 0, Q5 := {0, 1}, Q10 := {0} }}
All goals completed! 🐙