DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor: Move files and update toml

Browse source
This commit is contained in:
jstoobysmith 2025-02-14 08:45:02 +00:00
parent a957bb484c
commit 49ec0b6ea7
220 changed files with 832 additions and 832 deletions
Download patch file Download diff file Expand all files Collapse all files

213
HepLean.lean
View file

@ -1,213 +0,0 @@
import HepLean.AnomalyCancellation.Basic
import HepLean.AnomalyCancellation.GroupActions
import HepLean.AnomalyCancellation.MSSMNu.B3
import HepLean.AnomalyCancellation.MSSMNu.Basic
import HepLean.AnomalyCancellation.MSSMNu.HyperCharge
import HepLean.AnomalyCancellation.MSSMNu.LineY3B3
import HepLean.AnomalyCancellation.MSSMNu.OrthogY3B3.Basic
import HepLean.AnomalyCancellation.MSSMNu.OrthogY3B3.PlaneWithY3B3
import HepLean.AnomalyCancellation.MSSMNu.OrthogY3B3.ToSols
import HepLean.AnomalyCancellation.MSSMNu.Permutations
import HepLean.AnomalyCancellation.MSSMNu.Y3
import HepLean.AnomalyCancellation.PureU1.Basic
import HepLean.AnomalyCancellation.PureU1.BasisLinear
import HepLean.AnomalyCancellation.PureU1.ConstAbs
import HepLean.AnomalyCancellation.PureU1.Even.BasisLinear
import HepLean.AnomalyCancellation.PureU1.Even.LineInCubic
import HepLean.AnomalyCancellation.PureU1.Even.Parameterization
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.Odd.Parameterization
import HepLean.AnomalyCancellation.PureU1.Permutations
import HepLean.AnomalyCancellation.PureU1.Sorts
import HepLean.AnomalyCancellation.PureU1.VectorLike
import HepLean.AnomalyCancellation.SM.Basic
import HepLean.AnomalyCancellation.SM.FamilyMaps
import HepLean.AnomalyCancellation.SM.NoGrav.Basic
import HepLean.AnomalyCancellation.SM.NoGrav.One.Lemmas
import HepLean.AnomalyCancellation.SM.NoGrav.One.LinearParameterization
import HepLean.AnomalyCancellation.SM.Permutations
import HepLean.AnomalyCancellation.SMNu.Basic
import HepLean.AnomalyCancellation.SMNu.FamilyMaps
import HepLean.AnomalyCancellation.SMNu.NoGrav.Basic
import HepLean.AnomalyCancellation.SMNu.Ordinary.Basic
import HepLean.AnomalyCancellation.SMNu.Ordinary.DimSevenPlane
import HepLean.AnomalyCancellation.SMNu.Ordinary.FamilyMaps
import HepLean.AnomalyCancellation.SMNu.Permutations
import HepLean.AnomalyCancellation.SMNu.PlusU1.BMinusL
import HepLean.AnomalyCancellation.SMNu.PlusU1.Basic
import HepLean.AnomalyCancellation.SMNu.PlusU1.BoundPlaneDim
import HepLean.AnomalyCancellation.SMNu.PlusU1.FamilyMaps
import HepLean.AnomalyCancellation.SMNu.PlusU1.HyperCharge
import HepLean.AnomalyCancellation.SMNu.PlusU1.PlaneNonSols
import HepLean.AnomalyCancellation.SMNu.PlusU1.QuadSol
import HepLean.AnomalyCancellation.SMNu.PlusU1.QuadSolToSol
import HepLean.BeyondTheStandardModel.GeorgiGlashow.Basic
import HepLean.BeyondTheStandardModel.PatiSalam.Basic
import HepLean.BeyondTheStandardModel.Spin10.Basic
import HepLean.BeyondTheStandardModel.TwoHDM.Basic
import HepLean.BeyondTheStandardModel.TwoHDM.GaugeOrbits
import HepLean.FlavorPhysics.CKMMatrix.Basic
import HepLean.FlavorPhysics.CKMMatrix.Invariants
import HepLean.FlavorPhysics.CKMMatrix.PhaseFreedom
import HepLean.FlavorPhysics.CKMMatrix.Relations
import HepLean.FlavorPhysics.CKMMatrix.Rows
import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.Basic
import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.StandardParameters
import HepLean.Lorentz.Algebra.Basic
import HepLean.Lorentz.Algebra.Basis
import HepLean.Lorentz.ComplexTensor.Basic
import HepLean.Lorentz.ComplexTensor.Basis
import HepLean.Lorentz.ComplexTensor.Bispinors.Basic
import HepLean.Lorentz.ComplexTensor.Lemmas
import HepLean.Lorentz.ComplexTensor.Metrics.Basic
import HepLean.Lorentz.ComplexTensor.Metrics.Basis
import HepLean.Lorentz.ComplexTensor.Metrics.Lemmas
import HepLean.Lorentz.ComplexTensor.PauliMatrices.Basic
import HepLean.Lorentz.ComplexTensor.PauliMatrices.Basis
import HepLean.Lorentz.ComplexTensor.PauliMatrices.CoContractContr
import HepLean.Lorentz.ComplexTensor.Units.Basic
import HepLean.Lorentz.ComplexTensor.Units.Symm
import HepLean.Lorentz.ComplexVector.Basic
import HepLean.Lorentz.ComplexVector.Contraction
import HepLean.Lorentz.ComplexVector.Metric
import HepLean.Lorentz.ComplexVector.Modules
import HepLean.Lorentz.ComplexVector.Two
import HepLean.Lorentz.ComplexVector.Unit
import HepLean.Lorentz.Group.Basic
import HepLean.Lorentz.Group.Boosts
import HepLean.Lorentz.Group.Orthochronous
import HepLean.Lorentz.Group.Proper
import HepLean.Lorentz.Group.Restricted
import HepLean.Lorentz.Group.Rotations
import HepLean.Lorentz.MinkowskiMatrix
import HepLean.Lorentz.PauliMatrices.AsTensor
import HepLean.Lorentz.PauliMatrices.Basic
import HepLean.Lorentz.PauliMatrices.SelfAdjoint
import HepLean.Lorentz.RealVector.Basic
import HepLean.Lorentz.RealVector.Contraction
import HepLean.Lorentz.RealVector.Modules
import HepLean.Lorentz.RealVector.NormOne
import HepLean.Lorentz.SL2C.Basic
import HepLean.Lorentz.SL2C.SelfAdjoint
import HepLean.Lorentz.Weyl.Basic
import HepLean.Lorentz.Weyl.Contraction
import HepLean.Lorentz.Weyl.Metric
import HepLean.Lorentz.Weyl.Modules
import HepLean.Lorentz.Weyl.Two
import HepLean.Lorentz.Weyl.Unit
import HepLean.Mathematics.Fin
import HepLean.Mathematics.Fin.Involutions
import HepLean.Mathematics.LinearMaps
import HepLean.Mathematics.List
import HepLean.Mathematics.List.InsertIdx
import HepLean.Mathematics.List.InsertionSort
import HepLean.Mathematics.PiTensorProduct
import HepLean.Mathematics.SO3.Basic
import HepLean.Mathematics.SchurTriangulation
import HepLean.Meta.AllFilePaths
import HepLean.Meta.Basic
import HepLean.Meta.Informal.Basic
import HepLean.Meta.Informal.Post
import HepLean.Meta.Notes.Basic
import HepLean.Meta.Notes.HTMLNote
import HepLean.Meta.Notes.NoteFile
import HepLean.Meta.Notes.ToHTML
import HepLean.Meta.Remark.Basic
import HepLean.Meta.Remark.Properties
import HepLean.Meta.TODO.Basic
import HepLean.Meta.TransverseTactics
import HepLean.PerturbationTheory.CreateAnnihilate
import HepLean.PerturbationTheory.FeynmanDiagrams.Basic
import HepLean.PerturbationTheory.FeynmanDiagrams.Instances.ComplexScalar
import HepLean.PerturbationTheory.FeynmanDiagrams.Instances.Phi4
import HepLean.PerturbationTheory.FeynmanDiagrams.Momentum
import HepLean.PerturbationTheory.FieldOpAlgebra.Basic
import HepLean.PerturbationTheory.FieldOpAlgebra.Grading
import HepLean.PerturbationTheory.FieldOpAlgebra.NormalOrder.Basic
import HepLean.PerturbationTheory.FieldOpAlgebra.NormalOrder.Lemmas
import HepLean.PerturbationTheory.FieldOpAlgebra.NormalOrder.WickContractions
import HepLean.PerturbationTheory.FieldOpAlgebra.StaticWickTerm
import HepLean.PerturbationTheory.FieldOpAlgebra.StaticWickTheorem
import HepLean.PerturbationTheory.FieldOpAlgebra.SuperCommute
import HepLean.PerturbationTheory.FieldOpAlgebra.TimeContraction
import HepLean.PerturbationTheory.FieldOpAlgebra.TimeOrder
import HepLean.PerturbationTheory.FieldOpAlgebra.Universality
import HepLean.PerturbationTheory.FieldOpAlgebra.WickTerm
import HepLean.PerturbationTheory.FieldOpAlgebra.WicksTheorem
import HepLean.PerturbationTheory.FieldOpAlgebra.WicksTheoremNormal
import HepLean.PerturbationTheory.FieldOpFreeAlgebra.Basic
import HepLean.PerturbationTheory.FieldOpFreeAlgebra.Grading
import HepLean.PerturbationTheory.FieldOpFreeAlgebra.NormTimeOrder
import HepLean.PerturbationTheory.FieldOpFreeAlgebra.NormalOrder
import HepLean.PerturbationTheory.FieldOpFreeAlgebra.SuperCommute
import HepLean.PerturbationTheory.FieldOpFreeAlgebra.TimeOrder
import HepLean.PerturbationTheory.FieldSpecification.Basic
import HepLean.PerturbationTheory.FieldSpecification.CrAnFieldOp
import HepLean.PerturbationTheory.FieldSpecification.CrAnSection
import HepLean.PerturbationTheory.FieldSpecification.Filters
import HepLean.PerturbationTheory.FieldSpecification.NormalOrder
import HepLean.PerturbationTheory.FieldSpecification.TimeOrder
import HepLean.PerturbationTheory.FieldStatistics.Basic
import HepLean.PerturbationTheory.FieldStatistics.ExchangeSign
import HepLean.PerturbationTheory.FieldStatistics.OfFinset
import HepLean.PerturbationTheory.Koszul.KoszulSign
import HepLean.PerturbationTheory.Koszul.KoszulSignInsert
import HepLean.PerturbationTheory.WickContraction.Basic
import HepLean.PerturbationTheory.WickContraction.Card
import HepLean.PerturbationTheory.WickContraction.Erase
import HepLean.PerturbationTheory.WickContraction.ExtractEquiv
import HepLean.PerturbationTheory.WickContraction.InsertAndContract
import HepLean.PerturbationTheory.WickContraction.InsertAndContractNat
import HepLean.PerturbationTheory.WickContraction.Involutions
import HepLean.PerturbationTheory.WickContraction.IsFull
import HepLean.PerturbationTheory.WickContraction.Join
import HepLean.PerturbationTheory.WickContraction.Sign.Basic
import HepLean.PerturbationTheory.WickContraction.Sign.InsertNone
import HepLean.PerturbationTheory.WickContraction.Sign.InsertSome
import HepLean.PerturbationTheory.WickContraction.Sign.Join
import HepLean.PerturbationTheory.WickContraction.Singleton
import HepLean.PerturbationTheory.WickContraction.StaticContract
import HepLean.PerturbationTheory.WickContraction.SubContraction
import HepLean.PerturbationTheory.WickContraction.TimeCond
import HepLean.PerturbationTheory.WickContraction.TimeContract
import HepLean.PerturbationTheory.WickContraction.Uncontracted
import HepLean.PerturbationTheory.WickContraction.UncontractedList
import HepLean.SpaceTime.Basic
import HepLean.SpaceTime.CliffordAlgebra
import HepLean.StandardModel.Basic
import HepLean.StandardModel.HiggsBoson.Basic
import HepLean.StandardModel.HiggsBoson.GaugeAction
import HepLean.StandardModel.HiggsBoson.PointwiseInnerProd
import HepLean.StandardModel.HiggsBoson.Potential
import HepLean.StandardModel.Representations
import HepLean.Tensors.OverColor.Basic
import HepLean.Tensors.OverColor.Discrete
import HepLean.Tensors.OverColor.Functors
import HepLean.Tensors.OverColor.Iso
import HepLean.Tensors.OverColor.Lift
import HepLean.Tensors.TensorSpecies.Basic
import HepLean.Tensors.TensorSpecies.Contractions.Basic
import HepLean.Tensors.TensorSpecies.Contractions.Categorical
import HepLean.Tensors.TensorSpecies.Contractions.ContrMap
import HepLean.Tensors.TensorSpecies.DualRepIso
import HepLean.Tensors.TensorSpecies.MetricTensor
import HepLean.Tensors.TensorSpecies.Pure
import HepLean.Tensors.TensorSpecies.UnitTensor
import HepLean.Tensors.Tree.Basic
import HepLean.Tensors.Tree.Dot
import HepLean.Tensors.Tree.Elab
import HepLean.Tensors.Tree.NodeIdentities.Assoc
import HepLean.Tensors.Tree.NodeIdentities.Basic
import HepLean.Tensors.Tree.NodeIdentities.Congr
import HepLean.Tensors.Tree.NodeIdentities.ContrContr
import HepLean.Tensors.Tree.NodeIdentities.ContrSwap
import HepLean.Tensors.Tree.NodeIdentities.PermContr
import HepLean.Tensors.Tree.NodeIdentities.PermProd
import HepLean.Tensors.Tree.NodeIdentities.ProdAssoc
import HepLean.Tensors.Tree.NodeIdentities.ProdComm
import HepLean.Tensors.Tree.NodeIdentities.ProdContr

