Line In Cubic Odd 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 the charge must be zero.

The main reference for this file is:

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

def PureU1.Odd.LineInCubic {n : ℕ} (S : (PureU1 (2 * n + 1)).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.Odd.lineInCubic_expand {n : ℕ} {S : (PureU1 (2 * n + 1)).LinSols} (h : LineInCubic S) (g f : Fin n → ℚ) : S.val = VectorLikeOddPlane.P g + VectorLikeOddPlane.P! f → ∀ (a b : ℚ), 3 * a * b * (a * ((accCubeTriLinSymm (VectorLikeOddPlane.P g)) (VectorLikeOddPlane.P g)) (VectorLikeOddPlane.P! f) + b * ((accCubeTriLinSymm (VectorLikeOddPlane.P! f)) (VectorLikeOddPlane.P! f)) (VectorLikeOddPlane.P g)) = 0

The condition that a linear solution sits on a line between the two planes within the cubic expands into a on accCubeTriLinSymm applied to the points within the planes.

theorem PureU1.Odd.line_in_cubic_P_P_P! {n : ℕ} {S : (PureU1 (2 * n + 1)).LinSols} (h : LineInCubic S) (g f : Fin n → ℚ) : S.val = VectorLikeOddPlane.P g + VectorLikeOddPlane.P! f → ((accCubeTriLinSymm (VectorLikeOddPlane.P g)) (VectorLikeOddPlane.P g)) (VectorLikeOddPlane.P! f) = 0

def PureU1.Odd.LineInCubicPerm {n : ℕ} (S : (PureU1 (2 * n + 1)).LinSols) : Prop

A LinSol satisfies lineInCubicPerm if all its permutations satisfy lineInCubic.

Equations

• PureU1.Odd.LineInCubicPerm S = ∀ (M : (PureU1.FamilyPermutations (2 * n + 1)).group), PureU1.Odd.LineInCubic (((PureU1.FamilyPermutations (2 * n + 1)).linSolRep M) S)

theorem PureU1.Odd.lineInCubicPerm_self {n : ℕ} {S : (PureU1 (2 * n + 1)).LinSols} (hS : LineInCubicPerm S) : LineInCubic S

If lineInCubicPerm S, then lineInCubic S.

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

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

theorem PureU1.Odd.lineInCubicPerm_swap {n : ℕ} {S : (PureU1 (2 * n.succ + 1)).LinSols} (LIC : LineInCubicPerm S) (j : Fin n.succ) (g f : Fin n.succ → ℚ) : S.val = VectorLikeOddPlane.Pa g f → (S.val (VectorLikeOddPlane.oddShiftSnd j) - S.val (VectorLikeOddPlane.oddShiftFst j)) * ((accCubeTriLinSymm (VectorLikeOddPlane.P g)) (VectorLikeOddPlane.P g)) (VectorLikeOddPlane.basis!AsCharges j) = 0

theorem PureU1.Odd.P_P_P!_accCube' {n : ℕ} {S : (PureU1 (2 * n.succ.succ + 1)).LinSols} (f g : Fin n.succ.succ → ℚ) (hS : S.val = VectorLikeOddPlane.Pa f g) : ((accCubeTriLinSymm (VectorLikeOddPlane.P f)) (VectorLikeOddPlane.P f)) (VectorLikeOddPlane.basis!AsCharges 0) = (S.val (VectorLikeOddPlane.oddShiftFst 0) + S.val (VectorLikeOddPlane.oddShiftSnd 0)) * (2 * S.val VectorLikeOddPlane.oddShiftZero + S.val (VectorLikeOddPlane.oddShiftFst 0) + S.val (VectorLikeOddPlane.oddShiftSnd 0))

theorem PureU1.Odd.lineInCubicPerm_last_cond {n : ℕ} {S : (PureU1 (2 * n.succ.succ + 1)).LinSols} (LIC : LineInCubicPerm S) : LineInPlaneProp (S.val (VectorLikeOddPlane.oddShiftSnd 0), S.val (VectorLikeOddPlane.oddShiftFst 0), S.val VectorLikeOddPlane.oddShiftZero)

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

theorem PureU1.Odd.lineInCubicPerm_constAbs {n : ℕ} {S : (PureU1 (2 * n.succ.succ + 1)).LinSols} (LIC : LineInCubicPerm S) : ConstAbs S.val

theorem PureU1.Odd.lineInCubicPerm_zero {n : ℕ} {S : (PureU1 (2 * n.succ.succ + 1)).LinSols} (LIC : LineInCubicPerm S) : S = 0