diff --git a/HepLean.lean b/HepLean.lean index dcd2d019..b6b3c598 100644 --- a/HepLean.lean +++ b/HepLean.lean @@ -121,24 +121,25 @@ import HepLean.Meta.Remark.Basic import HepLean.Meta.Remark.Properties import HepLean.Meta.TODO.Basic import HepLean.Meta.TransverseTactics -import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.Basic -import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.NormalOrder -import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.StaticWickTheorem -import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.SuperCommute -import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.TimeContraction -import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.TimeOrder -import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.WicksTheoremNormal -import HepLean.PerturbationTheory.Algebras.FieldOpFreeAlgebra.Basic -import HepLean.PerturbationTheory.Algebras.FieldOpFreeAlgebra.Grading -import HepLean.PerturbationTheory.Algebras.FieldOpFreeAlgebra.NormTimeOrder -import HepLean.PerturbationTheory.Algebras.FieldOpFreeAlgebra.NormalOrder -import HepLean.PerturbationTheory.Algebras.FieldOpFreeAlgebra.SuperCommute -import HepLean.PerturbationTheory.Algebras.FieldOpFreeAlgebra.TimeOrder 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.NormalOrder +import HepLean.PerturbationTheory.FieldOpAlgebra.StaticWickTheorem +import HepLean.PerturbationTheory.FieldOpAlgebra.SuperCommute +import HepLean.PerturbationTheory.FieldOpAlgebra.TimeContraction +import HepLean.PerturbationTheory.FieldOpAlgebra.TimeOrder +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 @@ -170,7 +171,6 @@ import HepLean.PerturbationTheory.WickContraction.TimeCond import HepLean.PerturbationTheory.WickContraction.TimeContract import HepLean.PerturbationTheory.WickContraction.Uncontracted import HepLean.PerturbationTheory.WickContraction.UncontractedList -import HepLean.PerturbationTheory.WicksTheorem import HepLean.SpaceTime.Basic import HepLean.SpaceTime.CliffordAlgebra import HepLean.StandardModel.Basic diff --git a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/Basic.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean similarity index 99% rename from HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/Basic.lean rename to HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean index 6c4f2ed3..92ac539c 100644 --- a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/Basic.lean +++ b/HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean @@ -3,7 +3,7 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ -import HepLean.PerturbationTheory.Algebras.FieldOpFreeAlgebra.SuperCommute +import HepLean.PerturbationTheory.FieldOpFreeAlgebra.SuperCommute import Mathlib.Algebra.RingQuot import Mathlib.RingTheory.TwoSidedIdeal.Operations /-! diff --git a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/NormalOrder.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder.lean similarity index 99% rename from HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/NormalOrder.lean rename to HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder.lean index 9eda79a8..9b8aab21 100644 --- a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/NormalOrder.lean +++ b/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder.lean @@ -3,8 +3,8 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ -import HepLean.PerturbationTheory.Algebras.FieldOpFreeAlgebra.NormalOrder -import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.SuperCommute +import HepLean.PerturbationTheory.FieldOpFreeAlgebra.NormalOrder +import HepLean.PerturbationTheory.FieldOpAlgebra.SuperCommute /-! # Normal Ordering on Field operator algebra diff --git a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/StaticWickTheorem.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTheorem.lean similarity index 98% rename from HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/StaticWickTheorem.lean rename to HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTheorem.lean index eb4572ea..599deef2 100644 --- a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/StaticWickTheorem.lean +++ b/HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTheorem.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ import HepLean.PerturbationTheory.WickContraction.StaticContract -import HepLean.PerturbationTheory.WicksTheorem +import HepLean.PerturbationTheory.FieldOpAlgebra.WicksTheorem import HepLean.Meta.Remark.Basic /-! diff --git a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/SuperCommute.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/SuperCommute.lean similarity index 99% rename from HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/SuperCommute.lean rename to HepLean/PerturbationTheory/FieldOpAlgebra/SuperCommute.lean index 81e06a76..68a18512 100644 --- a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/SuperCommute.lean +++ b/HepLean/PerturbationTheory/FieldOpAlgebra/SuperCommute.lean @@ -3,8 +3,8 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ -import HepLean.PerturbationTheory.Algebras.FieldOpFreeAlgebra.TimeOrder -import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.Basic +import HepLean.PerturbationTheory.FieldOpFreeAlgebra.TimeOrder +import HepLean.PerturbationTheory.FieldOpAlgebra.Basic /-! # SuperCommute on Field operator algebra diff --git a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/TimeContraction.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/TimeContraction.lean similarity index 97% rename from HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/TimeContraction.lean rename to HepLean/PerturbationTheory/FieldOpAlgebra/TimeContraction.lean index f74482e5..12d0a427 100644 --- a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/TimeContraction.lean +++ b/HepLean/PerturbationTheory/FieldOpAlgebra/TimeContraction.lean @@ -3,8 +3,8 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ -import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.NormalOrder -import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.TimeOrder +import HepLean.PerturbationTheory.FieldOpAlgebra.NormalOrder +import HepLean.PerturbationTheory.FieldOpAlgebra.TimeOrder /-! # Time contractions diff --git a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/TimeOrder.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/TimeOrder.lean similarity index 99% rename from HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/TimeOrder.lean rename to HepLean/PerturbationTheory/FieldOpAlgebra/TimeOrder.lean index d5407c53..afbf9dd4 100644 --- a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/TimeOrder.lean +++ b/HepLean/PerturbationTheory/FieldOpAlgebra/TimeOrder.lean @@ -3,8 +3,8 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ -import HepLean.PerturbationTheory.Algebras.FieldOpFreeAlgebra.TimeOrder -import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.SuperCommute +import HepLean.PerturbationTheory.FieldOpFreeAlgebra.TimeOrder +import HepLean.PerturbationTheory.FieldOpAlgebra.SuperCommute /-! # Time Ordering on Field operator algebra diff --git a/HepLean/PerturbationTheory/WicksTheorem.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheorem.lean similarity index 100% rename from HepLean/PerturbationTheory/WicksTheorem.lean rename to HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheorem.lean diff --git a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/WicksTheoremNormal.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheoremNormal.lean similarity index 99% rename from HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/WicksTheoremNormal.lean rename to HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheoremNormal.lean index ccd787ae..d2c68756 100644 --- a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/WicksTheoremNormal.lean +++ b/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheoremNormal.lean @@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith -/ import HepLean.PerturbationTheory.WickContraction.TimeCond import HepLean.PerturbationTheory.WickContraction.Sign.Join -import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.StaticWickTheorem +import HepLean.PerturbationTheory.FieldOpAlgebra.StaticWickTheorem import HepLean.Meta.Remark.Basic /-! diff --git a/HepLean/PerturbationTheory/Algebras/FieldOpFreeAlgebra/Basic.lean b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean similarity index 100% rename from HepLean/PerturbationTheory/Algebras/FieldOpFreeAlgebra/Basic.lean rename to HepLean/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean diff --git a/HepLean/PerturbationTheory/Algebras/FieldOpFreeAlgebra/Grading.lean b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Grading.lean similarity index 99% rename from HepLean/PerturbationTheory/Algebras/FieldOpFreeAlgebra/Grading.lean rename to HepLean/PerturbationTheory/FieldOpFreeAlgebra/Grading.lean index 5a8acef2..8f0c9df8 100644 --- a/HepLean/PerturbationTheory/Algebras/FieldOpFreeAlgebra/Grading.lean +++ b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Grading.lean @@ -3,7 +3,7 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ -import HepLean.PerturbationTheory.Algebras.FieldOpFreeAlgebra.Basic +import HepLean.PerturbationTheory.FieldOpFreeAlgebra.Basic import HepLean.PerturbationTheory.Koszul.KoszulSign import Mathlib.RingTheory.GradedAlgebra.Basic /-! diff --git a/HepLean/PerturbationTheory/Algebras/FieldOpFreeAlgebra/NormTimeOrder.lean b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/NormTimeOrder.lean similarity index 94% rename from HepLean/PerturbationTheory/Algebras/FieldOpFreeAlgebra/NormTimeOrder.lean rename to HepLean/PerturbationTheory/FieldOpFreeAlgebra/NormTimeOrder.lean index 8343080b..e247bafd 100644 --- a/HepLean/PerturbationTheory/Algebras/FieldOpFreeAlgebra/NormTimeOrder.lean +++ b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/NormTimeOrder.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ import HepLean.PerturbationTheory.FieldSpecification.TimeOrder -import HepLean.PerturbationTheory.Algebras.FieldOpFreeAlgebra.Basic +import HepLean.PerturbationTheory.FieldOpFreeAlgebra.Basic import HepLean.PerturbationTheory.Koszul.KoszulSign /-! diff --git a/HepLean/PerturbationTheory/Algebras/FieldOpFreeAlgebra/NormalOrder.lean b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/NormalOrder.lean similarity index 99% rename from HepLean/PerturbationTheory/Algebras/FieldOpFreeAlgebra/NormalOrder.lean rename to HepLean/PerturbationTheory/FieldOpFreeAlgebra/NormalOrder.lean index 6dea226d..f3212ca2 100644 --- a/HepLean/PerturbationTheory/Algebras/FieldOpFreeAlgebra/NormalOrder.lean +++ b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/NormalOrder.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ import HepLean.PerturbationTheory.FieldSpecification.NormalOrder -import HepLean.PerturbationTheory.Algebras.FieldOpFreeAlgebra.SuperCommute +import HepLean.PerturbationTheory.FieldOpFreeAlgebra.SuperCommute import HepLean.PerturbationTheory.Koszul.KoszulSign /-! diff --git a/HepLean/PerturbationTheory/Algebras/FieldOpFreeAlgebra/SuperCommute.lean b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/SuperCommute.lean similarity index 99% rename from HepLean/PerturbationTheory/Algebras/FieldOpFreeAlgebra/SuperCommute.lean rename to HepLean/PerturbationTheory/FieldOpFreeAlgebra/SuperCommute.lean index e588bb98..05d8dd65 100644 --- a/HepLean/PerturbationTheory/Algebras/FieldOpFreeAlgebra/SuperCommute.lean +++ b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/SuperCommute.lean @@ -3,8 +3,8 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ -import HepLean.PerturbationTheory.Algebras.FieldOpFreeAlgebra.Basic -import HepLean.PerturbationTheory.Algebras.FieldOpFreeAlgebra.Grading +import HepLean.PerturbationTheory.FieldOpFreeAlgebra.Basic +import HepLean.PerturbationTheory.FieldOpFreeAlgebra.Grading /-! # Super Commute diff --git a/HepLean/PerturbationTheory/Algebras/FieldOpFreeAlgebra/TimeOrder.lean b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/TimeOrder.lean similarity index 99% rename from HepLean/PerturbationTheory/Algebras/FieldOpFreeAlgebra/TimeOrder.lean rename to HepLean/PerturbationTheory/FieldOpFreeAlgebra/TimeOrder.lean index e729e321..6a5ec8f8 100644 --- a/HepLean/PerturbationTheory/Algebras/FieldOpFreeAlgebra/TimeOrder.lean +++ b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/TimeOrder.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ import HepLean.PerturbationTheory.FieldSpecification.TimeOrder -import HepLean.PerturbationTheory.Algebras.FieldOpFreeAlgebra.SuperCommute +import HepLean.PerturbationTheory.FieldOpFreeAlgebra.SuperCommute import HepLean.PerturbationTheory.Koszul.KoszulSign /-! diff --git a/HepLean/PerturbationTheory/WickContraction/Basic.lean b/HepLean/PerturbationTheory/WickContraction/Basic.lean index 1d27072c..b6227ff3 100644 --- a/HepLean/PerturbationTheory/WickContraction/Basic.lean +++ b/HepLean/PerturbationTheory/WickContraction/Basic.lean @@ -3,7 +3,7 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ -import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.NormalOrder +import HepLean.PerturbationTheory.FieldOpAlgebra.NormalOrder import HepLean.Mathematics.List.InsertIdx /-! diff --git a/HepLean/PerturbationTheory/WickContraction/Join.lean b/HepLean/PerturbationTheory/WickContraction/Join.lean index b474e611..67b8e5fd 100644 --- a/HepLean/PerturbationTheory/WickContraction/Join.lean +++ b/HepLean/PerturbationTheory/WickContraction/Join.lean @@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith -/ import HepLean.PerturbationTheory.WickContraction.TimeContract import HepLean.PerturbationTheory.WickContraction.StaticContract -import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.TimeContraction +import HepLean.PerturbationTheory.FieldOpAlgebra.TimeContraction import HepLean.PerturbationTheory.WickContraction.SubContraction import HepLean.PerturbationTheory.WickContraction.Singleton diff --git a/HepLean/PerturbationTheory/WickContraction/StaticContract.lean b/HepLean/PerturbationTheory/WickContraction/StaticContract.lean index 49c368ee..e16a0832 100644 --- a/HepLean/PerturbationTheory/WickContraction/StaticContract.lean +++ b/HepLean/PerturbationTheory/WickContraction/StaticContract.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ import HepLean.PerturbationTheory.WickContraction.Sign.Basic -import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.TimeContraction +import HepLean.PerturbationTheory.FieldOpAlgebra.TimeContraction /-! # Time contractions diff --git a/HepLean/PerturbationTheory/WickContraction/SubContraction.lean b/HepLean/PerturbationTheory/WickContraction/SubContraction.lean index 0f9d75fc..6378c7e0 100644 --- a/HepLean/PerturbationTheory/WickContraction/SubContraction.lean +++ b/HepLean/PerturbationTheory/WickContraction/SubContraction.lean @@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith -/ import HepLean.PerturbationTheory.WickContraction.TimeContract import HepLean.PerturbationTheory.WickContraction.StaticContract -import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.TimeContraction +import HepLean.PerturbationTheory.FieldOpAlgebra.TimeContraction /-! # Sub contractions diff --git a/HepLean/PerturbationTheory/WickContraction/TimeContract.lean b/HepLean/PerturbationTheory/WickContraction/TimeContract.lean index c1d588c8..65632aa7 100644 --- a/HepLean/PerturbationTheory/WickContraction/TimeContract.lean +++ b/HepLean/PerturbationTheory/WickContraction/TimeContract.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ import HepLean.PerturbationTheory.WickContraction.Sign.Basic -import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.TimeContraction +import HepLean.PerturbationTheory.FieldOpAlgebra.TimeContraction /-! # Time contractions diff --git a/README.md b/README.md index e65e9752..fa9f7163 100644 --- a/README.md +++ b/README.md @@ -42,7 +42,7 @@ __BSM physics [🗂️](https://heplean.github.io/HepLean/docs/HepLean/BeyondThe __Flavor physics [🗂️](https://heplean.github.io/HepLean/docs/HepLean/FlavorPhysics/CKMMatrix/Basic.html):__ Properties of the CKM matrix. -__Perturbation Theory [🗂️](https://heplean.github.io/HepLean/docs/HepLean/PerturbationTheory/WicksTheorem.html):__ Time-dependent version of Wick's theorem for both fermions and bosons. +__Perturbation Theory [🗂️](https://heplean.github.io/HepLean/docs/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheorem.html):__ Time-dependent version of Wick's theorem for both fermions and bosons. ## Associated media and publications - [📄](https://arxiv.org/abs/2405.08863) Joseph Tooby-Smith,