213
PhysLean.lean Normal file
View file

@ -0,0 +1,213 @@
import PhysLean.AnomalyCancellation.Basic
import PhysLean.AnomalyCancellation.GroupActions
import PhysLean.AnomalyCancellation.MSSMNu.B3
import PhysLean.AnomalyCancellation.MSSMNu.Basic
import PhysLean.AnomalyCancellation.MSSMNu.HyperCharge
import PhysLean.AnomalyCancellation.MSSMNu.LineY3B3
import PhysLean.AnomalyCancellation.MSSMNu.OrthogY3B3.Basic
import PhysLean.AnomalyCancellation.MSSMNu.OrthogY3B3.PlaneWithY3B3
import PhysLean.AnomalyCancellation.MSSMNu.OrthogY3B3.ToSols
import PhysLean.AnomalyCancellation.MSSMNu.Permutations
import PhysLean.AnomalyCancellation.MSSMNu.Y3
import PhysLean.AnomalyCancellation.PureU1.Basic
import PhysLean.AnomalyCancellation.PureU1.BasisLinear
import PhysLean.AnomalyCancellation.PureU1.ConstAbs
import PhysLean.AnomalyCancellation.PureU1.Even.BasisLinear
import PhysLean.AnomalyCancellation.PureU1.Even.LineInCubic
import PhysLean.AnomalyCancellation.PureU1.Even.Parameterization
import PhysLean.AnomalyCancellation.PureU1.LineInPlaneCond
import PhysLean.AnomalyCancellation.PureU1.LowDim.One
import PhysLean.AnomalyCancellation.PureU1.LowDim.Three
import PhysLean.AnomalyCancellation.PureU1.LowDim.Two
import PhysLean.AnomalyCancellation.PureU1.Odd.BasisLinear
import PhysLean.AnomalyCancellation.PureU1.Odd.LineInCubic
import PhysLean.AnomalyCancellation.PureU1.Odd.Parameterization
import PhysLean.AnomalyCancellation.PureU1.Permutations
import PhysLean.AnomalyCancellation.PureU1.Sorts
import PhysLean.AnomalyCancellation.PureU1.VectorLike
import PhysLean.AnomalyCancellation.SM.Basic
import PhysLean.AnomalyCancellation.SM.FamilyMaps
import PhysLean.AnomalyCancellation.SM.NoGrav.Basic
import PhysLean.AnomalyCancellation.SM.NoGrav.One.Lemmas
import PhysLean.AnomalyCancellation.SM.NoGrav.One.LinearParameterization
import PhysLean.AnomalyCancellation.SM.Permutations
import PhysLean.AnomalyCancellation.SMNu.Basic
import PhysLean.AnomalyCancellation.SMNu.FamilyMaps
import PhysLean.AnomalyCancellation.SMNu.NoGrav.Basic
import PhysLean.AnomalyCancellation.SMNu.Ordinary.Basic
import PhysLean.AnomalyCancellation.SMNu.Ordinary.DimSevenPlane
import PhysLean.AnomalyCancellation.SMNu.Ordinary.FamilyMaps
import PhysLean.AnomalyCancellation.SMNu.Permutations
import PhysLean.AnomalyCancellation.SMNu.PlusU1.BMinusL
import PhysLean.AnomalyCancellation.SMNu.PlusU1.Basic
import PhysLean.AnomalyCancellation.SMNu.PlusU1.BoundPlaneDim
import PhysLean.AnomalyCancellation.SMNu.PlusU1.FamilyMaps
import PhysLean.AnomalyCancellation.SMNu.PlusU1.HyperCharge
import PhysLean.AnomalyCancellation.SMNu.PlusU1.PlaneNonSols
import PhysLean.AnomalyCancellation.SMNu.PlusU1.QuadSol
import PhysLean.AnomalyCancellation.SMNu.PlusU1.QuadSolToSol
import PhysLean.BeyondTheStandardModel.GeorgiGlashow.Basic
import PhysLean.BeyondTheStandardModel.PatiSalam.Basic
import PhysLean.BeyondTheStandardModel.Spin10.Basic
import PhysLean.BeyondTheStandardModel.TwoHDM.Basic
import PhysLean.BeyondTheStandardModel.TwoHDM.GaugeOrbits
import PhysLean.FlavorPhysics.CKMMatrix.Basic
import PhysLean.FlavorPhysics.CKMMatrix.Invariants
import PhysLean.FlavorPhysics.CKMMatrix.PhaseFreedom
import PhysLean.FlavorPhysics.CKMMatrix.Relations
import PhysLean.FlavorPhysics.CKMMatrix.Rows
import PhysLean.FlavorPhysics.CKMMatrix.StandardParameterization.Basic
import PhysLean.FlavorPhysics.CKMMatrix.StandardParameterization.StandardParameters
import PhysLean.Lorentz.Algebra.Basic
import PhysLean.Lorentz.Algebra.Basis
import PhysLean.Lorentz.ComplexTensor.Basic
import PhysLean.Lorentz.ComplexTensor.Basis
import PhysLean.Lorentz.ComplexTensor.Bispinors.Basic
import PhysLean.Lorentz.ComplexTensor.Lemmas
import PhysLean.Lorentz.ComplexTensor.Metrics.Basic
import PhysLean.Lorentz.ComplexTensor.Metrics.Basis
import PhysLean.Lorentz.ComplexTensor.Metrics.Lemmas
import PhysLean.Lorentz.ComplexTensor.PauliMatrices.Basic
import PhysLean.Lorentz.ComplexTensor.PauliMatrices.Basis
import PhysLean.Lorentz.ComplexTensor.PauliMatrices.CoContractContr
import PhysLean.Lorentz.ComplexTensor.Units.Basic
import PhysLean.Lorentz.ComplexTensor.Units.Symm
import PhysLean.Lorentz.ComplexVector.Basic
import PhysLean.Lorentz.ComplexVector.Contraction
import PhysLean.Lorentz.ComplexVector.Metric
import PhysLean.Lorentz.ComplexVector.Modules
import PhysLean.Lorentz.ComplexVector.Two
import PhysLean.Lorentz.ComplexVector.Unit
import PhysLean.Lorentz.Group.Basic
import PhysLean.Lorentz.Group.Boosts
import PhysLean.Lorentz.Group.Orthochronous
import PhysLean.Lorentz.Group.Proper
import PhysLean.Lorentz.Group.Restricted
import PhysLean.Lorentz.Group.Rotations
import PhysLean.Lorentz.MinkowskiMatrix
import PhysLean.Lorentz.PauliMatrices.AsTensor
import PhysLean.Lorentz.PauliMatrices.Basic
import PhysLean.Lorentz.PauliMatrices.SelfAdjoint
import PhysLean.Lorentz.RealVector.Basic
import PhysLean.Lorentz.RealVector.Contraction
import PhysLean.Lorentz.RealVector.Modules
import PhysLean.Lorentz.RealVector.NormOne
import PhysLean.Lorentz.SL2C.Basic
import PhysLean.Lorentz.SL2C.SelfAdjoint
import PhysLean.Lorentz.Weyl.Basic
import PhysLean.Lorentz.Weyl.Contraction
import PhysLean.Lorentz.Weyl.Metric
import PhysLean.Lorentz.Weyl.Modules
import PhysLean.Lorentz.Weyl.Two
import PhysLean.Lorentz.Weyl.Unit
import PhysLean.Mathematics.Fin
import PhysLean.Mathematics.Fin.Involutions
import PhysLean.Mathematics.LinearMaps
import PhysLean.Mathematics.List
import PhysLean.Mathematics.List.InsertIdx
import PhysLean.Mathematics.List.InsertionSort
import PhysLean.Mathematics.PiTensorProduct
import PhysLean.Mathematics.SO3.Basic
import PhysLean.Mathematics.SchurTriangulation
import PhysLean.Meta.AllFilePaths
import PhysLean.Meta.Basic
import PhysLean.Meta.Informal.Basic
import PhysLean.Meta.Informal.Post
import PhysLean.Meta.Notes.Basic
import PhysLean.Meta.Notes.HTMLNote
import PhysLean.Meta.Notes.NoteFile
import PhysLean.Meta.Notes.ToHTML
import PhysLean.Meta.Remark.Basic
import PhysLean.Meta.Remark.Properties
import PhysLean.Meta.TODO.Basic
import PhysLean.Meta.TransverseTactics
import PhysLean.PerturbationTheory.CreateAnnihilate
import PhysLean.PerturbationTheory.FeynmanDiagrams.Basic
import PhysLean.PerturbationTheory.FeynmanDiagrams.Instances.ComplexScalar
import PhysLean.PerturbationTheory.FeynmanDiagrams.Instances.Phi4
import PhysLean.PerturbationTheory.FeynmanDiagrams.Momentum
import PhysLean.PerturbationTheory.FieldOpAlgebra.Basic
import PhysLean.PerturbationTheory.FieldOpAlgebra.Grading
import PhysLean.PerturbationTheory.FieldOpAlgebra.NormalOrder.Basic
import PhysLean.PerturbationTheory.FieldOpAlgebra.NormalOrder.Lemmas
import PhysLean.PerturbationTheory.FieldOpAlgebra.NormalOrder.WickContractions
import PhysLean.PerturbationTheory.FieldOpAlgebra.StaticWickTerm
import PhysLean.PerturbationTheory.FieldOpAlgebra.StaticWickTheorem
import PhysLean.PerturbationTheory.FieldOpAlgebra.SuperCommute
import PhysLean.PerturbationTheory.FieldOpAlgebra.TimeContraction
import PhysLean.PerturbationTheory.FieldOpAlgebra.TimeOrder
import PhysLean.PerturbationTheory.FieldOpAlgebra.Universality
import PhysLean.PerturbationTheory.FieldOpAlgebra.WickTerm
import PhysLean.PerturbationTheory.FieldOpAlgebra.WicksTheorem
import PhysLean.PerturbationTheory.FieldOpAlgebra.WicksTheoremNormal
import PhysLean.PerturbationTheory.FieldOpFreeAlgebra.Basic
import PhysLean.PerturbationTheory.FieldOpFreeAlgebra.Grading
import PhysLean.PerturbationTheory.FieldOpFreeAlgebra.NormTimeOrder
import PhysLean.PerturbationTheory.FieldOpFreeAlgebra.NormalOrder
import PhysLean.PerturbationTheory.FieldOpFreeAlgebra.SuperCommute
import PhysLean.PerturbationTheory.FieldOpFreeAlgebra.TimeOrder
import PhysLean.PerturbationTheory.FieldSpecification.Basic
import PhysLean.PerturbationTheory.FieldSpecification.CrAnFieldOp
import PhysLean.PerturbationTheory.FieldSpecification.CrAnSection
import PhysLean.PerturbationTheory.FieldSpecification.Filters
import PhysLean.PerturbationTheory.FieldSpecification.NormalOrder
import PhysLean.PerturbationTheory.FieldSpecification.TimeOrder
import PhysLean.PerturbationTheory.FieldStatistics.Basic
import PhysLean.PerturbationTheory.FieldStatistics.ExchangeSign
import PhysLean.PerturbationTheory.FieldStatistics.OfFinset
import PhysLean.PerturbationTheory.Koszul.KoszulSign
import PhysLean.PerturbationTheory.Koszul.KoszulSignInsert
import PhysLean.PerturbationTheory.WickContraction.Basic
import PhysLean.PerturbationTheory.WickContraction.Card
import PhysLean.PerturbationTheory.WickContraction.Erase
import PhysLean.PerturbationTheory.WickContraction.ExtractEquiv
import PhysLean.PerturbationTheory.WickContraction.InsertAndContract
import PhysLean.PerturbationTheory.WickContraction.InsertAndContractNat
import PhysLean.PerturbationTheory.WickContraction.Involutions
import PhysLean.PerturbationTheory.WickContraction.IsFull
import PhysLean.PerturbationTheory.WickContraction.Join
import PhysLean.PerturbationTheory.WickContraction.Sign.Basic
import PhysLean.PerturbationTheory.WickContraction.Sign.InsertNone
import PhysLean.PerturbationTheory.WickContraction.Sign.InsertSome
import PhysLean.PerturbationTheory.WickContraction.Sign.Join
import PhysLean.PerturbationTheory.WickContraction.Singleton
import PhysLean.PerturbationTheory.WickContraction.StaticContract
import PhysLean.PerturbationTheory.WickContraction.SubContraction
import PhysLean.PerturbationTheory.WickContraction.TimeCond
import PhysLean.PerturbationTheory.WickContraction.TimeContract
import PhysLean.PerturbationTheory.WickContraction.Uncontracted
import PhysLean.PerturbationTheory.WickContraction.UncontractedList
import PhysLean.SpaceTime.Basic
import PhysLean.SpaceTime.CliffordAlgebra
import PhysLean.StandardModel.Basic
import PhysLean.StandardModel.HiggsBoson.Basic
import PhysLean.StandardModel.HiggsBoson.GaugeAction
import PhysLean.StandardModel.HiggsBoson.PointwiseInnerProd
import PhysLean.StandardModel.HiggsBoson.Potential
import PhysLean.StandardModel.Representations
import PhysLean.Tensors.OverColor.Basic
import PhysLean.Tensors.OverColor.Discrete
import PhysLean.Tensors.OverColor.Functors
import PhysLean.Tensors.OverColor.Iso
import PhysLean.Tensors.OverColor.Lift
import PhysLean.Tensors.TensorSpecies.Basic
import PhysLean.Tensors.TensorSpecies.Contractions.Basic
import PhysLean.Tensors.TensorSpecies.Contractions.Categorical
import PhysLean.Tensors.TensorSpecies.Contractions.ContrMap
import PhysLean.Tensors.TensorSpecies.DualRepIso
import PhysLean.Tensors.TensorSpecies.MetricTensor
import PhysLean.Tensors.TensorSpecies.Pure
import PhysLean.Tensors.TensorSpecies.UnitTensor
import PhysLean.Tensors.Tree.Basic
import PhysLean.Tensors.Tree.Dot
import PhysLean.Tensors.Tree.Elab
import PhysLean.Tensors.Tree.NodeIdentities.Assoc
import PhysLean.Tensors.Tree.NodeIdentities.Basic
import PhysLean.Tensors.Tree.NodeIdentities.Congr
import PhysLean.Tensors.Tree.NodeIdentities.ContrContr
import PhysLean.Tensors.Tree.NodeIdentities.ContrSwap
import PhysLean.Tensors.Tree.NodeIdentities.PermContr
import PhysLean.Tensors.Tree.NodeIdentities.PermProd
import PhysLean.Tensors.Tree.NodeIdentities.ProdAssoc
import PhysLean.Tensors.Tree.NodeIdentities.ProdComm
import PhysLean.Tensors.Tree.NodeIdentities.ProdContr

