Parameterization in even case

Given maps g : Fin n.succ → ℚ, 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, up to permutation, lives in the plane spanned by the first part of the basis vector.

The main reference is:

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

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

Given coefficients g of a point in P and f of a point in P!, and a rational, we get a rational a ∈ ℚ, we get a point in (PureU1 (2 * n.succ)).AnomalyFreeLinear, which we will later show extends to an anomaly free point.

Equations

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

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

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

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

The construction of a Sol from a Fin n.succ → ℚ, a Fin n → ℚ and a ℚ.

Equations

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

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

def PureU1.Even.GenericCase {n : ℕ} (S : (PureU1 (2 * n.succ)).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.Even.genericCase_exists {n : ℕ} (S : (PureU1 (2 * n.succ)).Sols) (hs : ∃ (g : Fin n.succ → ℚ) (f : Fin n → ℚ), S.val = VectorLikeEvenPlane.P g + VectorLikeEvenPlane.P! f ∧ ((accCubeTriLinSymm (VectorLikeEvenPlane.P g)) (VectorLikeEvenPlane.P g)) (VectorLikeEvenPlane.P! f) ≠ 0) : GenericCase S

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

A proposition on a solution which is true if accCubeTriLinSymm (P g, P g, P! f) = 0.

Equations

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

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

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

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

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

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

theorem PureU1.Even.special_case {n : ℕ} {S : (PureU1 (2 * n.succ.succ)).Sols} (h : ∀ (M : (FamilyPermutations (2 * n.succ.succ)).group), SpecialCase ((MulAction.toFun (FamilyPermutations (2 * n.succ.succ)).group (PureU1 (2 * n.succ.succ)).Sols) S M)) : ∃ (M : (FamilyPermutations (2 * n.succ.succ)).group), ((MulAction.toFun (FamilyPermutations (2 * n.succ.succ)).group (PureU1 (2 * n.succ.succ)).Sols) S M).toLinSols ∈ Submodule.span ℚ (Set.range VectorLikeEvenPlane.basis)