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

Merge branch 'master' into TensorNotation

Browse source
This commit is contained in:
jstoobysmith 2024-08-01 06:56:53 -04:00
commit 717c4b0681
11 changed files with 34 additions and 30 deletions
Download patch file Download diff file Expand all files Collapse all files

4
HepLean/AnomalyCancellation/Basic.lean
View file

@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith
-/
import HepLean.Mathematics.LinearMaps
import Mathlib.Algebra.Module.Basic
import Mathlib.LinearAlgebra.FiniteDimensional
import Mathlib.LinearAlgebra.FiniteDimensional.Defs
/-!
# Basic set up for anomaly cancellation conditions
@ -96,7 +96,7 @@ instance linSolsAddCommMonoid (χ : ACCSystemLinear) :
zero := ⟨χ.chargesAddCommMonoid.zero, fun _ ↦ (χ.linearACCs _).map_zero⟩
zero_add S := LinSols.ext (χ.chargesAddCommMonoid.zero_add _)
add_zero S := LinSols.ext (χ.chargesAddCommMonoid.add_zero _)
nsmul n S := ⟨n • S.val, fun _ ↦ by simp [nsmul_eq_smul_cast ℚ, (χ.linearACCs _).map_smul,
nsmul n S := ⟨n • S.val, fun _ ↦ by simp [Nat.cast_smul_eq_nsmul ℚ, (χ.linearACCs _).map_smul,
S.linearSol _]⟩
nsmul_zero n := rfl
nsmul_succ n S := LinSols.ext (χ.chargesAddCommMonoid.nsmul_succ _ _)

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

@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.AnomalyCancellation.Basic
import Mathlib.Algebra.Module.Equiv
import Mathlib.Algebra.Module.Equiv.Basic
import Mathlib.Algebra.BigOperators.Ring
import Mathlib.Algebra.BigOperators.Fin
/-!

2
HepLean/FeynmanDiagrams/Basic.lean
View file

@ -14,7 +14,7 @@ import Mathlib.CategoryTheory.Limits.Shapes.Terminal
import Mathlib.Data.Fintype.Prod
import Mathlib.Data.Fintype.Perm
import Mathlib.Combinatorics.SimpleGraph.Basic
import Mathlib.Combinatorics.SimpleGraph.Connectivity
import Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting
import Mathlib.SetTheory.Cardinal.Basic
/-!
# Feynman diagrams

5
HepLean/FlavorPhysics/CKMMatrix/Relations.lean
View file

@ -189,7 +189,6 @@ lemma conj_Vtb_cross_product {V : CKMMatrix} {τ : ℝ}
simp only [← exp_conj, _root_.map_mul, conj_ofReal, conj_I, mul_neg, Fin.isValue, neg_mul]
field_simp
ring_nf
simp
end crossProduct
@ -199,8 +198,6 @@ lemma conj_Vtb_mul_Vud {V : CKMMatrix} {τ : ℝ}
[V]cs * (normSq [V]ud + normSq [V]us) + [V]cb * conj [V]ub * [V]us := by
rw [conj_Vtb_cross_product hτ]
simp [exp_neg]
have h1 := exp_ne_zero (τ * I)
field_simp
have h2 : ([V]cs * [V]ud - [V]us * [V]cd) * conj [V]ud = [V]cs
* [V]ud * conj [V]ud - [V]us * ([V]cd * conj [V]ud) := by
ring
@ -215,8 +212,6 @@ lemma conj_Vtb_mul_Vus {V : CKMMatrix} {τ : ℝ}
- ([V]cd * (normSq [V]ud + normSq [V]us) + [V]cb * conj ([V]ub) * [V]ud) := by
rw [conj_Vtb_cross_product hτ]
simp [exp_neg]
have h1 := exp_ne_zero (τ * I)
field_simp
have h2 : ([V]cs * [V]ud - [V]us * [V]cd) * conj [V]us = ([V]cs
* conj [V]us) * [V]ud - [V]us * [V]cd * conj [V]us := by
ring

1
HepLean/FlavorPhysics/CKMMatrix/Rows.lean
View file

@ -6,6 +6,7 @@ Authors: Joseph Tooby-Smith
import HepLean.FlavorPhysics.CKMMatrix.Basic
import Mathlib.Analysis.SpecialFunctions.Complex.Arg
import Mathlib.LinearAlgebra.CrossProduct
import Mathlib.LinearAlgebra.FiniteDimensional
/-!
# Rows for the CKM Matrix

3
HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean
View file

@ -359,8 +359,7 @@ lemma mulExpδ₁₃_on_param_eq_zero_iff (V : CKMMatrix) (δ₁₃ : ℝ) :
rw [mulExpδ₁₃_on_param_δ₁₃]
simp only [mul_eq_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, pow_eq_zero_iff,
ofReal_zero]
have h1 := exp_ne_zero (I * δ₁₃)
simp_all
simp only [exp_ne_zero, or_false]
aesop
lemma mulExpδ₁₃_on_param_abs (V : CKMMatrix) (δ₁₃ : ℝ) :

1
HepLean/SpaceTime/Basic.lean
View file

@ -6,7 +6,6 @@ Authors: Joseph Tooby-Smith
import Mathlib.Data.Complex.Exponential
import Mathlib.Geometry.Manifold.SmoothManifoldWithCorners
import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.LinearAlgebra.Matrix.DotProduct
/-!
# Space time

2
README.md
View file

@ -4,7 +4,7 @@
[![](https://img.shields.io/badge/PRs-Welcome-green)](https://github.com/HEPLean/HepLean/pulls)
[![](https://img.shields.io/badge/Lean-Zulip-green)](https://leanprover.zulipchat.com)
[![](https://img.shields.io/badge/TODO-List-green)](https://heplean.github.io/HepLean/TODOList)
[![](https://img.shields.io/badge/Lean-v4.10.0--rc2-blue)](https://github.com/leanprover/lean4/releases/tag/v4.10.0-rc2)
[![](https://img.shields.io/badge/Lean-v4.10.0-blue)](https://github.com/leanprover/lean4/releases/tag/v4.10.0)
A project to digitalize high energy physics.

38
lake-manifest.json
View file

@ -5,7 +5,7 @@
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "c0efc1fd2a0bec51bd55c5b17348af13d7419239",
"rev": "0f3e143dffdc3a591662f3401ce1d7a3405227c0",
"name": "batteries",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
@ -15,7 +15,7 @@
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
"rev": "01ad33937acd996ee99eb74eefb39845e4e4b9f5",
"name": "Qq",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
@ -25,7 +25,7 @@
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "deb5bd446a108da8aa8c1a1b62dd50722b961b73",
"rev": "209712c78b16c795453b6da7f7adbda4589a8f21",
"name": "aesop",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
@ -35,27 +35,27 @@
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "d1b33202c3a29a079f292de65ea438648123b635",
"rev": "c87908619cccadda23f71262e6898b9893bffa36",
"name": "proofwidgets",
"manifestFile": "lake-manifest.json",
"inputRev": "v0.0.39",
"inputRev": "v0.0.40",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover/lean4-cli",
"type": "git",
"subDir": null,
"scope": "",
"rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
"rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
"name": "Cli",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
"configFile": "lakefile.lean"},
"configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover-community/import-graph",
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7",
"rev": "543725b3bfed792097fc134adca628406f6145f5",
"name": "importGraph",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
@ -65,17 +65,17 @@
"type": "git",
"subDir": null,
"scope": "",
"rev": "984c68d7773ac133c74543b99b82c33e53baea6b",
"rev": "a719ba5c3115d47b68bf0497a9dd1bcbb21ea663",
"name": "mathlib",
"manifestFile": "lake-manifest.json",
"inputRev": "v4.10.0-rc2",
"inputRev": "v4.10.0",
"inherited": false,
"configFile": "lakefile.lean"},
{"url": "https://github.com/acmepjz/md4lean",
"type": "git",
"subDir": null,
"scope": "",
"rev": "9148a0a7506099963925cf239c491fcda5ed0044",
"rev": "5e95f4776be5e048364f325c7e9d619bb56fb005",
"name": "MD4Lean",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
@ -85,20 +85,30 @@
"type": "git",
"subDir": null,
"scope": "",
"rev": "c74a052aebee847780e165611099854de050adf7",
"rev": "5c11428272fe190b7e726ebe448f93437d057b74",
"name": "UnicodeBasic",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/dupuisf/BibtexQuery",
"type": "git",
"subDir": null,
"scope": "",
"rev": "bd8747df9ee72fca365efa5bd3bd0d8dcd083b9f",
"name": "BibtexQuery",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover/doc-gen4",
"type": "git",
"subDir": null,
"scope": "",
"rev": "c369436d21c583a60da62d4513c7b9ea08389074",
"rev": "593ac5bd2ca98c5294675b5cccf3d89b300a76eb",
"name": "«doc-gen4»",
"manifestFile": "lake-manifest.json",
"inputRev": "v4.10.0-rc1",
"inputRev": "v4.10.0",
"inherited": false,
"configFile": "lakefile.lean"}],
"name": "hep_lean",

4
lakefile.toml
View file

@ -6,12 +6,12 @@ defaultTargets = ["HepLean"]
[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4.git"
rev = "v4.10.0-rc2"
rev = "v4.10.0"
[[require]]
name = "«doc-gen4»"
git = "https://github.com/leanprover/doc-gen4"
rev = "v4.10.0-rc1"
rev = "v4.10.0"
[[lean_lib]]
name = "HepLean"

2
lean-toolchain
View file

@ -1 +1 @@
leanprover/lean4:v4.10.0-rc2
leanprover/lean4:v4.10.0