feat: Informal lemmas about Higgs bosons

HepLean/StandardModel/HiggsBoson/GaugeAction.lean

@@ -190,6 +190,11 @@ 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 guage_orbit where
+  math :≈ "There exists a `g` in ``GaugeGroupI such that `rep g φ = φ'` if and only if
+    ‖φ‖ = ‖φ'‖."
+  deps :≈ [``rotate_fst_zero_snd_real]
+
 informal_lemma stability_group_single 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 ‖φ‖]`,
@@ -203,7 +208,7 @@ informal_lemma stability_group where
     by the action of ``StandardModel.HiggsVec.rep is given by `SU(3) x ℤ₆` where ℤ₆
     is the subgroup of `SU(2) x U(1)` with elements `(α^(-3) * I₂, α)` where
     α is a sixth root of unity."
-  deps :≈ [``StandardModel.HiggsVec, ``StandardModel.HiggsVec.rep]
+  deps :≈ [``HiggsVec, ``rep]
 
 end HiggsVec
 
@@ -211,5 +216,30 @@ end HiggsVec
 /-! TODO: Prove `⟪φ1, φ2⟫_H` invariant under the global gauge action. (norm_map_of_mem_unitary) -/
 /-! TODO: Prove invariance of potential under global gauge action. -/
 
+namespace HiggsField
+
+/-!
+
+## Gauge transformations acting on Higgs fields.
+
+-/
+
+informal_definition gaugeAction where
+  math :≈ "The action of ``gaugeTransformI on ``HiggsField acting pointwise through
+    ``HiggsVec.rep."
+  deps :≈ [``HiggsVec.rep, ``gaugeTransformI]
+
+informal_lemma guage_orbit where
+  math :≈ "There exists a `g` in ``gaugeTransformI such that `gaugeAction g φ = φ'` if and only if
+    φ(x)^† φ(x) = φ'(x)^† φ'(x)."
+  deps :≈ [``gaugeAction]
+
+informal_lemma gauge_orbit_surject where
+  math :≈ "For every smooth map f from ``SpaceTime to ℝ such that `f` is positive semidefinite,
+    there exists a Higgs field φ such that `f = φ^† φ`."
+  deps :≈ [``HiggsField, ``SpaceTime]
+
+end HiggsField
+
 end StandardModel
 end