feat: Add properties for line in cubic
This commit is contained in:
jstoobysmith
parent
3218b93c27
commit
18183c8cef
3 changed files with 349 additions and 1 deletions
|
|
@ -13,12 +13,14 @@ import HepLean.AnomalyCancellation.MSSMNu.Y3
|
|||
import HepLean.AnomalyCancellation.PureU1.Basic
|
||||
import HepLean.AnomalyCancellation.PureU1.BasisLinear
|
||||
import HepLean.AnomalyCancellation.PureU1.ConstAbs
|
||||
import HepLean.AnomalyCancellation.PureU1.LineInPlaneCond
|
||||
import HepLean.AnomalyCancellation.PureU1.Even.BasisLinear
|
||||
import HepLean.AnomalyCancellation.PureU1.Even.LineInCubic
|
||||
import HepLean.AnomalyCancellation.PureU1.LineInPlaneCond
|
||||
import HepLean.AnomalyCancellation.PureU1.LowDim.One
|
||||
import HepLean.AnomalyCancellation.PureU1.LowDim.Three
|
||||
import HepLean.AnomalyCancellation.PureU1.LowDim.Two
|
||||
import HepLean.AnomalyCancellation.PureU1.Odd.BasisLinear
|
||||
import HepLean.AnomalyCancellation.PureU1.Odd.LineInCubic
|
||||
import HepLean.AnomalyCancellation.PureU1.Permutations
|
||||
import HepLean.AnomalyCancellation.PureU1.Sort
|
||||
import HepLean.AnomalyCancellation.PureU1.VectorLike
|
||||
|
|
|
|||
173
HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean
Normal file
173
HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean
Normal file
|
|
@ -0,0 +1,173 @@
|
|||
/-
|
||||
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
|
||||
Released under Apache 2.0 license.
|
||||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import HepLean.AnomalyCancellation.PureU1.Basic
|
||||
import HepLean.AnomalyCancellation.PureU1.ConstAbs
|
||||
import HepLean.AnomalyCancellation.PureU1.Even.BasisLinear
|
||||
import HepLean.AnomalyCancellation.PureU1.LineInPlaneCond
|
||||
import HepLean.AnomalyCancellation.PureU1.Permutations
|
||||
import Mathlib.RepresentationTheory.Basic
|
||||
import Mathlib.Tactic.Polyrith
|
||||
/-!
|
||||
|
||||
# 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 baisis of
|
||||
`LinSols` lies in the cubic.
|
||||
|
||||
We show that for a solution all its permutations satsfiy 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
|
||||
-/
|
||||
|
||||
namespace PureU1
|
||||
namespace Even
|
||||
|
||||
open BigOperators
|
||||
|
||||
variable {n : ℕ}
|
||||
open VectorLikeEvenPlane
|
||||
|
||||
/-- A property on `LinSols`, statified if every point on the line between the two planes
|
||||
in the basis through that point is in the cubic. -/
|
||||
def lineInCubic (S : (PureU1 (2 * n.succ)).LinSols) : Prop :=
|
||||
∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = Pa g f) (a b : ℚ) ,
|
||||
accCube (2 * n.succ) (a • P g + b • P! f) = 0
|
||||
|
||||
lemma lineInCubic_expand {S : (PureU1 (2 * n.succ)).LinSols} (h : lineInCubic S) :
|
||||
∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = Pa g f) (a b : ℚ) ,
|
||||
3 * a * b * (a * accCubeTriLinSymm (P g, P g, P! f)
|
||||
+ b * accCubeTriLinSymm (P! f, P! f, P g)) = 0 := by
|
||||
intro g f hS a b
|
||||
have h1 := h g f hS a b
|
||||
change accCubeTriLinSymm.toCubic (a • P g + b • P! f) = 0 at h1
|
||||
simp only [TriLinearSymm.toCubic_add] at h1
|
||||
simp only [HomogeneousCubic.map_smul,
|
||||
accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂, accCubeTriLinSymm.map_smul₃] at h1
|
||||
erw [P_accCube, P!_accCube] at h1
|
||||
rw [← h1]
|
||||
ring
|
||||
|
||||
/--
|
||||
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`.
|
||||
-/
|
||||
lemma line_in_cubic_P_P_P! {S : (PureU1 (2 * n.succ)).LinSols} (h : lineInCubic S) :
|
||||
∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = P g + P! f),
|
||||
accCubeTriLinSymm (P g, P g, P! f) = 0 := by
|
||||
intro g f hS
|
||||
linear_combination 2 / 3 * (lineInCubic_expand h g f hS 1 1) -
|
||||
(lineInCubic_expand h g f hS 1 2) / 6
|
||||
|
||||
/-- We say a `LinSol` satifies `lineInCubicPerm` if all its permutations satsify `lineInCubic`. -/
|
||||
def lineInCubicPerm (S : (PureU1 (2 * n.succ)).LinSols) : Prop :=
|
||||
∀ (M : (FamilyPermutations (2 * n.succ)).group ),
|
||||
lineInCubic ((FamilyPermutations (2 * n.succ)).linSolRep M S)
|
||||
|
||||
/-- If `lineInCubicPerm S` then `lineInCubic S`. -/
|
||||
lemma lineInCubicPerm_self {S : (PureU1 (2 * n.succ)).LinSols}
|
||||
(hS : lineInCubicPerm S) : lineInCubic S := hS 1
|
||||
|
||||
/-- If `lineInCubicPerm S` then `lineInCubicPerm (M S)` for all permutations `M`. -/
|
||||
lemma lineInCubicPerm_permute {S : (PureU1 (2 * n.succ)).LinSols}
|
||||
(hS : lineInCubicPerm S) (M' : (FamilyPermutations (2 * n.succ)).group) :
|
||||
lineInCubicPerm ((FamilyPermutations (2 * n.succ)).linSolRep M' S) := by
|
||||
rw [lineInCubicPerm]
|
||||
intro M
|
||||
change lineInCubic
|
||||
(((FamilyPermutations (2 * n.succ)).linSolRep M * (FamilyPermutations (2 * n.succ)).linSolRep M') S)
|
||||
erw [← (FamilyPermutations (2 * n.succ)).linSolRep.map_mul M M']
|
||||
exact hS (M * M')
|
||||
|
||||
lemma lineInCubicPerm_swap {S : (PureU1 (2 * n.succ)).LinSols}
|
||||
(LIC : lineInCubicPerm S) :
|
||||
∀ (j : Fin n) (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = Pa g f) ,
|
||||
(S.val (δ!₂ j) - S.val (δ!₁ j))
|
||||
* accCubeTriLinSymm.toFun (P g, P g, basis!AsCharges j) = 0 := by
|
||||
intro j g f h
|
||||
let S' := (FamilyPermutations (2 * n.succ)).linSolRep (pairSwap (δ!₁ j) (δ!₂ j)) S
|
||||
have hSS' : ((FamilyPermutations (2 * n.succ)).linSolRep (pairSwap (δ!₁ j) (δ!₂ j))) S = S' := rfl
|
||||
obtain ⟨g', f', hall⟩ := span_basis_swap! j hSS' g f h
|
||||
have h1 := line_in_cubic_P_P_P! (lineInCubicPerm_self LIC) g f h
|
||||
have h2 := line_in_cubic_P_P_P!
|
||||
(lineInCubicPerm_self (lineInCubicPerm_permute LIC (pairSwap (δ!₁ j) (δ!₂ j)))) g' f' hall.1
|
||||
rw [hall.2.1, hall.2.2] at h2
|
||||
rw [accCubeTriLinSymm.map_add₃, h1, accCubeTriLinSymm.map_smul₃] at h2
|
||||
simpa using h2
|
||||
|
||||
lemma P_P_P!_accCube' {S : (PureU1 (2 * n.succ.succ )).LinSols}
|
||||
(f : Fin n.succ.succ → ℚ) (g : Fin n.succ → ℚ) (hS : S.val = Pa f g) :
|
||||
accCubeTriLinSymm.toFun (P f, P f, basis!AsCharges (Fin.last n)) =
|
||||
- (S.val (δ!₂ (Fin.last n)) + S.val (δ!₁ (Fin.last n))) * (2 * S.val δ!₄ +
|
||||
S.val (δ!₂ (Fin.last n)) + S.val (δ!₁ (Fin.last n))) := by
|
||||
rw [P_P_P!_accCube f (Fin.last n)]
|
||||
have h1 := Pa_δ!₄ f g
|
||||
have h2 := Pa_δ!₁ f g (Fin.last n)
|
||||
have h3 := Pa_δ!₂ f g (Fin.last n)
|
||||
simp at h1 h2 h3
|
||||
have hl : f (Fin.succ (Fin.last (n ))) = - Pa f g δ!₄ := by
|
||||
simp_all only [Fin.succ_last, neg_neg]
|
||||
erw [hl] at h2
|
||||
have hg : g (Fin.last n) = Pa f g (δ!₁ (Fin.last n)) + Pa f g δ!₄ := by
|
||||
linear_combination -(1 * h2)
|
||||
have hll : f (Fin.castSucc (Fin.last (n ))) =
|
||||
- (Pa f g (δ!₂ (Fin.last n)) + Pa f g (δ!₁ (Fin.last n)) + Pa f g δ!₄) := by
|
||||
linear_combination h3 - 1 * hg
|
||||
rw [← hS] at hl hll
|
||||
rw [hl, hll]
|
||||
ring
|
||||
|
||||
lemma lineInCubicPerm_last_cond {S : (PureU1 (2 * n.succ.succ)).LinSols}
|
||||
(LIC : lineInCubicPerm S) :
|
||||
lineInPlaneProp
|
||||
((S.val (δ!₂ (Fin.last n))), ((S.val (δ!₁ (Fin.last n))), (S.val δ!₄))) := by
|
||||
obtain ⟨g, f, hfg⟩ := span_basis S
|
||||
have h1 := lineInCubicPerm_swap LIC (Fin.last n) g f hfg
|
||||
rw [P_P_P!_accCube' g f hfg] at h1
|
||||
simp at h1
|
||||
cases h1 <;> rename_i h1
|
||||
apply Or.inl
|
||||
linear_combination h1
|
||||
cases h1 <;> rename_i h1
|
||||
apply Or.inr
|
||||
apply Or.inl
|
||||
linear_combination -(1 * h1)
|
||||
apply Or.inr
|
||||
apply Or.inr
|
||||
exact h1
|
||||
|
||||
lemma lineInCubicPerm_last_perm {S : (PureU1 (2 * n.succ.succ)).LinSols}
|
||||
(LIC : lineInCubicPerm S) : lineInPlaneCond S := by
|
||||
refine @Prop_three (2 * n.succ.succ) lineInPlaneProp S (δ!₂ (Fin.last n)) (δ!₁ (Fin.last n))
|
||||
δ!₄ ?_ ?_ ?_ ?_
|
||||
simp [Fin.ext_iff, δ!₂, δ!₁]
|
||||
simp [Fin.ext_iff, δ!₂, δ!₄]
|
||||
simp [Fin.ext_iff, δ!₁, δ!₄]
|
||||
omega
|
||||
intro M
|
||||
exact lineInCubicPerm_last_cond (lineInCubicPerm_permute LIC M)
|
||||
|
||||
lemma lineInCubicPerm_constAbs {S : (PureU1 (2 * n.succ.succ)).Sols}
|
||||
(LIC : lineInCubicPerm S.1.1) : constAbs S.val :=
|
||||
linesInPlane_constAbs_AF S (lineInCubicPerm_last_perm LIC)
|
||||
|
||||
theorem lineInCubicPerm_vectorLike {S : (PureU1 (2 * n.succ.succ)).Sols}
|
||||
(LIC : lineInCubicPerm S.1.1) : vectorLikeEven S.val :=
|
||||
ConstAbs.boundary_value_even S.1.1 (lineInCubicPerm_constAbs LIC)
|
||||
|
||||
theorem lineInCubicPerm_in_plane (S : (PureU1 (2 * n.succ.succ)).Sols)
|
||||
(LIC : lineInCubicPerm S.1.1) : ∃ (M : (FamilyPermutations (2 * n.succ.succ)).group),
|
||||
(FamilyPermutations (2 * n.succ.succ)).linSolRep M S.1.1
|
||||
∈ Submodule.span ℚ (Set.range basis) :=
|
||||
vectorLikeEven_in_span S.1.1 (lineInCubicPerm_vectorLike LIC)
|
||||
|
||||
end Even
|
||||
end PureU1
|
||||
173
HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
Normal file
173
HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
Normal file
|
|
@ -0,0 +1,173 @@
|
|||
/-
|
||||
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
|
||||
Released under Apache 2.0 license.
|
||||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import HepLean.AnomalyCancellation.PureU1.Basic
|
||||
import HepLean.AnomalyCancellation.PureU1.Permutations
|
||||
import HepLean.AnomalyCancellation.PureU1.VectorLike
|
||||
import HepLean.AnomalyCancellation.PureU1.ConstAbs
|
||||
import HepLean.AnomalyCancellation.PureU1.LineInPlaneCond
|
||||
import HepLean.AnomalyCancellation.PureU1.Odd.BasisLinear
|
||||
import Mathlib.Tactic.Polyrith
|
||||
import Mathlib.RepresentationTheory.Basic
|
||||
/-!
|
||||
|
||||
# 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 baisis of
|
||||
`LinSols` lies in the cubic.
|
||||
|
||||
We show that for a solution all its permutations satsfiy this property,
|
||||
then the charge must be zero.
|
||||
|
||||
The main reference for this file is:
|
||||
|
||||
- https://arxiv.org/pdf/1912.04804.pdf
|
||||
-/
|
||||
namespace PureU1
|
||||
namespace Odd
|
||||
|
||||
open BigOperators
|
||||
|
||||
variable {n : ℕ}
|
||||
open VectorLikeOddPlane
|
||||
|
||||
/-- A property on `LinSols`, statified if every point on the line between the two planes
|
||||
in the basis through that point is in the cubic. -/
|
||||
def lineInCubic (S : (PureU1 (2 * n + 1)).LinSols) : Prop :=
|
||||
∀ (g f : Fin n → ℚ) (_ : S.val = Pa g f) (a b : ℚ) ,
|
||||
accCube (2 * n + 1) (a • P g + b • P! f) = 0
|
||||
|
||||
lemma lineInCubic_expand {S : (PureU1 (2 * n + 1)).LinSols} (h : lineInCubic S) :
|
||||
∀ (g : Fin n → ℚ) (f : Fin n → ℚ) (_ : S.val = P g + P! f) (a b : ℚ) ,
|
||||
3 * a * b * (a * accCubeTriLinSymm (P g, P g, P! f)
|
||||
+ b * accCubeTriLinSymm (P! f, P! f, P g)) = 0 := by
|
||||
intro g f hS a b
|
||||
have h1 := h g f hS a b
|
||||
change accCubeTriLinSymm.toCubic (a • P g + b • P! f) = 0 at h1
|
||||
simp only [TriLinearSymm.toCubic_add] at h1
|
||||
simp only [HomogeneousCubic.map_smul,
|
||||
accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂, accCubeTriLinSymm.map_smul₃] at h1
|
||||
erw [P_accCube, P!_accCube] at h1
|
||||
rw [← h1]
|
||||
ring
|
||||
|
||||
|
||||
lemma line_in_cubic_P_P_P! {S : (PureU1 (2 * n + 1)).LinSols} (h : lineInCubic S) :
|
||||
∀ (g : Fin n → ℚ) (f : Fin n → ℚ) (_ : S.val = P g + P! f),
|
||||
accCubeTriLinSymm (P g, P g, P! f) = 0 := by
|
||||
intro g f hS
|
||||
linear_combination 2 / 3 * (lineInCubic_expand h g f hS 1 1 ) -
|
||||
(lineInCubic_expand h g f hS 1 2 ) / 6
|
||||
|
||||
|
||||
|
||||
/-- We say a `LinSol` satifies `lineInCubicPerm` if all its permutations satsify `lineInCubic`. -/
|
||||
def lineInCubicPerm (S : (PureU1 (2 * n + 1)).LinSols) : Prop :=
|
||||
∀ (M : (FamilyPermutations (2 * n + 1)).group ),
|
||||
lineInCubic ((FamilyPermutations (2 * n + 1)).linSolRep M S)
|
||||
|
||||
/-- If `lineInCubicPerm S` then `lineInCubic S`. -/
|
||||
lemma lineInCubicPerm_self {S : (PureU1 (2 * n + 1)).LinSols} (hS : lineInCubicPerm S) :
|
||||
lineInCubic S := hS 1
|
||||
|
||||
/-- If `lineInCubicPerm S` then `lineInCubicPerm (M S)` for all permutations `M`. -/
|
||||
lemma lineInCubicPerm_permute {S : (PureU1 (2 * n + 1)).LinSols}
|
||||
(hS : lineInCubicPerm S) (M' : (FamilyPermutations (2 * n + 1)).group) :
|
||||
lineInCubicPerm ((FamilyPermutations (2 * n + 1)).linSolRep M' S) := by
|
||||
rw [lineInCubicPerm]
|
||||
intro M
|
||||
have ht : ((FamilyPermutations (2 * n + 1)).linSolRep M)
|
||||
((FamilyPermutations (2 * n + 1)).linSolRep M' S)
|
||||
= (FamilyPermutations (2 * n + 1)).linSolRep (M * M') S := by
|
||||
simp [(FamilyPermutations (2 * n.succ)).linSolRep.map_mul']
|
||||
rw [ht]
|
||||
exact hS (M * M')
|
||||
|
||||
|
||||
lemma lineInCubicPerm_swap {S : (PureU1 (2 * n.succ + 1)).LinSols}
|
||||
(LIC : lineInCubicPerm S) :
|
||||
∀ (j : Fin n.succ) (g f : Fin n.succ → ℚ) (_ : S.val = Pa g f) ,
|
||||
(S.val (δ!₂ j) - S.val (δ!₁ j))
|
||||
* accCubeTriLinSymm.toFun (P g, P g, basis!AsCharges j) = 0 := by
|
||||
intro j g f h
|
||||
let S' := (FamilyPermutations (2 * n.succ + 1)).linSolRep
|
||||
(pairSwap (δ!₁ j) (δ!₂ j)) S
|
||||
have hSS' : ((FamilyPermutations (2 * n.succ + 1)).linSolRep
|
||||
(pairSwap (δ!₁ j) (δ!₂ j))) S = S' := rfl
|
||||
obtain ⟨g', f', hall⟩ := span_basis_swap! j hSS' g f h
|
||||
have h1 := line_in_cubic_P_P_P! (lineInCubicPerm_self LIC) g f h
|
||||
have h2 := line_in_cubic_P_P_P!
|
||||
(lineInCubicPerm_self (lineInCubicPerm_permute LIC (pairSwap (δ!₁ j) (δ!₂ j)))) g' f' hall.1
|
||||
rw [hall.2.1, hall.2.2] at h2
|
||||
rw [accCubeTriLinSymm.map_add₃, h1, accCubeTriLinSymm.map_smul₃] at h2
|
||||
simpa using h2
|
||||
|
||||
lemma P_P_P!_accCube' {S : (PureU1 (2 * n.succ.succ + 1)).LinSols}
|
||||
(f g : Fin n.succ.succ → ℚ) (hS : S.val = Pa f g) :
|
||||
accCubeTriLinSymm.toFun (P f, P f, basis!AsCharges 0) =
|
||||
(S.val (δ!₁ 0) + S.val (δ!₂ 0)) * (2 * S.val δ!₃ + S.val (δ!₁ 0) + S.val (δ!₂ 0)) := by
|
||||
rw [P_P_P!_accCube f 0]
|
||||
rw [← Pa_δa₁ f g]
|
||||
rw [← hS]
|
||||
have ht : δ!₁ (0 : Fin n.succ.succ) = δ₁ 1 := by
|
||||
simp [δ!₁, δ₁]
|
||||
rw [Fin.ext_iff]
|
||||
simp
|
||||
nth_rewrite 1 [ht]
|
||||
rw [P_δ₁]
|
||||
have h1 := Pa_δa₁ f g
|
||||
have h4 := Pa_δa₄ f g 0
|
||||
have h2 := Pa_δa₂ f g 0
|
||||
rw [← hS] at h1 h2 h4
|
||||
simp at h2
|
||||
have h5 : f 1 = S.val (δa₂ 0) + S.val δa₁ + S.val (δa₄ 0):= by
|
||||
linear_combination -(1 * h1) - 1 * h4 - 1 * h2
|
||||
rw [h5]
|
||||
rw [δa₄_δ!₂]
|
||||
have h0 : (δa₂ (0 : Fin n.succ)) = δ!₁ 0 := by
|
||||
rw [δa₂_δ!₁]
|
||||
simp
|
||||
rw [h0, δa₁_δ!₃]
|
||||
ring
|
||||
|
||||
lemma lineInCubicPerm_last_cond {S : (PureU1 (2 * n.succ.succ+1)).LinSols}
|
||||
(LIC : lineInCubicPerm S) :
|
||||
lineInPlaneProp ((S.val (δ!₂ 0)), ((S.val (δ!₁ 0)), (S.val δ!₃))) := by
|
||||
obtain ⟨g, f, hfg⟩ := span_basis S
|
||||
have h1 := lineInCubicPerm_swap LIC 0 g f hfg
|
||||
rw [P_P_P!_accCube' g f hfg] at h1
|
||||
simp at h1
|
||||
cases h1 <;> rename_i h1
|
||||
apply Or.inl
|
||||
linear_combination h1
|
||||
cases h1 <;> rename_i h1
|
||||
apply Or.inr
|
||||
apply Or.inl
|
||||
linear_combination h1
|
||||
apply Or.inr
|
||||
apply Or.inr
|
||||
linear_combination h1
|
||||
|
||||
lemma lineInCubicPerm_last_perm {S : (PureU1 (2 * n.succ.succ + 1)).LinSols}
|
||||
(LIC : lineInCubicPerm S) : lineInPlaneCond S := by
|
||||
refine @Prop_three (2 * n.succ.succ + 1) lineInPlaneProp S (δ!₂ 0) (δ!₁ 0)
|
||||
δ!₃ ?_ ?_ ?_ ?_
|
||||
simp [Fin.ext_iff, δ!₂, δ!₁]
|
||||
simp [Fin.ext_iff, δ!₂, δ!₃]
|
||||
simp [Fin.ext_iff, δ!₁, δ!₃]
|
||||
intro M
|
||||
exact lineInCubicPerm_last_cond (lineInCubicPerm_permute LIC M)
|
||||
|
||||
lemma lineInCubicPerm_constAbs {S : (PureU1 (2 * n.succ.succ + 1)).LinSols}
|
||||
(LIC : lineInCubicPerm S) : constAbs S.val :=
|
||||
linesInPlane_constAbs (lineInCubicPerm_last_perm LIC)
|
||||
|
||||
theorem lineInCubicPerm_zero {S : (PureU1 (2 * n.succ.succ + 1)).LinSols}
|
||||
(LIC : lineInCubicPerm S) : S = 0 :=
|
||||
ConstAbs.boundary_value_odd S (lineInCubicPerm_constAbs LIC)
|
||||
|
||||
end Odd
|
||||
end PureU1
|
||||
Loading…
Add table
Add a link
Reference in a new issue