The Pure U(1) case with 3 fermion

We show that S is a solution only if one of its charges is zero. We define a surjective map from LinSols with a charge equal to zero to Sols.

theorem PureU1.Three.cube_for_linSol' (S : (PureU1 3).LinSols) : 3 * S.val 0 * S.val 1 * S.val 2 = 0 ↔ (PureU1 3).cubicACC S.val = 0

theorem PureU1.Three.cube_for_linSol (S : (PureU1 3).LinSols) : S.val 0 = 0 ∨ S.val 1 = 0 ∨ S.val 2 = 0 ↔ (PureU1 3).cubicACC S.val = 0

theorem PureU1.Three.three_sol_zero (S : (PureU1 3).Sols) : S.val 0 = 0 ∨ S.val 1 = 0 ∨ S.val 2 = 0

def PureU1.Three.solOfLinear (S : (PureU1 3).LinSols) (hS : S.val 0 = 0 ∨ S.val 1 = 0 ∨ S.val 2 = 0) : (PureU1 3).Sols

Given a LinSol with a charge equal to zero a Sol.

Equations

• PureU1.Three.solOfLinear S hS = { toLinSols := S, quadSol := ⋯, cubicSol := ⋯ }

theorem PureU1.Three.solOfLinear_surjects (S : (PureU1 3).Sols) : ∃ (T : (PureU1 3).LinSols) (hT : T.val 0 = 0 ∨ T.val 1 = 0 ∨ T.val 2 = 0), solOfLinear T hT = S