Line In Cubic Even case

We say that a linear solution satisfies the lineInCubic property if the line through that point and through the two different planes formed by the basis of LinSols lies in the cubic.

We show that for a solution all its permutations satisfy this property, then there exists a permutation for which it lies in the plane spanned by the first part of the basis.

The main reference for this file is:

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

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

A property on LinSols, satisfied if every point on the line between the two planes in the basis through that point is in the cubic.

Equations

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

theorem PureU1.Even.lineInCubic_expand {n : ℕ} {S : (PureU1 (2 * n.succ)).LinSols} (h : LineInCubic S) (g : Fin n.succ → ℚ) (f : Fin n → ℚ) : S.val = VectorLikeEvenPlane.Pa g f → ∀ (a b : ℚ), 3 * a * b * (a * ((accCubeTriLinSymm (VectorLikeEvenPlane.P g)) (VectorLikeEvenPlane.P g)) (VectorLikeEvenPlane.P! f) + b * ((accCubeTriLinSymm (VectorLikeEvenPlane.P! f)) (VectorLikeEvenPlane.P! f)) (VectorLikeEvenPlane.P g)) = 0

theorem PureU1.Even.line_in_cubic_P_P_P! {n : ℕ} {S : (PureU1 (2 * n.succ)).LinSols} (h : LineInCubic S) (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

This lemma states that for a given S of type (PureU1 (2 * n.succ)).AnomalyFreeLinear and a proof h that the line through S lies on a cubic curve, for any functions g : Fin n.succ → ℚ and f : Fin n → ℚ, if S.val = P g + P! f, then accCubeTriLinSymm.toFun (P g, P g, P! f) = 0.

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

A LinSol satisfies LineInCubicPerm if all its permutations satisfy lineInCubic.

Equations

• PureU1.Even.LineInCubicPerm S = ∀ (M : (PureU1.FamilyPermutations (2 * n.succ)).group), PureU1.Even.LineInCubic (((PureU1.FamilyPermutations (2 * n.succ)).linSolRep M) S)

theorem PureU1.Even.lineInCubicPerm_self {n : ℕ} {S : (PureU1 (2 * n.succ)).LinSols} (hS : LineInCubicPerm S) : LineInCubic S

If lineInCubicPerm S then lineInCubic S.

theorem PureU1.Even.lineInCubicPerm_permute {n : ℕ} {S : (PureU1 (2 * n.succ)).LinSols} (hS : LineInCubicPerm S) (M' : (FamilyPermutations (2 * n.succ)).group) : LineInCubicPerm (((FamilyPermutations (2 * n.succ)).linSolRep M') S)

If lineInCubicPerm S then lineInCubicPerm (M S) for all permutations M.

theorem PureU1.Even.lineInCubicPerm_swap {n : ℕ} {S : (PureU1 (2 * n.succ)).LinSols} (LIC : LineInCubicPerm S) (j : Fin n) (g : Fin n.succ → ℚ) (f : Fin n → ℚ) : S.val = VectorLikeEvenPlane.Pa g f → (S.val (VectorLikeEvenPlane.evenShiftSnd j) - S.val (VectorLikeEvenPlane.evenShiftFst j)) * ((accCubeTriLinSymm (VectorLikeEvenPlane.P g)) (VectorLikeEvenPlane.P g)) (VectorLikeEvenPlane.basis!AsCharges j) = 0

theorem PureU1.Even.P_P_P!_accCube' {n : ℕ} {S : (PureU1 (2 * n.succ.succ)).LinSols} (f : Fin n.succ.succ → ℚ) (g : Fin n.succ → ℚ) (hS : S.val = VectorLikeEvenPlane.Pa f g) : ((accCubeTriLinSymm (VectorLikeEvenPlane.P f)) (VectorLikeEvenPlane.P f)) (VectorLikeEvenPlane.basis!AsCharges (Fin.last n)) = -(S.val (VectorLikeEvenPlane.evenShiftSnd (Fin.last n)) + S.val (VectorLikeEvenPlane.evenShiftFst (Fin.last n))) * (2 * S.val VectorLikeEvenPlane.evenShiftLast + S.val (VectorLikeEvenPlane.evenShiftSnd (Fin.last n)) + S.val (VectorLikeEvenPlane.evenShiftFst (Fin.last n)))

theorem PureU1.Even.lineInCubicPerm_last_cond {n : ℕ} {S : (PureU1 (2 * n.succ.succ)).LinSols} (LIC : LineInCubicPerm S) : LineInPlaneProp (S.val (VectorLikeEvenPlane.evenShiftSnd (Fin.last n)), S.val (VectorLikeEvenPlane.evenShiftFst (Fin.last n)), S.val VectorLikeEvenPlane.evenShiftLast)

theorem PureU1.Even.lineInCubicPerm_last_perm {n : ℕ} {S : (PureU1 (2 * n.succ.succ)).LinSols} (LIC : LineInCubicPerm S) : LineInPlaneCond S

theorem PureU1.Even.lineInCubicPerm_constAbs {n : ℕ} {S : (PureU1 (2 * n.succ.succ)).Sols} (LIC : LineInCubicPerm S.toLinSols) : ConstAbs S.val

theorem PureU1.Even.lineInCubicPerm_vectorLike {n : ℕ} {S : (PureU1 (2 * n.succ.succ)).Sols} (LIC : LineInCubicPerm S.toLinSols) : VectorLikeEven S.val

theorem PureU1.Even.lineInCubicPerm_in_plane {n : ℕ} (S : (PureU1 (2 * n.succ.succ)).Sols) (LIC : LineInCubicPerm S.toLinSols) : ∃ (M : (FamilyPermutations (2 * n.succ.succ)).group), ((FamilyPermutations (2 * n.succ.succ)).linSolRep M) S.toLinSols ∈ Submodule.span ℚ (Set.range VectorLikeEvenPlane.basis)