4
HepLean/AnomalyCancellation/Basic.lean → PhysLean/AnomalyCancellation/Basic.lean
View file

@ -3,8 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Mathematics.LinearMaps
import HepLean.Meta.TODO.Basic
import PhysLean.Mathematics.LinearMaps
import PhysLean.Meta.TODO.Basic
import Mathlib.LinearAlgebra.FiniteDimensional.Defs
/-!
# Basic set up for anomaly cancellation conditions

2
HepLean/AnomalyCancellation/GroupActions.lean → PhysLean/AnomalyCancellation/GroupActions.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.Basic
import PhysLean.AnomalyCancellation.Basic
import Mathlib.RepresentationTheory.Basic
/-!
# Group actions on ACC systems.

2
HepLean/AnomalyCancellation/MSSMNu/B3.lean → PhysLean/AnomalyCancellation/MSSMNu/B3.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.MSSMNu.Basic
import PhysLean.AnomalyCancellation.MSSMNu.Basic
/-!
# The definition of the solution B₃ and properties thereof

2
HepLean/AnomalyCancellation/MSSMNu/Basic.lean → PhysLean/AnomalyCancellation/MSSMNu/Basic.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.Basic
import PhysLean.AnomalyCancellation.Basic
/-!
# The MSSM with 3 families and RHNs

