feat: Examples of informal_lemmas

HepLean/StandardModel/HiggsBoson/Basic.lean

@@ -11,6 +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
 /-!
 
 # The Higgs field
@@ -173,6 +174,11 @@ def ofReal (a : ℝ) : HiggsField := (HiggsVec.ofReal a).toField
 /-- The higgs field which is all zero. -/
 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`
+    is the constant zero-section of the bundle `HiggsBundle`."
+
 end HiggsField
 
 end

HepLean/StandardModel/HiggsBoson/Potential.lean

@@ -5,6 +5,7 @@ Authors: Joseph Tooby-Smith
 -/
 import Mathlib.Algebra.QuadraticDiscriminant
 import HepLean.StandardModel.HiggsBoson.PointwiseInnerProd
+import HepLean.Meta.InformalDef
 /-!
 # The potential of the Higgs field
 
@@ -314,6 +315,12 @@ lemma isBounded_of_𝓵_pos (h : 0 < P.𝓵) : P.IsBounded := by
   have h2' := h2 φ x
   linarith
 
+informal_lemma isBounded_iff_of_𝓵_zero where
+  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.
+    That is to say `- P.μ2 * ‖φ‖_H ^ 2 x` is bounded below if and only if `P.μ2 ≤ 0`."
+
 /-!
 
 ## Minimum and maximum