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

feat: stats and AI doc strings

Browse source
This commit is contained in:
jstoobysmith 2024-07-15 14:52:50 -04:00
parent a17c98e922
commit d6460e62bc
19 changed files with 162 additions and 40 deletions
Download patch file Download diff file Expand all files Collapse all files

10
HepLean/AnomalyCancellation/Basic.lean
View file

@ -119,7 +119,7 @@ instance linSolsAddCommMonoid (χ : ACCSystemLinear) :
apply LinSols.ext
exact χ.chargesAddCommMonoid.nsmul_succ _ _
/-- An instance providing the operations and properties for `LinSols` to form an
/-- An instance providing the operations and properties for `LinSols` to form a
module over `ℚ`. -/
@[simps!]
instance linSolsModule (χ : ACCSystemLinear) : Module ℚ χ.LinSols where
@ -147,7 +147,7 @@ instance linSolsModule (χ : ACCSystemLinear) : Module ℚ χ.LinSols where
exact χ.chargesModule.add_smul _ _ _
/-- An instance providing the operations and properties for `LinSols` to form an
an additive community. -/
additive commutative group. -/
instance linSolsAddCommGroup (χ : ACCSystemLinear) : AddCommGroup χ.LinSols :=
Module.addCommMonoidToAddCommGroup ℚ
@ -201,8 +201,8 @@ def quadSolsInclLinSols (χ : ACCSystemQuad) : χ.QuadSols →[ℚ] χ.LinSols w
toFun := QuadSols.toLinSols
map_smul' _ _ := rfl
/-- If there are no quadratic equations (i.e. no U(1)'s in the underlying gauge group. The inclusion
of linear solutions into quadratic solutions. -/
/-- The inclusion of the linear solutions into the quadratic solutions, where there is
no quadratic equations (i.e. no U(1)'s in the underlying gauge group). -/
def linSolsInclQuadSolsZero (χ : ACCSystemQuad) (h : χ.numberQuadratic = 0) :
χ.LinSols →[ℚ] χ.QuadSols where
toFun S := ⟨S, by intro i; rw [h] at i; exact Fin.elim0 i⟩
@ -233,7 +233,7 @@ lemma Sols.ext {χ : ACCSystem} {S T : χ.Sols} (h : S.val = T.val) :
cases' S
simp_all only
/-- We say a charge S is a solution if it extends to a solution. -/
/-- A charge `S` is a solution if it extends to a solution. -/
def IsSolution (χ : ACCSystem) (S : χ.Charges) : Prop :=
∃ (sol : χ.Sols), sol.val = S

10
HepLean/AnomalyCancellation/GroupActions.lean
View file

@ -18,13 +18,13 @@ From this we define
-/
/-- The type of of a group action on a system of charges is defined as a representation on
/-- The type of a group action on a system of charges is defined as a representation on
the vector spaces of charges under which the anomaly equations are invariant.
-/
structure ACCSystemGroupAction (χ : ACCSystem) where
/-- The underlying type of the group. -/
group : Type
/-- An instance given group the structure of a group. -/
/-- An instance given the `group` component the structure of a `Group`. -/
groupInst : Group group
/-- The representation of group acting on the vector space of charges. -/
rep : Representation ℚ group χ.Charges
@ -79,8 +79,7 @@ lemma rep_linSolRep_commute {χ : ACCSystem} (G : ACCSystemGroupAction χ) (g :
(S : χ.LinSols) : χ.linSolsIncl (G.linSolRep g S) =
G.rep g (χ.linSolsIncl S) := rfl
/-- An instance given the structure to define a multiplicative action of `G.group` on `quadSols`.
-/
/-- A multiplicative action of `G.group` on `quadSols`. -/
instance quadSolAction {χ : ACCSystem} (G : ACCSystemGroupAction χ) :
MulAction G.group χ.QuadSols where
smul f S := ⟨G.linSolRep f S.1, by
@ -112,8 +111,7 @@ instance solAction {χ : ACCSystem} (G : ACCSystemGroupAction χ) : MulAction G.
smul g S := ⟨G.quadSolAction.toFun S.1 g, by
simp only [MulAction.toFun_apply]
change χ.cubicACC (G.rep g S.val) = 0
rw [G.cubicInvariant, S.cubicSol]
⟩
rw [G.cubicInvariant, S.cubicSol]⟩
mul_smul f1 f2 S := by
apply ACCSystem.Sols.ext
change (G.rep.toFun (f1 * f2)) S.val = _

20
HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean
View file

@ -48,7 +48,7 @@ def LineEqPropSol (R : MSSMACC.Sols) : Prop :=
cubeTriLin R.val R.val Y₃.val * quadBiLin B₃.val R.val -
cubeTriLin R.val R.val B₃.val * quadBiLin Y₃.val R.val = 0
/-- A rational which appears in `toSolNS` acting on sols, and which been zero is
/-- A rational which appears in `toSolNS` acting on sols, and which being zero is
equivalent to satisfying `lineEqPropSol`. -/
def lineEqCoeff (T : MSSMACC.Sols) : ℚ := dot Y₃.val B₃.val * α₃ (proj T.1.1)
@ -185,30 +185,30 @@ lemma inCubeSolProp_iff_proj_inCubeProp (R : MSSMACC.Sols) :
`lineEqProp`. -/
def InLineEq : Type := {R : MSSMACC.AnomalyFreePerp // LineEqProp R}
/-- Those charge assignments perpendicular to `Y₃` and `B₃` which satisfy the condition
/-- Those charge assignments perpendicular to `Y₃` and `B₃` which satisfy the conditions
`lineEqProp` and `inQuadProp`. -/
def InQuad : Type := {R : InLineEq // InQuadProp R.val}
/-- Those charge assignments perpendicular to `Y₃` and `B₃` which satisfy the condition
/-- Those charge assignments perpendicular to `Y₃` and `B₃` which satisfy the conditions
`lineEqProp`, `inQuadProp` and `inCubeProp`. -/
def InQuadCube : Type := {R : InQuad // InCubeProp R.val.val}
/-- Those solutions which do not satisfy the condition `lineEqPropSol`. -/
def NotInLineEqSol : Type := {R : MSSMACC.Sols // ¬ LineEqPropSol R}
/-- Those solutions which satisfy the condition `lineEqPropSol` by not `inQuadSolProp`. -/
/-- Those solutions which satisfy the condition `lineEqPropSol` but not `inQuadSolProp`. -/
def InLineEqSol : Type := {R : MSSMACC.Sols // LineEqPropSol R ∧ ¬ InQuadSolProp R}
/-- Those solutions which satisfy the condition `lineEqPropSol` and `inQuadSolProp` but
not `inCubeSolProp`. -/
def InQuadSol : Type := {R : MSSMACC.Sols // LineEqPropSol R ∧ InQuadSolProp R ∧ ¬ InCubeSolProp R}
/-- Those solutions which satisfy the condition all the conditions `lineEqPropSol`, `inQuadSolProp`
/-- Those solutions which satisfy the conditions `lineEqPropSol`, `inQuadSolProp`
and `inCubeSolProp`. -/
def InQuadCubeSol : Type :=
{R : MSSMACC.Sols // LineEqPropSol R ∧ InQuadSolProp R ∧ InCubeSolProp R}
/-- Given a `R` perpendicular to `Y₃` and `B₃` a quadratic solution. -/
/-- Given an `R` perpendicular to `Y₃` and `B₃` a quadratic solution. -/
def toSolNSQuad (R : MSSMACC.AnomalyFreePerp) : MSSMACC.QuadSols :=
lineQuad R
(3 * cubeTriLin R.val R.val Y₃.val)
@ -230,7 +230,7 @@ lemma toSolNSQuad_eq_planeY₃B₃_on_α (R : MSSMACC.AnomalyFreePerp) :
ring_nf
simp
/-- Given a `R ` perpendicular to `Y₃` and `B₃`, an element of `Sols`. This map is
/-- Given an `R` perpendicular to `Y₃` and `B₃`, an element of `Sols`. This map is
not surjective. -/
def toSolNS : MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, a, _ , _) =>
a • AnomalyFreeMk'' (toSolNSQuad R) (toSolNSQuad_cube R)
@ -258,7 +258,7 @@ lemma toSolNS_proj (T : NotInLineEqSol) : toSolNS (toSolNSProj T.val) = T.val :=
rw [← MulAction.mul_smul, mul_comm, mul_inv_cancel h1]
simp
/-- Given a element of `inLineEq × ℚ × ℚ × ℚ`, a solution to the ACCs. -/
/-- A solution to the ACCs, given an element of `inLineEq × ℚ × ℚ × ℚ`. -/
def inLineEqToSol : InLineEq × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, c₁, c₂, c₃) =>
AnomalyFreeMk'' (lineQuad R.val c₁ c₂ c₃)
(by
@ -301,7 +301,7 @@ lemma inLineEqToSol_proj (T : InLineEqSol) : inLineEqToSol (inLineEqProj T) = T.
rw [← MulAction.mul_smul, mul_comm, mul_inv_cancel h2]
simp
/-- Given a element of `inQuad × ℚ × ℚ × ℚ`, a solution to the ACCs. -/
/-- Given an element of `inQuad × ℚ × ℚ × ℚ`, a solution to the ACCs. -/
def inQuadToSol : InQuad × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, a₁, a₂, a₃) =>
AnomalyFreeMk' (lineCube R.val.val a₁ a₂ a₃)
(by
@ -389,7 +389,7 @@ lemma inQuadCubeToSol_proj (T : InQuadCubeSol) :
rw [show dot Y₃.val B₃.val = 108 by rfl]
simp
/-- Given an element of `MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ` a solution. We will
/-- A solution from an element of `MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ`. We will
show that this map is a surjection. -/
def toSol : MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, a, b, c) =>
if h₃ : LineEqProp R ∧ InQuadProp R ∧ InCubeProp R then

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

@ -136,7 +136,7 @@ lemma boundary_accGrav'' (k : Fin n) (hk : Boundary S k) :
rw [boundary_castSucc hS hk, boundary_succ hS hk]
ring
/-- We say a `S ∈ charges` has a boundary if there exists a `k ∈ Fin n` which is a boundary. -/
/-- A `S ∈ charges` has a boundary if there exists a `k ∈ Fin n` which is a boundary. -/
@[simp]
def HasBoundary (S : (PureU1 n.succ).Charges) : Prop :=
∃ (k : Fin n), Boundary S k

2
HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean
View file

@ -667,7 +667,7 @@ lemma basisa_card : Fintype.card ((Fin n.succ) ⊕ (Fin n)) =
simp only [Fintype.card_sum, Fintype.card_fin, mul_eq]
omega
/-- The basis formed out of our basisa vectors. -/
/-- The basis formed out of our `basisa` vectors. -/
noncomputable def basisaAsBasis :
Basis (Fin (succ n) ⊕ Fin n) ℚ (PureU1 (2 * succ n)).LinSols :=
basisOfLinearIndependentOfCardEqFinrank (@basisa_linear_independent n) basisa_card

2
HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean
View file

@ -67,7 +67,7 @@ lemma line_in_cubic_P_P_P! {S : (PureU1 (2 * n.succ)).LinSols} (h : LineInCubic
linear_combination 2 / 3 * (lineInCubic_expand h g f hS 1 1) -
(lineInCubic_expand h g f hS 1 2) / 6
/-- We say a `LinSol` satisfies `lineInCubicPerm` if all its permutations satisfy `lineInCubic`. -/
/-- A `LinSol` satisfies `LineInCubicPerm` if all its permutations satisfy `lineInCubic`. -/
def LineInCubicPerm (S : (PureU1 (2 * n.succ)).LinSols) : Prop :=
∀ (M : (FamilyPermutations (2 * n.succ)).group),
LineInCubic ((FamilyPermutations (2 * n.succ)).linSolRep M S)

6
HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
View file

@ -61,16 +61,16 @@ lemma line_in_cubic_P_P_P! {S : (PureU1 (2 * n + 1)).LinSols} (h : LineInCubic S
linear_combination 2 / 3 * (lineInCubic_expand h g f hS 1 1) -
(lineInCubic_expand h g f hS 1 2) / 6
/-- We say a `LinSol` satisfies `lineInCubicPerm` if all its permutations satisfy `lineInCubic`. -/
/-- A `LinSol` satisfies `lineInCubicPerm` if all its permutations satisfy `lineInCubic`. -/
def LineInCubicPerm (S : (PureU1 (2 * n + 1)).LinSols) : Prop :=
∀ (M : (FamilyPermutations (2 * n + 1)).group),
LineInCubic ((FamilyPermutations (2 * n + 1)).linSolRep M S)
/-- If `lineInCubicPerm S` then `lineInCubic S`. -/
/-- If `lineInCubicPerm S`, then `lineInCubic S`. -/
lemma lineInCubicPerm_self {S : (PureU1 (2 * n + 1)).LinSols} (hS : LineInCubicPerm S) :
LineInCubic S := hS 1
/-- If `lineInCubicPerm S` then `lineInCubicPerm (M S)` for all permutations `M`. -/
/-- If `lineInCubicPerm S`, then `lineInCubicPerm (M S)` for all permutations `M`. -/
lemma lineInCubicPerm_permute {S : (PureU1 (2 * n + 1)).LinSols}
(hS : LineInCubicPerm S) (M' : (FamilyPermutations (2 * n + 1)).group) :
LineInCubicPerm ((FamilyPermutations (2 * n + 1)).linSolRep M' S) := by

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

@ -21,7 +21,7 @@ namespace PureU1
variable {n : ℕ}
/-- We say a charge is shorted if for all `i ≤ j`, then `S i ≤ S j`. -/
/-- A charge is sorted if for all `i ≤ j`, then `S i ≤ S j`. -/
@[simp]
def Sorted {n : ℕ} (S : (PureU1 n).Charges) : Prop :=
∀ i j (_ : i ≤ j), S i ≤ S j