Parameterization in odd case

Given maps g : Fin n → ℚ, f : Fin n → ℚ and a : ℚ we form a solution to the anomaly equations. We show that every solution can be got in this way, up to permutation, unless it is zero.

The main reference is:

• https://arxiv.org/pdf/1912.04804.pdf

def PureU1.Odd.parameterizationAsLinear {n : ℕ} (g : Fin n → ℚ) (f : Fin n → ℚ) (a : ℚ) : (PureU1 (2 * n + 1)).LinSols

Given a g f : Fin n → ℚ and a a : ℚ we form a linear solution. We will later show that this can be extended to a complete solution.

Equations

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

theorem PureU1.Odd.parameterizationAsLinear_val {n : ℕ} (g : Fin n → ℚ) (f : Fin n → ℚ) (a : ℚ) : (PureU1.Odd.parameterizationAsLinear g f a).val = a • (((PureU1.accCubeTriLinSymm (PureU1.VectorLikeOddPlane.P! f)) (PureU1.VectorLikeOddPlane.P! f)) (PureU1.VectorLikeOddPlane.P g) • PureU1.VectorLikeOddPlane.P g + -((PureU1.accCubeTriLinSymm (PureU1.VectorLikeOddPlane.P g)) (PureU1.VectorLikeOddPlane.P g)) (PureU1.VectorLikeOddPlane.P! f) • PureU1.VectorLikeOddPlane.P! f)

theorem PureU1.Odd.parameterizationCharge_cube {n : ℕ} (g : Fin n → ℚ) (f : Fin n → ℚ) (a : ℚ) : (PureU1.accCube (2 * n + 1)) (PureU1.Odd.parameterizationAsLinear g f a).val = 0

def PureU1.Odd.parameterization {n : ℕ} (g : Fin n → ℚ) (f : Fin n → ℚ) (a : ℚ) : (PureU1 (2 * n + 1)).Sols

Given a g f : Fin n → ℚ and a a : ℚ we form a solution.

Equations

• PureU1.Odd.parameterization g f a = { toLinSols := PureU1.Odd.parameterizationAsLinear g f a, quadSol := ⋯, cubicSol := ⋯ }

theorem PureU1.Odd.anomalyFree_param {n : ℕ} {S : (PureU1 (2 * n + 1)).Sols} (g : Fin n → ℚ) (f : Fin n → ℚ) (hS : S.val = PureU1.VectorLikeOddPlane.P g + PureU1.VectorLikeOddPlane.P! f) : ((PureU1.accCubeTriLinSymm (PureU1.VectorLikeOddPlane.P g)) (PureU1.VectorLikeOddPlane.P g)) (PureU1.VectorLikeOddPlane.P! f) = -((PureU1.accCubeTriLinSymm (PureU1.VectorLikeOddPlane.P! f)) (PureU1.VectorLikeOddPlane.P! f)) (PureU1.VectorLikeOddPlane.P g)

def PureU1.Odd.GenericCase {n : ℕ} (S : (PureU1 (2 * n.succ + 1)).Sols) : Prop

A proposition on a solution which is true if accCubeTriLinSymm (P g, P g, P! f) ≠ 0. In this case our parameterization above will be able to recover this point.

Equations

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

theorem PureU1.Odd.genericCase_exists {n : ℕ} (S : (PureU1 (2 * n.succ + 1)).Sols) (hs : ∃ (g : Fin n.succ → ℚ) (f : Fin n.succ → ℚ), S.val = PureU1.VectorLikeOddPlane.P g + PureU1.VectorLikeOddPlane.P! f ∧ ((PureU1.accCubeTriLinSymm (PureU1.VectorLikeOddPlane.P g)) (PureU1.VectorLikeOddPlane.P g)) (PureU1.VectorLikeOddPlane.P! f) ≠ 0) : PureU1.Odd.GenericCase S

def PureU1.Odd.SpecialCase {n : ℕ} (S : (PureU1 (2 * n.succ + 1)).Sols) : Prop

A proposition on a solution which is true if accCubeTriLinSymm (P g, P g, P! f) ≠ 0. In this case we will show that S is zero if it is true for all permutations.

Equations

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

theorem PureU1.Odd.specialCase_exists {n : ℕ} (S : (PureU1 (2 * n.succ + 1)).Sols) (hs : ∃ (g : Fin n.succ → ℚ) (f : Fin n.succ → ℚ), S.val = PureU1.VectorLikeOddPlane.P g + PureU1.VectorLikeOddPlane.P! f ∧ ((PureU1.accCubeTriLinSymm (PureU1.VectorLikeOddPlane.P g)) (PureU1.VectorLikeOddPlane.P g)) (PureU1.VectorLikeOddPlane.P! f) = 0) : PureU1.Odd.SpecialCase S

theorem PureU1.Odd.generic_or_special {n : ℕ} (S : (PureU1 (2 * n.succ + 1)).Sols) : PureU1.Odd.GenericCase S ∨ PureU1.Odd.SpecialCase S

theorem PureU1.Odd.generic_case {n : ℕ} {S : (PureU1 (2 * n.succ + 1)).Sols} (h : PureU1.Odd.GenericCase S) : ∃ (g : Fin n.succ → ℚ) (f : Fin n.succ → ℚ) (a : ℚ), S = PureU1.Odd.parameterization g f a

theorem PureU1.Odd.special_case_lineInCubic {n : ℕ} {S : (PureU1 (2 * n.succ + 1)).Sols} (h : PureU1.Odd.SpecialCase S) : PureU1.Odd.LineInCubic S.toLinSols

theorem PureU1.Odd.special_case_lineInCubic_perm {n : ℕ} {S : (PureU1 (2 * n.succ + 1)).Sols} (h : ∀ (M : (PureU1.FamilyPermutations (2 * n.succ + 1)).group), PureU1.Odd.SpecialCase ((MulAction.toFun (PureU1.FamilyPermutations (2 * n.succ + 1)).group (PureU1 (2 * n.succ + 1)).Sols) S M)) : PureU1.Odd.LineInCubicPerm S.toLinSols

theorem PureU1.Odd.special_case {n : ℕ} {S : (PureU1 (2 * n.succ.succ + 1)).Sols} (h : ∀ (M : (PureU1.FamilyPermutations (2 * n.succ.succ + 1)).group), PureU1.Odd.SpecialCase ((MulAction.toFun (PureU1.FamilyPermutations (2 * n.succ.succ + 1)).group (PureU1 (2 * n.succ.succ + 1)).Sols) S M)) : S.toLinSols = 0