The localized tadpole never obstructs an anomaly-free completion of (3, 60)

In the six-dimensional SU(4) gauge-Higgs unification model with the colour-fundamental block (3, 60), each species of added matter contributes an integer 10-vector [108 · (eight anomaly coefficients), Θ₀₁, Θ₂₃]; the anomalies are scaled by their common denominator 108. The species data are inputs (computed with SageMath).

The file exhibits four anomaly-neutral non-negative additions (sums of species) that realize the four signed tadpole axes ±Θ₀₁, ±Θ₂₃: a Farkas certificate that 0 is interior to the achievable tadpole cone. Two of their tadpoles are linearly independent, so Θ has rank 2 on the anomaly kernel and no linear invariant of Θ is conserved. Everything is decided by the kernel with decide; the file uses no Mathlib.

Main results

• existence_certificate: the four additions are anomaly-neutral, have tadpoles (288, 0), (−288, 0), (0, 48), (0, −16), and 288 · 48 − 0 · 0 ≠ 0.

References

• C. Marín, Anomaly- and Tadpole-Compatible Fermion Completion of Six-Dimensional SU(4) Gauge-Higgs Unification, Zenodo, doi:10.5281/zenodo.21432625.

@[reducible, inline]

abbrev GaugeHiggsUnification.R60JointExistence.Vec : Type

A species vector, of length 10: [a₀, …, a₇, Θ₀₁, Θ₂₃].

Equations

• GaugeHiggsUnification.R60JointExistence.Vec = List Int

def GaugeHiggsUnification.R60JointExistence.add (u v : Vec) : Vec

Componentwise sum.

Equations

• GaugeHiggsUnification.R60JointExistence.add u v = List.zipWith (fun (x1 x2 : Int) => x1 + x2) u v

def GaugeHiggsUnification.R60JointExistence.sumv (l : List Vec) : Vec

Sum of a list of vectors.

Equations

• GaugeHiggsUnification.R60JointExistence.sumv l = List.foldl GaugeHiggsUnification.R60JointExistence.add (List.replicate 10 0) l

def GaugeHiggsUnification.R60JointExistence.s86 : Vec

Equations

• GaugeHiggsUnification.R60JointExistence.s86 = [-3780, -88128, -11340, 648, -288, 108, -21828, -1728, 144, 0]

def GaugeHiggsUnification.R60JointExistence.s87 : Vec

Equations

• GaugeHiggsUnification.R60JointExistence.s87 = [3780, 88128, 11340, -648, 288, -108, 21828, 1728, 144, 0]

def GaugeHiggsUnification.R60JointExistence.s82 : Vec

Equations

• GaugeHiggsUnification.R60JointExistence.s82 = [-3780, -88128, -11340, -324, 288, 1188, 11028, 1728, -144, 0]

def GaugeHiggsUnification.R60JointExistence.s83 : Vec

Equations

• GaugeHiggsUnification.R60JointExistence.s83 = [3780, 88128, 11340, 324, -288, -1188, -11028, -1728, -144, 0]

def GaugeHiggsUnification.R60JointExistence.s129 : Vec

Equations

• GaugeHiggsUnification.R60JointExistence.s129 = [2160, -3564, 6480, 108, -126, -621, -2253, -756, -54, 12]

def GaugeHiggsUnification.R60JointExistence.s133 : Vec

Equations

• GaugeHiggsUnification.R60JointExistence.s133 = [2160, -3564, 6480, -108, 90, 378, 366, 540, 54, 12]

def GaugeHiggsUnification.R60JointExistence.s234 : Vec

Equations

• GaugeHiggsUnification.R60JointExistence.s234 = [-2160, 3564, -6480, 108, -90, -378, -366, -540, 54, 12]

def GaugeHiggsUnification.R60JointExistence.s238 : Vec

Equations

• GaugeHiggsUnification.R60JointExistence.s238 = [-2160, 3564, -6480, -108, 126, 621, 2253, 756, -54, 12]

def GaugeHiggsUnification.R60JointExistence.s122 : Vec

Equations

• GaugeHiggsUnification.R60JointExistence.s122 = [0, 1188, -2160, 0, 0, 126, 122, 180, -18, -4]

def GaugeHiggsUnification.R60JointExistence.s127 : Vec

Equations

• GaugeHiggsUnification.R60JointExistence.s127 = [0, -1188, 2160, 0, 0, 207, 751, 252, 18, -4]

def GaugeHiggsUnification.R60JointExistence.s216 : Vec

Equations

• GaugeHiggsUnification.R60JointExistence.s216 = [0, 1188, -2160, 0, 0, -207, -751, -252, 18, -4]

def GaugeHiggsUnification.R60JointExistence.s221 : Vec

Equations

• GaugeHiggsUnification.R60JointExistence.s221 = [0, -1188, 2160, 0, 0, -126, -122, -180, -18, -4]

def GaugeHiggsUnification.R60JointExistence.wP01 : Vec

Witness for +Θ₀₁.

Equations

• GaugeHiggsUnification.R60JointExistence.wP01 = GaugeHiggsUnification.R60JointExistence.sumv [GaugeHiggsUnification.R60JointExistence.s86, GaugeHiggsUnification.R60JointExistence.s87]

def GaugeHiggsUnification.R60JointExistence.wM01 : Vec

Witness for −Θ₀₁.

Equations

• GaugeHiggsUnification.R60JointExistence.wM01 = GaugeHiggsUnification.R60JointExistence.sumv [GaugeHiggsUnification.R60JointExistence.s82, GaugeHiggsUnification.R60JointExistence.s83]

def GaugeHiggsUnification.R60JointExistence.wP23 : Vec

Witness for +Θ₂₃.

Equations

• One or more equations did not get rendered due to their size.

def GaugeHiggsUnification.R60JointExistence.wM23 : Vec

Witness for −Θ₂₃.

Equations

• One or more equations did not get rendered due to their size.

def GaugeHiggsUnification.R60JointExistence.anomZero (v : Vec) : Bool

All eight anomalies cancel.

Equations

• GaugeHiggsUnification.R60JointExistence.anomZero v = (List.take 8 v).all fun (x : Int) => x == 0

def GaugeHiggsUnification.R60JointExistence.tad (v : Vec) : Int × Int

The tadpole (Θ₀₁, Θ₂₃).

Equations

• GaugeHiggsUnification.R60JointExistence.tad v = (List.getD v 8 0, List.getD v 9 0)

theorem GaugeHiggsUnification.R60JointExistence.existence_certificate : (anomZero wP01 = true ∧ anomZero wM01 = true ∧ anomZero wP23 = true ∧ anomZero wM23 = true) ∧ (tad wP01 = (288, 0) ∧ tad wM01 = (-288, 0) ∧ tad wP23 = (0, 48) ∧ tad wM23 = (0, -16)) ∧ 288 * 48 - 0 * 0 ≠ 0

Existence certificate. The four additions are anomaly-neutral and realize the four signed tadpole axes; two of their tadpoles, (288, 0) and (0, 48), have non-zero determinant.