refactor: Lint
This commit is contained in:
jstoobysmith
parent
5327c2249f
commit
016fb72af8
7 changed files with 113 additions and 85 deletions
|
|
@ -61,6 +61,7 @@ import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.StandardParamete
|
|||
import HepLean.Mathematics.LinearMaps
|
||||
import HepLean.Mathematics.SO3.Basic
|
||||
import HepLean.Meta.AllFilePaths
|
||||
import HepLean.Meta.Informal
|
||||
import HepLean.Meta.TransverseTactics
|
||||
import HepLean.SpaceTime.Basic
|
||||
import HepLean.SpaceTime.CliffordAlgebra
|
||||
|
|
|
|||
103
HepLean/Meta/Informal.lean
Normal file
103
HepLean/Meta/Informal.lean
Normal file
|
|
@ -0,0 +1,103 @@
|
|||
/-
|
||||
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
|
||||
Released under Apache 2.0 license.
|
||||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import Lean
|
||||
/-!
|
||||
|
||||
## Informal definitions and lemmas
|
||||
|
||||
-/
|
||||
open Lean Elab System
|
||||
|
||||
/-! TODO: Derive a means to extract informal definitions and informal lemmas. -/
|
||||
|
||||
/-- The structure representating an informal definition. -/
|
||||
structure InformalDefinition where
|
||||
/-- The name of the informal definition. This is autogenerated. -/
|
||||
name : Name
|
||||
/-- The mathematical description of the definition. -/
|
||||
math : String
|
||||
/-- The physics description of the definition. -/
|
||||
physics : String
|
||||
|
||||
/-- The structure representating an informal proof. -/
|
||||
structure InformalLemma where
|
||||
/-- The name of the informal lemma. This is autogenerated. -/
|
||||
name : Name
|
||||
/-- The mathematical description of the lemma. -/
|
||||
math : String
|
||||
/-- The physics description of the lemma. -/
|
||||
physics : String
|
||||
/-- A description of the proof. -/
|
||||
proof : String
|
||||
|
||||
namespace Informal
|
||||
|
||||
/-- The Parser.Category we will use for assignments. -/
|
||||
declare_syntax_cat informalAssignment
|
||||
|
||||
/-- The syntax describing an informal assignment of `ident` to a string. -/
|
||||
syntax (name := informalAssignment) ident ":≈" str : informalAssignment
|
||||
|
||||
/-- The syntax for the command informal_definition. -/
|
||||
syntax (name := informal_definition) "informal_definition " ident
|
||||
" where " (colGt informalAssignment)* : command
|
||||
|
||||
/-- The macro turning `informal_definition ... where ...` into a definition. -/
|
||||
macro "informal_definition " name:ident " where " assignments:informalAssignment* : command => do
|
||||
let mut math_def? : Option (TSyntax `term) := none
|
||||
let mut physics_def? : Option (TSyntax `term) := none
|
||||
for assignment in assignments do
|
||||
match assignment with
|
||||
| `(informalAssignment| physics :≈ $val:str) =>
|
||||
let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for physics"
|
||||
physics_def? := some (← `($(Lean.quote strVal)))
|
||||
| `(informalAssignment| math :≈ $val:str) =>
|
||||
let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for math"
|
||||
math_def? := some (← `($(Lean.quote strVal)))
|
||||
| _ => Macro.throwError "invalid assignment syntax"
|
||||
unless physics_def?.isSome && math_def?.isSome do
|
||||
Macro.throwError "Both 'physics' and 'math' assignments are required"
|
||||
`(
|
||||
/-- An informal definition. -/
|
||||
def $name : InformalDefinition := {
|
||||
name := $(Lean.quote name.getId),
|
||||
physics := $(physics_def?.getD (← `("No physics description provided"))),
|
||||
math := $(math_def?.getD (panic! "math not assigned"))
|
||||
})
|
||||
|
||||
/-- The syntax for the command `informal_lemma`. -/
|
||||
syntax (name := informal_lemma) "informal_lemma " ident " where "
|
||||
(colGt informalAssignment)* : command
|
||||
|
||||
/-- The macro turning `informal_lemma ... where ...` into a definition. -/
|
||||
macro "informal_lemma " name:ident " where " assignments:informalAssignment* : command => do
|
||||
let mut math_def? : Option (TSyntax `term) := none
|
||||
let mut physics_def? : Option (TSyntax `term) := none
|
||||
let mut proof_def? : Option (TSyntax `term) := none
|
||||
for assignment in assignments do
|
||||
match assignment with
|
||||
| `(informalAssignment| physics :≈ $val:str) =>
|
||||
let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for physics"
|
||||
physics_def? := some (← `($(Lean.quote strVal)))
|
||||
| `(informalAssignment| math :≈ $val:str) =>
|
||||
let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for math"
|
||||
math_def? := some (← `($(Lean.quote strVal)))
|
||||
| `(informalAssignment| proof :≈ $val:str) =>
|
||||
let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for proof"
|
||||
proof_def? := some (← `($(Lean.quote strVal)))
|
||||
| _ => Macro.throwError "invalid assignment syntax"
|
||||
unless math_def?.isSome do
|
||||
Macro.throwError "Both 'physics' and 'math' assignments are required"
|
||||
`(
|
||||
/-- An informal lemma. -/
|
||||
def $name : InformalLemma := {
|
||||
name := $(Lean.quote name.getId),
|
||||
physics := $(physics_def?.getD (← `("No physics description provided"))),
|
||||
math := $(math_def?.getD (panic! "math not assigned")),
|
||||
proof := $(proof_def?.getD (← `("No proof description provided"))),
|
||||
})
|
||||
|
||||
end Informal
|
||||
|
|
@ -1,75 +0,0 @@
|
|||
import Lean
|
||||
|
||||
open Lean Elab System
|
||||
|
||||
structure InformalDefinition where
|
||||
name : Name
|
||||
math_t : String
|
||||
physics_t : String
|
||||
|
||||
structure InformalLemma where
|
||||
name : Name
|
||||
math_t : String
|
||||
physics_t : String
|
||||
|
||||
namespace InformalDefinition
|
||||
|
||||
declare_syntax_cat assignment
|
||||
|
||||
syntax (name := physics_assignment) "physics := " str : assignment
|
||||
syntax (name := math_assignment) "math := " str : assignment
|
||||
|
||||
syntax (name := informal_definition) "informal_definition " ident " where " (colGt assignment)* : command
|
||||
|
||||
|
||||
macro "informal_definition " name:ident " where " assignments:assignment* : command => do
|
||||
let mut math_def? : Option (TSyntax `term) := none
|
||||
let mut physics_def? : Option (TSyntax `term) := none
|
||||
for assignment in assignments do
|
||||
match assignment with
|
||||
| `(assignment| physics := $val:str) =>
|
||||
let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for physics"
|
||||
physics_def? := some (← `($(Lean.quote strVal)))
|
||||
| `(assignment| math := $val:str) =>
|
||||
let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for math"
|
||||
math_def? := some (← `($(Lean.quote strVal)))
|
||||
| _ => Macro.throwError "invalid assignment syntax"
|
||||
|
||||
unless physics_def?.isSome && math_def?.isSome do
|
||||
Macro.throwError "Both 'physics' and 'math' assignments are required"
|
||||
|
||||
`(
|
||||
def $name : InformalDefinition := {
|
||||
name := $(Lean.quote name.getId),
|
||||
physics_t := $(physics_def?.getD (panic! "physics not assigned")),
|
||||
math_t := $(math_def?.getD (panic! "math not assigned"))
|
||||
}
|
||||
)
|
||||
|
||||
syntax (name := informal_lemma) "informal_lemma " ident " where " (colGt assignment)* : command
|
||||
|
||||
macro "informal_lemma " name:ident " where " assignments:assignment* : command => do
|
||||
let mut math_def? : Option (TSyntax `term) := none
|
||||
let mut physics_def? : Option (TSyntax `term) := none
|
||||
for assignment in assignments do
|
||||
match assignment with
|
||||
| `(assignment| physics := $val:str) =>
|
||||
let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for physics"
|
||||
physics_def? := some (← `($(Lean.quote strVal)))
|
||||
| `(assignment| math := $val:str) =>
|
||||
let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for math"
|
||||
math_def? := some (← `($(Lean.quote strVal)))
|
||||
| _ => Macro.throwError "invalid assignment syntax"
|
||||
|
||||
unless physics_def?.isSome && math_def?.isSome do
|
||||
Macro.throwError "Both 'physics' and 'math' assignments are required"
|
||||
|
||||
`(
|
||||
def $name : InformalDefinition := {
|
||||
name := $(Lean.quote name.getId),
|
||||
physics_t := $(physics_def?.getD (panic! "physics not assigned")),
|
||||
math_t := $(math_def?.getD (panic! "math not assigned"))
|
||||
}
|
||||
)
|
||||
|
||||
end InformalDefinition
|
||||
|
|
@ -6,7 +6,6 @@ Authors: Joseph Tooby-Smith
|
|||
import Mathlib.Data.Complex.Exponential
|
||||
import Mathlib.Geometry.Manifold.Instances.Real
|
||||
import Mathlib.LinearAlgebra.Matrix.ToLin
|
||||
import HepLean.Meta.InformalDef
|
||||
/-!
|
||||
# The Standard Model
|
||||
|
||||
|
|
|
|||
|
|
@ -11,7 +11,7 @@ import Mathlib.Geometry.Manifold.VectorBundle.SmoothSection
|
|||
import Mathlib.Geometry.Manifold.Instances.Real
|
||||
import Mathlib.Analysis.InnerProductSpace.Basic
|
||||
import Mathlib.Geometry.Manifold.ContMDiff.Product
|
||||
import HepLean.Meta.InformalDef
|
||||
import HepLean.Meta.Informal
|
||||
/-!
|
||||
|
||||
# The Higgs field
|
||||
|
|
@ -175,8 +175,8 @@ def ofReal (a : ℝ) : HiggsField := (HiggsVec.ofReal a).toField
|
|||
def zero : HiggsField := ofReal 0
|
||||
|
||||
informal_lemma zero_is_zero_section where
|
||||
physics := "The zero Higgs field is the zero section of the Higgs bundle."
|
||||
math := "The HiggsField `zero` defined by `ofReal 0`
|
||||
physics :≈ "The zero Higgs field is the zero section of the Higgs bundle."
|
||||
math :≈ "The HiggsField `zero` defined by `ofReal 0`
|
||||
is the constant zero-section of the bundle `HiggsBundle`."
|
||||
|
||||
end HiggsField
|
||||
|
|
|
|||
|
|
@ -191,9 +191,9 @@ theorem rotate_fst_real_snd_zero (φ : HiggsVec) :
|
|||
tail_cons, smul_zero]
|
||||
|
||||
informal_lemma stablity_group where
|
||||
physics := "The Higgs boson breaks electroweak symmetry down to the electromagnetic force."
|
||||
math := "The stablity group of the action of `rep` on `![0, Complex.ofReal ‖φ‖]`,
|
||||
for non-zero `‖φ‖` is the `SU(3) x U(1)` subgroup of
|
||||
physics :≈ "The Higgs boson breaks electroweak symmetry down to the electromagnetic force."
|
||||
math :≈ "The stablity group of the action of `rep` on `![0, Complex.ofReal ‖φ‖]`,
|
||||
for non-zero `‖φ‖` is the `SU(3) x U(1)` subgroup of
|
||||
`gaugeGroup := SU(3) x SU(2) x U(1)` with the embedding given by
|
||||
`(g, e^{i θ}) ↦ (g, diag (e ^ {3 * i θ}, e ^ {- 3 * i θ}), e^{i θ})`."
|
||||
|
||||
|
|
|
|||
|
|
@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith
|
|||
-/
|
||||
import Mathlib.Algebra.QuadraticDiscriminant
|
||||
import HepLean.StandardModel.HiggsBoson.PointwiseInnerProd
|
||||
import HepLean.Meta.InformalDef
|
||||
import HepLean.Meta.Informal
|
||||
/-!
|
||||
# The potential of the Higgs field
|
||||
|
||||
|
|
@ -316,9 +316,9 @@ lemma isBounded_of_𝓵_pos (h : 0 < P.𝓵) : P.IsBounded := by
|
|||
linarith
|
||||
|
||||
informal_lemma isBounded_iff_of_𝓵_zero where
|
||||
physics := "When there is no quartic coupling, the potential is bounded iff the mass squared is
|
||||
physics :≈ "When there is no quartic coupling, the potential is bounded iff the mass squared is
|
||||
non-positive."
|
||||
math := "For `P : Potential` then P.IsBounded if and only if P.μ2 ≤ 0.
|
||||
math :≈ "For `P : Potential` then P.IsBounded if and only if P.μ2 ≤ 0.
|
||||
That is to say `- P.μ2 * ‖φ‖_H ^ 2 x` is bounded below if and only if `P.μ2 ≤ 0`."
|
||||
|
||||
/-!
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue