feat: Add informal_definition and informal_lemma

HepLean/Meta/InformalDef.lean

@@ -0,0 +1,75 @@
+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

HepLean/StandardModel/Basic.lean

@@ -6,6 +6,7 @@ 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
 

HepLean/StandardModel/HiggsBoson/GaugeAction.lean

@@ -190,6 +190,13 @@ theorem rotate_fst_real_snd_zero (φ : HiggsVec) :
   · simp only [Fin.mk_one, Fin.isValue, Pi.smul_apply, Function.comp_apply, cons_val_one, head_cons,
       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
+    `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 θ})`."
+
 end HiggsVec
 
 /-! TODO: Define the global gauge action on HiggsField. -/