2
HepLean/AnomalyCancellation/MSSMNu/HyperCharge.lean → PhysLean/AnomalyCancellation/MSSMNu/HyperCharge.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.MSSMNu.Basic
import PhysLean.AnomalyCancellation.MSSMNu.Basic
/-!
# Hypercharge in MSSM.

4
HepLean/AnomalyCancellation/MSSMNu/LineY3B3.lean → PhysLean/AnomalyCancellation/MSSMNu/LineY3B3.lean
View file

@ -3,8 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.MSSMNu.Y3
import HepLean.AnomalyCancellation.MSSMNu.B3
import PhysLean.AnomalyCancellation.MSSMNu.Y3
import PhysLean.AnomalyCancellation.MSSMNu.B3
/-!
# The line through B₃ and Y₃

2
HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/Basic.lean → PhysLean/AnomalyCancellation/MSSMNu/OrthogY3B3/Basic.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.MSSMNu.LineY3B3
import PhysLean.AnomalyCancellation.MSSMNu.LineY3B3
/-!
# The type of solutions perpendicular to `Y₃` and `B₃`

2
HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean → PhysLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.MSSMNu.OrthogY3B3.Basic
import PhysLean.AnomalyCancellation.MSSMNu.OrthogY3B3.Basic
/-!
# Plane Y₃ B₃ and an orthogonal third point

2
HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean → PhysLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.MSSMNu.OrthogY3B3.PlaneWithY3B3
import PhysLean.AnomalyCancellation.MSSMNu.OrthogY3B3.PlaneWithY3B3
/-!
# From charges perpendicular to `Y₃` and `B₃` to solutions

2
HepLean/AnomalyCancellation/MSSMNu/Permutations.lean → PhysLean/AnomalyCancellation/MSSMNu/Permutations.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.MSSMNu.Basic
import PhysLean.AnomalyCancellation.MSSMNu.Basic
import Mathlib.RepresentationTheory.Basic
/-!
# Permutations of MSSM charges and solutions

2
HepLean/AnomalyCancellation/MSSMNu/Y3.lean → PhysLean/AnomalyCancellation/MSSMNu/Y3.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.MSSMNu.Basic
import PhysLean.AnomalyCancellation.MSSMNu.Basic
/-!
# The definition of the solution Y₃ and properties thereof

2
HepLean/AnomalyCancellation/PureU1/Basic.lean → PhysLean/AnomalyCancellation/PureU1/Basic.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.Basic
import PhysLean.AnomalyCancellation.Basic
/-!
# Pure U(1) ACC system.

2
HepLean/AnomalyCancellation/PureU1/BasisLinear.lean → PhysLean/AnomalyCancellation/PureU1/BasisLinear.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.PureU1.Basic
import PhysLean.AnomalyCancellation.PureU1.Basic
import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
/-!
# Basis of `LinSols`

2
HepLean/AnomalyCancellation/PureU1/ConstAbs.lean → PhysLean/AnomalyCancellation/PureU1/ConstAbs.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.PureU1.VectorLike
import PhysLean.AnomalyCancellation.PureU1.VectorLike
/-!
# Charges assignments with constant abs

4
HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean → PhysLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean
View file

@ -3,8 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.PureU1.BasisLinear
import HepLean.AnomalyCancellation.PureU1.VectorLike
import PhysLean.AnomalyCancellation.PureU1.BasisLinear
import PhysLean.AnomalyCancellation.PureU1.VectorLike
/-!
# Basis of `LinSols` in the even case

4
HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean → PhysLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean
View file

@ -3,8 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.PureU1.Even.BasisLinear
import HepLean.AnomalyCancellation.PureU1.LineInPlaneCond
import PhysLean.AnomalyCancellation.PureU1.Even.BasisLinear
import PhysLean.AnomalyCancellation.PureU1.LineInPlaneCond
/-!
# Line In Cubic Even case

2
HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean → PhysLean/AnomalyCancellation/PureU1/Even/Parameterization.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.PureU1.Even.LineInCubic
import PhysLean.AnomalyCancellation.PureU1.Even.LineInCubic
/-!
# Parameterization in even case

2
HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean → PhysLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.PureU1.ConstAbs
import PhysLean.AnomalyCancellation.PureU1.ConstAbs
import Mathlib.Tactic.FieldSimp
/-!
# Line in plane condition

2
HepLean/AnomalyCancellation/PureU1/LowDim/One.lean → PhysLean/AnomalyCancellation/PureU1/LowDim/One.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.PureU1.Basic
import PhysLean.AnomalyCancellation.PureU1.Basic
/-!
# The Pure U(1) case with 1 fermion

2
HepLean/AnomalyCancellation/PureU1/LowDim/Three.lean → PhysLean/AnomalyCancellation/PureU1/LowDim/Three.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.PureU1.Basic
import PhysLean.AnomalyCancellation.PureU1.Basic
/-!
# The Pure U(1) case with 3 fermion

2
HepLean/AnomalyCancellation/PureU1/LowDim/Two.lean → PhysLean/AnomalyCancellation/PureU1/LowDim/Two.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.PureU1.Basic
import PhysLean.AnomalyCancellation.PureU1.Basic
/-!
# The Pure U(1) case with 2 fermions

4
HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean → PhysLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean
View file

@ -3,8 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.PureU1.BasisLinear
import HepLean.AnomalyCancellation.PureU1.VectorLike
import PhysLean.AnomalyCancellation.PureU1.BasisLinear
import PhysLean.AnomalyCancellation.PureU1.VectorLike
/-!
# Basis of `LinSols` in the odd case

4
HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean → PhysLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
View file

@ -3,8 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.PureU1.LineInPlaneCond
import HepLean.AnomalyCancellation.PureU1.Odd.BasisLinear
import PhysLean.AnomalyCancellation.PureU1.LineInPlaneCond
import PhysLean.AnomalyCancellation.PureU1.Odd.BasisLinear
/-!
# Line In Cubic Odd case

2
HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean → PhysLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.PureU1.Odd.LineInCubic
import PhysLean.AnomalyCancellation.PureU1.Odd.LineInCubic
/-!
# Parameterization in odd case

4
HepLean/AnomalyCancellation/PureU1/Permutations.lean → PhysLean/AnomalyCancellation/PureU1/Permutations.lean
View file

@ -3,8 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.PureU1.Basic
import HepLean.AnomalyCancellation.GroupActions
import PhysLean.AnomalyCancellation.PureU1.Basic
import PhysLean.AnomalyCancellation.GroupActions
import Mathlib.Logic.Equiv.Fintype
/-!
# Permutations of Pure U(1) ACC

2
HepLean/AnomalyCancellation/PureU1/Sorts.lean → PhysLean/AnomalyCancellation/PureU1/Sorts.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.PureU1.Permutations
import PhysLean.AnomalyCancellation.PureU1.Permutations
import Mathlib.Data.Fin.Tuple.Sort
/-!
# Sort for Pure U(1) charges

2
HepLean/AnomalyCancellation/PureU1/VectorLike.lean → PhysLean/AnomalyCancellation/PureU1/VectorLike.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.PureU1.Sorts
import PhysLean.AnomalyCancellation.PureU1.Sorts
/-!
# Vector like charges

2
HepLean/AnomalyCancellation/SM/Basic.lean → PhysLean/AnomalyCancellation/SM/Basic.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.Basic
import PhysLean.AnomalyCancellation.Basic
/-!
# Anomaly cancellation conditions for n family SM.

2
HepLean/AnomalyCancellation/SM/FamilyMaps.lean → PhysLean/AnomalyCancellation/SM/FamilyMaps.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.SM.Basic
import PhysLean.AnomalyCancellation.SM.Basic
/-!
# Family maps for the Standard Model ACCs

2
HepLean/AnomalyCancellation/SM/NoGrav/Basic.lean → PhysLean/AnomalyCancellation/SM/NoGrav/Basic.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.SM.Basic
import PhysLean.AnomalyCancellation.SM.Basic
/-!
# Anomaly Cancellation in the Standard Model without Gravity

2
HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean → PhysLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.SM.NoGrav.One.LinearParameterization
import PhysLean.AnomalyCancellation.SM.NoGrav.One.LinearParameterization
/-!
# Lemmas for 1 family SM Accs

2
HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean → PhysLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.SM.NoGrav.Basic
import PhysLean.AnomalyCancellation.SM.NoGrav.Basic
import Mathlib.NumberTheory.FLT.Three
/-!
# Parameterizations for solutions to the linear ACCs for 1 family

2
HepLean/AnomalyCancellation/SM/Permutations.lean → PhysLean/AnomalyCancellation/SM/Permutations.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.SM.Basic
import PhysLean.AnomalyCancellation.SM.Basic
import Mathlib.RepresentationTheory.Basic
/-!

2
HepLean/AnomalyCancellation/SMNu/Basic.lean → PhysLean/AnomalyCancellation/SMNu/Basic.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.Basic
import PhysLean.AnomalyCancellation.Basic
/-!
# Anomaly cancellation conditions for n family SM.
-/

2
HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean → PhysLean/AnomalyCancellation/SMNu/FamilyMaps.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.SMNu.Basic
import PhysLean.AnomalyCancellation.SMNu.Basic
/-!
# Family maps for the Standard Model for RHN ACCs

4
HepLean/AnomalyCancellation/SMNu/NoGrav/Basic.lean → PhysLean/AnomalyCancellation/SMNu/NoGrav/Basic.lean
View file

@ -3,8 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.SMNu.Permutations
import HepLean.AnomalyCancellation.GroupActions
import PhysLean.AnomalyCancellation.SMNu.Permutations
import PhysLean.AnomalyCancellation.GroupActions
/-!
# ACC system for SM with RHN and no gravitational anomaly.

4
HepLean/AnomalyCancellation/SMNu/Ordinary/Basic.lean → PhysLean/AnomalyCancellation/SMNu/Ordinary/Basic.lean
View file

@ -3,8 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.SMNu.Permutations
import HepLean.AnomalyCancellation.GroupActions
import PhysLean.AnomalyCancellation.SMNu.Permutations
import PhysLean.AnomalyCancellation.GroupActions
/-!
# ACC system for SM with RHN (without hypercharge).

2
HepLean/AnomalyCancellation/SMNu/Ordinary/DimSevenPlane.lean → PhysLean/AnomalyCancellation/SMNu/Ordinary/DimSevenPlane.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.SMNu.Ordinary.Basic
import PhysLean.AnomalyCancellation.SMNu.Ordinary.Basic
/-!
# Dimension 7 plane

4
HepLean/AnomalyCancellation/SMNu/Ordinary/FamilyMaps.lean → PhysLean/AnomalyCancellation/SMNu/Ordinary/FamilyMaps.lean
View file

@ -3,8 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.SMNu.Ordinary.Basic
import HepLean.AnomalyCancellation.SMNu.FamilyMaps
import PhysLean.AnomalyCancellation.SMNu.Ordinary.Basic
import PhysLean.AnomalyCancellation.SMNu.FamilyMaps
/-!
# Family Maps for SM with RHN (no hypercharge)

2
HepLean/AnomalyCancellation/SMNu/Permutations.lean → PhysLean/AnomalyCancellation/SMNu/Permutations.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.SMNu.Basic
import PhysLean.AnomalyCancellation.SMNu.Basic
import Mathlib.RepresentationTheory.Basic
/-!
# Permutations of SM charges with RHN.

2
HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean → PhysLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.SMNu.PlusU1.FamilyMaps
import PhysLean.AnomalyCancellation.SMNu.PlusU1.FamilyMaps
/-!
# B Minus L in SM with RHN.

4
HepLean/AnomalyCancellation/SMNu/PlusU1/Basic.lean → PhysLean/AnomalyCancellation/SMNu/PlusU1/Basic.lean
View file

@ -3,8 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.SMNu.Permutations
import HepLean.AnomalyCancellation.GroupActions
import PhysLean.AnomalyCancellation.SMNu.Permutations
import PhysLean.AnomalyCancellation.GroupActions
/-!
# ACC system for SM with RHN

2
HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean → PhysLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.SMNu.PlusU1.PlaneNonSols
import PhysLean.AnomalyCancellation.SMNu.PlusU1.PlaneNonSols
/-!
# Bound on plane dimension

4
HepLean/AnomalyCancellation/SMNu/PlusU1/FamilyMaps.lean → PhysLean/AnomalyCancellation/SMNu/PlusU1/FamilyMaps.lean
View file

@ -3,8 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.SMNu.PlusU1.Basic
import HepLean.AnomalyCancellation.SMNu.FamilyMaps
import PhysLean.AnomalyCancellation.SMNu.PlusU1.Basic
import PhysLean.AnomalyCancellation.SMNu.FamilyMaps
/-!
# Family Maps for SM with RHN

2
HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean → PhysLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.SMNu.PlusU1.FamilyMaps
import PhysLean.AnomalyCancellation.SMNu.PlusU1.FamilyMaps
/-!
# Hypercharge in SM with RHN.

2
HepLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean → PhysLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.SMNu.PlusU1.Basic
import PhysLean.AnomalyCancellation.SMNu.PlusU1.Basic
/-!
# Plane of non-solutions

2
HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSol.lean → PhysLean/AnomalyCancellation/SMNu/PlusU1/QuadSol.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.SMNu.PlusU1.Basic
import PhysLean.AnomalyCancellation.SMNu.PlusU1.Basic
import Mathlib.Tactic.FieldSimp
/-!
# Properties of Quad Sols for SM with RHN

2
HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSolToSol.lean → PhysLean/AnomalyCancellation/SMNu/PlusU1/QuadSolToSol.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.SMNu.PlusU1.BMinusL
import PhysLean.AnomalyCancellation.SMNu.PlusU1.BMinusL
import Mathlib.Tactic.FieldSimp
/-!
# Solutions from quad solutions

2
HepLean/BeyondTheStandardModel/GeorgiGlashow/Basic.lean → PhysLean/BeyondTheStandardModel/GeorgiGlashow/Basic.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.StandardModel.Basic
import PhysLean.StandardModel.Basic
/-!
# The Georgi-Glashow Model

2
HepLean/BeyondTheStandardModel/PatiSalam/Basic.lean → PhysLean/BeyondTheStandardModel/PatiSalam/Basic.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.StandardModel.Basic
import PhysLean.StandardModel.Basic
/-!
# The Pati-Salam Model

4
HepLean/BeyondTheStandardModel/Spin10/Basic.lean → PhysLean/BeyondTheStandardModel/Spin10/Basic.lean
View file

@ -3,8 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.BeyondTheStandardModel.PatiSalam.Basic
import HepLean.BeyondTheStandardModel.GeorgiGlashow.Basic
import PhysLean.BeyondTheStandardModel.PatiSalam.Basic
import PhysLean.BeyondTheStandardModel.GeorgiGlashow.Basic
/-!
# The Spin(10) Model

4
HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean → PhysLean/BeyondTheStandardModel/TwoHDM/Basic.lean
View file

@ -3,8 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.StandardModel.HiggsBoson.Potential
import HepLean.Meta.TODO.Basic
import PhysLean.StandardModel.HiggsBoson.Potential
import PhysLean.Meta.TODO.Basic
/-!
# The Two Higgs Doublet Model

4
HepLean/BeyondTheStandardModel/TwoHDM/GaugeOrbits.lean → PhysLean/BeyondTheStandardModel/TwoHDM/GaugeOrbits.lean
View file

@ -3,8 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.BeyondTheStandardModel.TwoHDM.Basic
import HepLean.StandardModel.HiggsBoson.GaugeAction
import PhysLean.BeyondTheStandardModel.TwoHDM.Basic
import PhysLean.StandardModel.HiggsBoson.GaugeAction
import Mathlib.LinearAlgebra.Matrix.PosDef
import Mathlib.Analysis.CStarAlgebra.Matrix
/-!

0
HepLean/FlavorPhysics/CKMMatrix/Basic.lean → PhysLean/FlavorPhysics/CKMMatrix/Basic.lean
View file

2
HepLean/FlavorPhysics/CKMMatrix/Invariants.lean → PhysLean/FlavorPhysics/CKMMatrix/Invariants.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.FlavorPhysics.CKMMatrix.Basic
import PhysLean.FlavorPhysics.CKMMatrix.Basic
import Mathlib.Analysis.Complex.Basic
/-!
# Invariants of the CKM Matrix

2
HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean → PhysLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.FlavorPhysics.CKMMatrix.Relations
import PhysLean.FlavorPhysics.CKMMatrix.Relations
/-!
# Phase freedom of the CKM Matrix

2
HepLean/FlavorPhysics/CKMMatrix/Relations.lean → PhysLean/FlavorPhysics/CKMMatrix/Relations.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.FlavorPhysics.CKMMatrix.Rows
import PhysLean.FlavorPhysics.CKMMatrix.Rows
/-!
# Relations for the CKM Matrix

2
HepLean/FlavorPhysics/CKMMatrix/Rows.lean → PhysLean/FlavorPhysics/CKMMatrix/Rows.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.FlavorPhysics.CKMMatrix.Basic
import PhysLean.FlavorPhysics.CKMMatrix.Basic
import Mathlib.Analysis.SpecialFunctions.Complex.Arg
import Mathlib.LinearAlgebra.CrossProduct
import Mathlib.LinearAlgebra.FiniteDimensional

4
HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean → PhysLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean
View file

@ -3,8 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.FlavorPhysics.CKMMatrix.Rows
import HepLean.FlavorPhysics.CKMMatrix.Invariants
import PhysLean.FlavorPhysics.CKMMatrix.Rows
import PhysLean.FlavorPhysics.CKMMatrix.Invariants
/-!
# Standard parameterization for the CKM Matrix

4
HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean → PhysLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean
View file

@ -3,8 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.FlavorPhysics.CKMMatrix.PhaseFreedom
import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.Basic
import PhysLean.FlavorPhysics.CKMMatrix.PhaseFreedom
import PhysLean.FlavorPhysics.CKMMatrix.StandardParameterization.Basic
/-!
# Standard parameters for the CKM Matrix

2
HepLean/Lorentz/Algebra/Basic.lean → PhysLean/Lorentz/Algebra/Basic.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Lorentz.RealVector.Basic
import PhysLean.Lorentz.RealVector.Basic
/-!
# The Lorentz Algebra

4
HepLean/Lorentz/Algebra/Basis.lean → PhysLean/Lorentz/Algebra/Basis.lean
View file

@ -3,8 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Lorentz.Algebra.Basic
import HepLean.Meta.TODO.Basic
import PhysLean.Lorentz.Algebra.Basic
import PhysLean.Meta.TODO.Basic
/-!
# Basis of the Lorentz Algebra

8
HepLean/Lorentz/ComplexTensor/Basic.lean → PhysLean/Lorentz/ComplexTensor/Basic.lean
View file

@ -3,10 +3,10 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Tensors.Tree.Dot
import HepLean.Lorentz.Weyl.Metric
import HepLean.Lorentz.ComplexVector.Metric
import HepLean.Lorentz.PauliMatrices.AsTensor
import PhysLean.Tensors.Tree.Dot
import PhysLean.Lorentz.Weyl.Metric
import PhysLean.Lorentz.ComplexVector.Metric
import PhysLean.Lorentz.PauliMatrices.AsTensor
/-!
## Complex Lorentz tensors

16
HepLean/Lorentz/ComplexTensor/Basis.lean → PhysLean/Lorentz/ComplexTensor/Basis.lean
View file

