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:
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.
Instances For
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
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 := ⋯ }
Instances For
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)
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.
Instances For
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)
:
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.
Instances For
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)
:
theorem
PureU1.Odd.generic_case
{n : ℕ}
{S : (PureU1 (2 * n.succ + 1)).Sols}
(h : PureU1.Odd.GenericCase S)
:
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