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 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 f : Fin n → ℚ) (a : ℚ) : (parameterizationAsLinear g f a).val = a • (((accCubeTriLinSymm (VectorLikeOddPlane.P! f)) (VectorLikeOddPlane.P! f)) (VectorLikeOddPlane.P g) • VectorLikeOddPlane.P g + -((accCubeTriLinSymm (VectorLikeOddPlane.P g)) (VectorLikeOddPlane.P g)) (VectorLikeOddPlane.P! f) • VectorLikeOddPlane.P! f)

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

The parameterization satisfies the cubic ACC.

def PureU1.Odd.parameterization {n : ℕ} (g 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 f : Fin n → ℚ) (hS : S.val = VectorLikeOddPlane.P g + VectorLikeOddPlane.P! f) : ((accCubeTriLinSymm (VectorLikeOddPlane.P g)) (VectorLikeOddPlane.P g)) (VectorLikeOddPlane.P! f) = -((accCubeTriLinSymm (VectorLikeOddPlane.P! f)) (VectorLikeOddPlane.P! f)) (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 = VectorLikeOddPlane.P g + VectorLikeOddPlane.P! f ∧ ((accCubeTriLinSymm (VectorLikeOddPlane.P g)) (VectorLikeOddPlane.P g)) (VectorLikeOddPlane.P! f) ≠ 0) : 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 = VectorLikeOddPlane.P g + VectorLikeOddPlane.P! f ∧ ((accCubeTriLinSymm (VectorLikeOddPlane.P g)) (VectorLikeOddPlane.P g)) (VectorLikeOddPlane.P! f) = 0) : SpecialCase S

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

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

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

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

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