@ -3,12 +3,12 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Tensors.Tree.NodeIdentities.PermProd
import HepLean.Tensors.Tree.NodeIdentities.PermContr
import HepLean.Tensors.Tree.NodeIdentities.ProdComm
import HepLean.Tensors.Tree.NodeIdentities.ContrSwap
import HepLean.Tensors.Tree.NodeIdentities.ContrContr
import HepLean.Meta.TODO.Basic
import PhysLean.Tensors.Tree.NodeIdentities.PermProd
import PhysLean.Tensors.Tree.NodeIdentities.PermContr
import PhysLean.Tensors.Tree.NodeIdentities.ProdComm
import PhysLean.Tensors.Tree.NodeIdentities.ContrSwap
import PhysLean.Tensors.Tree.NodeIdentities.ContrContr
import PhysLean.Meta.TODO.Basic
/-!
## Basis vectors associated with complex Lorentz tensors
@ -175,7 +175,7 @@ lemma prod_basisVector {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
(prod (tensorNode (basisVector c b)) (tensorNode (basisVector c1 b1))).tensor =
basisVector (Sum.elim c c1 ∘ finSumFinEquiv.symm) (fun i =>
prodBasisVecEquiv (finSumFinEquiv.symm i)
((HepLean.PiTensorProduct.elimPureTensor b b1) (finSumFinEquiv.symm i))) := by
((PhysLean.PiTensorProduct.elimPureTensor b b1) (finSumFinEquiv.symm i))) := by
rw [prod_tensor, basisVector, basisVector]
simp only [TensorSpecies.F_def, Functor.id_obj, OverColor.mk_hom,
Action.instMonoidalCategory_tensorObj_V, Equivalence.symm_inverse,
@ -205,7 +205,7 @@ lemma prod_basisVector_tree {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
(prod (tensorNode (basisVector c b)) (tensorNode (basisVector c1 b1))).tensor =
(tensorNode (basisVector (Sum.elim c c1 ∘ finSumFinEquiv.symm) (fun i =>
prodBasisVecEquiv (finSumFinEquiv.symm i)
((HepLean.PiTensorProduct.elimPureTensor b b1) (finSumFinEquiv.symm i))))).tensor := by
((PhysLean.PiTensorProduct.elimPureTensor b b1) (finSumFinEquiv.symm i))))).tensor := by
exact prod_basisVector _ _
/-- The `eval` node acting on basis vectors corresponds to a basis vector. -/

2
HepLean/Lorentz/ComplexTensor/Bispinors/Basic.lean → PhysLean/Lorentz/ComplexTensor/Bispinors/Basic.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Lorentz.ComplexTensor.PauliMatrices.Basic
import PhysLean.Lorentz.ComplexTensor.PauliMatrices.Basic
/-!
## Bispinors

2
HepLean/Lorentz/ComplexTensor/Lemmas.lean → PhysLean/Lorentz/ComplexTensor/Lemmas.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Lorentz.ComplexTensor.Basis
import PhysLean.Lorentz.ComplexTensor.Basis
/-!
## Lemmas related to complex Lorentz tensors.

12
HepLean/Lorentz/ComplexTensor/Metrics/Basic.lean → PhysLean/Lorentz/ComplexTensor/Metrics/Basic.lean
View file

@ -3,12 +3,12 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Tensors.Tree.NodeIdentities.ProdAssoc
import HepLean.Tensors.Tree.NodeIdentities.ProdComm
import HepLean.Tensors.Tree.NodeIdentities.ProdContr
import HepLean.Tensors.Tree.NodeIdentities.ContrContr
import HepLean.Tensors.Tree.NodeIdentities.ContrSwap
import HepLean.Tensors.Tree.NodeIdentities.PermContr
import PhysLean.Tensors.Tree.NodeIdentities.ProdAssoc
import PhysLean.Tensors.Tree.NodeIdentities.ProdComm
import PhysLean.Tensors.Tree.NodeIdentities.ProdContr
import PhysLean.Tensors.Tree.NodeIdentities.ContrContr
import PhysLean.Tensors.Tree.NodeIdentities.ContrSwap
import PhysLean.Tensors.Tree.NodeIdentities.PermContr
/-!
## Metrics as complex Lorentz tensors

4
HepLean/Lorentz/ComplexTensor/Metrics/Basis.lean → PhysLean/Lorentz/ComplexTensor/Metrics/Basis.lean
View file

@ -3,8 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Lorentz.ComplexTensor.Metrics.Basic
import HepLean.Lorentz.ComplexTensor.Basis
import PhysLean.Lorentz.ComplexTensor.Metrics.Basic
import PhysLean.Lorentz.ComplexTensor.Basis
/-!
## Metrics and basis expansions

4
HepLean/Lorentz/ComplexTensor/Metrics/Lemmas.lean → PhysLean/Lorentz/ComplexTensor/Metrics/Lemmas.lean
View file

@ -3,8 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Lorentz.ComplexTensor.Metrics.Basis
import HepLean.Lorentz.ComplexTensor.Units.Basic
import PhysLean.Lorentz.ComplexTensor.Metrics.Basis
import PhysLean.Lorentz.ComplexTensor.Units.Basic
/-!
## Basic lemmas regarding metrics

2
HepLean/Lorentz/ComplexTensor/PauliMatrices/Basic.lean → PhysLean/Lorentz/ComplexTensor/PauliMatrices/Basic.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Lorentz.ComplexTensor.Metrics.Lemmas
import PhysLean.Lorentz.ComplexTensor.Metrics.Lemmas
/-!
## Pauli matrices as complex Lorentz tensors

6
HepLean/Lorentz/ComplexTensor/PauliMatrices/Basis.lean → PhysLean/Lorentz/ComplexTensor/PauliMatrices/Basis.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Lorentz.ComplexTensor.PauliMatrices.Basic
import PhysLean.Lorentz.ComplexTensor.PauliMatrices.Basic
/-!
## Pauli matrices and the basis of complex Lorentz tensors
@ -181,7 +181,7 @@ lemma basis_contr_pauliMatrix_basis_tree_expand' {n : ℕ} {c : Fin n → comple
(b : Π k, Fin (complexLorentzTensor.repDim (c k))) :
let c' := Sum.elim c ![Color.up, Color.upL, Color.upR] ∘ finSumFinEquiv.symm
let b' (i1 i2 i3 : Fin 4) := fun i => prodBasisVecEquiv (finSumFinEquiv.symm i)
((HepLean.PiTensorProduct.elimPureTensor b (fun | 0 => i1 | 1 => i2 | 2 => i3))
((PhysLean.PiTensorProduct.elimPureTensor b (fun | 0 => i1 | 1 => i2 | 2 => i3))
(finSumFinEquiv.symm i))
(contr i j h (TensorTree.prod (tensorNode (basisVector c b))
(tensorNode pauliContr))).tensor = ((contr i j h ((tensorNode
@ -223,7 +223,7 @@ def pauliMatrixBasisProdMap
(i : Fin (n + (Nat.succ 0).succ.succ)) →
Fin (complexLorentzTensor.repDim (Sum.elim c ![Color.up, Color.upL, Color.upR]
(finSumFinEquiv.symm i))) := fun i => prodBasisVecEquiv (finSumFinEquiv.symm i)
((HepLean.PiTensorProduct.elimPureTensor b (fun | (0 : Fin 3) => i1 | 1 => i2 | 2 => i3))
((PhysLean.PiTensorProduct.elimPureTensor b (fun | (0 : Fin 3) => i1 | 1 => i2 | 2 => i3))
(finSumFinEquiv.symm i))
/-- The new basis vectors which appear when contracting pauli matrices with

2
HepLean/Lorentz/ComplexTensor/PauliMatrices/CoContractContr.lean → PhysLean/Lorentz/ComplexTensor/PauliMatrices/CoContractContr.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Lorentz.ComplexTensor.PauliMatrices.Basis
import PhysLean.Lorentz.ComplexTensor.PauliMatrices.Basis
/-!
## Contractiong of indices of Pauli matrix.

12
HepLean/Lorentz/ComplexTensor/Units/Basic.lean → PhysLean/Lorentz/ComplexTensor/Units/Basic.lean
View file

@ -3,12 +3,12 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Tensors.Tree.NodeIdentities.ProdAssoc
import HepLean.Tensors.Tree.NodeIdentities.ProdComm
import HepLean.Tensors.Tree.NodeIdentities.ProdContr
import HepLean.Tensors.Tree.NodeIdentities.ContrContr
import HepLean.Tensors.Tree.NodeIdentities.ContrSwap
import HepLean.Tensors.Tree.NodeIdentities.PermContr
import PhysLean.Tensors.Tree.NodeIdentities.ProdAssoc
import PhysLean.Tensors.Tree.NodeIdentities.ProdComm
import PhysLean.Tensors.Tree.NodeIdentities.ProdContr
import PhysLean.Tensors.Tree.NodeIdentities.ContrContr
import PhysLean.Tensors.Tree.NodeIdentities.ContrSwap
import PhysLean.Tensors.Tree.NodeIdentities.PermContr
/-!
## Metrics as complex Lorentz tensors

4
HepLean/Lorentz/ComplexTensor/Units/Symm.lean → PhysLean/Lorentz/ComplexTensor/Units/Symm.lean
View file

@ -3,8 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Lorentz.ComplexTensor.Metrics.Basis
import HepLean.Lorentz.ComplexTensor.Units.Basic
import PhysLean.Lorentz.ComplexTensor.Metrics.Basis
import PhysLean.Lorentz.ComplexTensor.Units.Basic
/-!
## Symmetry lemmas relating to units

4
HepLean/Lorentz/ComplexVector/Basic.lean → PhysLean/Lorentz/ComplexVector/Basic.lean
View file

@ -3,8 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Lorentz.ComplexVector.Modules
import HepLean.Meta.TODO.Basic
import PhysLean.Lorentz.ComplexVector.Modules
import PhysLean.Meta.TODO.Basic
/-!
# Complex Lorentz vectors

2
HepLean/Lorentz/ComplexVector/Contraction.lean → PhysLean/Lorentz/ComplexVector/Contraction.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Lorentz.ComplexVector.Basic
import PhysLean.Lorentz.ComplexVector.Basic
/-!
# Contraction of Lorentz vectors

2
HepLean/Lorentz/ComplexVector/Metric.lean → PhysLean/Lorentz/ComplexVector/Metric.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Lorentz.ComplexVector.Unit
import PhysLean.Lorentz.ComplexVector.Unit
/-!
# Metric for complex Lorentz vectors

2
HepLean/Lorentz/ComplexVector/Modules.lean → PhysLean/Lorentz/ComplexVector/Modules.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Lorentz.SL2C.Basic
import PhysLean.Lorentz.SL2C.Basic
/-!
## Modules associated with complex Lorentz vectors

2
HepLean/Lorentz/ComplexVector/Two.lean → PhysLean/Lorentz/ComplexVector/Two.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Lorentz.ComplexVector.Basic
import PhysLean.Lorentz.ComplexVector.Basic
import Mathlib.LinearAlgebra.TensorProduct.Matrix
/-!

4
HepLean/Lorentz/ComplexVector/Unit.lean → PhysLean/Lorentz/ComplexVector/Unit.lean
View file

@ -3,8 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Lorentz.ComplexVector.Two
import HepLean.Lorentz.ComplexVector.Contraction
import PhysLean.Lorentz.ComplexVector.Two
import PhysLean.Lorentz.ComplexVector.Contraction
/-!
# Unit for complex Lorentz vectors

4
HepLean/Lorentz/Group/Basic.lean → PhysLean/Lorentz/Group/Basic.lean
View file

@ -3,8 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Lorentz.MinkowskiMatrix
import HepLean.Meta.TODO.Basic
import PhysLean.Lorentz.MinkowskiMatrix
import PhysLean.Meta.TODO.Basic
/-!
# The Lorentz Group

4
HepLean/Lorentz/Group/Boosts.lean → PhysLean/Lorentz/Group/Boosts.lean
View file

@ -3,8 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Lorentz.Group.Proper
import HepLean.Lorentz.RealVector.NormOne
import PhysLean.Lorentz.Group.Proper
import PhysLean.Lorentz.RealVector.NormOne
/-!
# Boosts

4
HepLean/Lorentz/Group/Orthochronous.lean → PhysLean/Lorentz/Group/Orthochronous.lean
View file

@ -3,8 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Lorentz.RealVector.NormOne
import HepLean.Lorentz.Group.Proper
import PhysLean.Lorentz.RealVector.NormOne
import PhysLean.Lorentz.Group.Proper
/-!
# The Orthochronous Lorentz Group

2
HepLean/Lorentz/Group/Proper.lean → PhysLean/Lorentz/Group/Proper.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Lorentz.Group.Basic
import PhysLean.Lorentz.Group.Basic
/-!
# The Proper Lorentz Group

4
HepLean/Lorentz/Group/Restricted.lean → PhysLean/Lorentz/Group/Restricted.lean
View file

@ -3,8 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Lorentz.Group.Orthochronous
import HepLean.Meta.Informal.Basic
import PhysLean.Lorentz.Group.Orthochronous
import PhysLean.Meta.Informal.Basic
/-!
# The Restricted Lorentz Group

4
HepLean/Lorentz/Group/Rotations.lean → PhysLean/Lorentz/Group/Rotations.lean
View file

@ -3,8 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Lorentz.Group.Basic
import HepLean.Mathematics.SO3.Basic
import PhysLean.Lorentz.Group.Basic
import PhysLean.Mathematics.SO3.Basic
/-!
# Rotations

0
HepLean/Lorentz/MinkowskiMatrix.lean → PhysLean/Lorentz/MinkowskiMatrix.lean
View file

4
HepLean/Lorentz/PauliMatrices/AsTensor.lean → PhysLean/Lorentz/PauliMatrices/AsTensor.lean
View file

@ -3,8 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Tensors.OverColor.Basic
import HepLean.Lorentz.Weyl.Two
import PhysLean.Tensors.OverColor.Basic
import PhysLean.Lorentz.Weyl.Two
/-!
## Pauli matrices

4
HepLean/Lorentz/PauliMatrices/Basic.lean → PhysLean/Lorentz/PauliMatrices/Basic.lean
View file

@ -3,9 +3,9 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Mathematics.PiTensorProduct
import PhysLean.Mathematics.PiTensorProduct
import Mathlib.RepresentationTheory.Rep
import HepLean.Lorentz.Group.Basic
import PhysLean.Lorentz.Group.Basic
/-!
## Pauli matrices

2
HepLean/Lorentz/PauliMatrices/SelfAdjoint.lean → PhysLean/Lorentz/PauliMatrices/SelfAdjoint.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Lorentz.PauliMatrices.Basic
import PhysLean.Lorentz.PauliMatrices.Basic
/-!
## Interaction of Pauli matrices with self-adjoint matrices

2
HepLean/Lorentz/RealVector/Basic.lean → PhysLean/Lorentz/RealVector/Basic.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Lorentz.RealVector.Modules
import PhysLean.Lorentz.RealVector.Modules
/-!
# Real Lorentz vectors

2
HepLean/Lorentz/RealVector/Contraction.lean → PhysLean/Lorentz/RealVector/Contraction.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Lorentz.RealVector.Basic
import PhysLean.Lorentz.RealVector.Basic
/-!
# Contraction of Real Lorentz vectors

2
HepLean/Lorentz/RealVector/Modules.lean → PhysLean/Lorentz/RealVector/Modules.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Lorentz.PauliMatrices.SelfAdjoint
import PhysLean.Lorentz.PauliMatrices.SelfAdjoint
/-!
## Modules associated with Real Lorentz vectors

2
HepLean/Lorentz/RealVector/NormOne.lean → PhysLean/Lorentz/RealVector/NormOne.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Lorentz.RealVector.Contraction
import PhysLean.Lorentz.RealVector.Contraction
import Mathlib.GroupTheory.GroupAction.Blocks
/-!

4
HepLean/Lorentz/SL2C/Basic.lean → PhysLean/Lorentz/SL2C/Basic.lean
View file

@ -3,8 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Lorentz.Group.Restricted
import HepLean.Lorentz.SL2C.SelfAdjoint
import PhysLean.Lorentz.Group.Restricted
import PhysLean.Lorentz.SL2C.SelfAdjoint
import Mathlib.Analysis.Complex.Polynomial.Basic -- Complex.isAlgClosed
/-!
# The group SL(2, ℂ) and it's relation to the Lorentz group

2
HepLean/Lorentz/SL2C/SelfAdjoint.lean → PhysLean/Lorentz/SL2C/SelfAdjoint.lean
View file

@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Gordon Hsu
-/
import Mathlib.LinearAlgebra.Matrix.SchurComplement
import HepLean.Mathematics.SchurTriangulation
import PhysLean.Mathematics.SchurTriangulation
/-! # Extra lemmas regarding `Lorentz.SL2C.toSelfAdjointMap`

2
HepLean/Lorentz/Weyl/Basic.lean → PhysLean/Lorentz/Weyl/Basic.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Lorentz.Weyl.Modules
import PhysLean.Lorentz.Weyl.Modules
/-!
# Weyl fermions

2
HepLean/Lorentz/Weyl/Contraction.lean → PhysLean/Lorentz/Weyl/Contraction.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Lorentz.Weyl.Basic
import PhysLean.Lorentz.Weyl.Basic
/-!
# Contraction of Weyl fermions

Some files were not shown because too many files have changed in this diff Show more