diff --git a/Physlib.lean b/Physlib.lean
index 981f36e36..be65098f9 100644
--- a/Physlib.lean
+++ b/Physlib.lean
@@ -113,6 +113,8 @@ public import Physlib.Mathematics.Resolvent
 public import Physlib.Mathematics.SO3.Basic
 public import Physlib.Mathematics.SchurTriangulation
 public import Physlib.Mathematics.SpecialFunctions.PhysHermite
+public import Physlib.Mathematics.SymmetricAlgebra.OfSymmetric
+public import Physlib.Mathematics.SymmetricAlgebra.SymmetricMap
 public import Physlib.Mathematics.Trigonometry.Tanh
 public import Physlib.Mathematics.VariationalCalculus.Basic
 public import Physlib.Mathematics.VariationalCalculus.HasVarAdjDeriv
@@ -176,6 +178,7 @@ public import Physlib.Particles.StandardModel.AnomalyCancellation.Permutations
 public import Physlib.Particles.StandardModel.Basic
 public import Physlib.Particles.StandardModel.Fermions.QuarkDoublet
 public import Physlib.Particles.StandardModel.HiggsBoson.Basic
+public import Physlib.Particles.StandardModel.HiggsBoson.EFTLagrangianExclDeriv
 public import Physlib.Particles.StandardModel.HiggsBoson.EffectivePotential
 public import Physlib.Particles.StandardModel.HiggsBoson.Potential
 public import Physlib.Particles.StandardModel.Representations
diff --git a/Physlib/Mathematics/SymmetricAlgebra/OfSymmetric.lean b/Physlib/Mathematics/SymmetricAlgebra/OfSymmetric.lean
new file mode 100644
index 000000000..b105991d2
--- /dev/null
+++ b/Physlib/Mathematics/SymmetricAlgebra/OfSymmetric.lean
@@ -0,0 +1,477 @@
+/-
+Copyright (c) 2026 Nathaneal Sajan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nathaneal Sajan
+-/
+module
+
+public import Mathlib.Algebra.BigOperators.Fin
+public import Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
+import Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
+import Mathlib.LinearAlgebra.PiTensorProduct.Basic
+import Mathlib.Algebra.DirectSum.Module
+public import Physlib.Mathematics.SymmetricAlgebra.SymmetricMap
+-- `TensorAlgebra.symRingCon` is `@[no_expose]`, so a plain `public import` does not expose its
+-- body and `symRingCon = ringConGen (SymRel ..)` is not available. This private `import all`
+-- supplies it.
+import all Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
+
+/-!
+# Symmetric monomials and the lift out of the symmetric algebra
+
+## i. Overview
+
+The symmetric algebra `SymmetricAlgebra R M` is the tensor algebra quotiented by the congruence
+forcing generators to commute. This file supplies the multilinear constructions mapping into and out
+of it.
+
+`ιMulti` maps in. It sends a tuple `v : Fin n → M` to the product of the corresponding generators.
+Its symmetry is permutation invariance of a finite product in a commutative algebra.
+
+`liftSymmetric` maps out. It takes a family of symmetric multilinear maps, one in each degree, and
+assembles them into a single linear map on the symmetric algebra, sending a degree-`n` monomial to
+the value prescribed in degree `n`. The target `N` need only be an `R`-module: the assembled map is
+linear but in general not multiplicative, so the family may prescribe unrelated behaviour in each
+degree.
+
+The construction passes through tensor powers and their direct sum, then descends from the tensor
+algebra through the symmetric congruence. Symmetry supplies the contextual permutation invariance
+required for this descent.
+
+## ii. Key results
+
+- `SymmetricAlgebra.ιMulti` : the symmetric multilinear map sending a tuple to the product of the
+  corresponding generators.
+- `SymmetricAlgebra.liftSymmetric` : the assembly of a degreewise family of symmetric multilinear
+  maps into a linear map on the symmetric algebra, itself linear in the family.
+- `SymmetricAlgebra.liftSymmetric_apply_ιMulti` : the defining computation on monomials.
+- `SymmetricAlgebra.lhom_ext` : a linear map out of the symmetric algebra is determined by its
+  values on monomials.
+- `SymmetricAlgebra.liftSymmetricEquiv` : the construction packaged as a linear equivalence.
+
+The supporting computation and composition lemmas are documented at their declarations.
+
+## iii. Table of contents
+
+- A. Products of symmetric algebra generators
+  - A.1. Definition
+  - A.2. Computation lemmas
+- B. The lift out of the symmetric algebra
+  - B.1. A pure `Fin`-coordinate lemma
+  - B.2. Internal helpers (family-independent)
+  - B.3. Internal helpers (family-dependent)
+  - B.4. Extensionality
+  - B.5. The bundled lift and its API
+
+## iv. References
+
+- Bergman, Tensor, Exterior, and Symmetric Algebras.
+-/
+
+namespace SymmetricAlgebra
+
+/-!
+## A. Products of symmetric algebra generators
+
+Stated throughout via the public generator `SymmetricAlgebra.ι` and commutative multiplication.
+-/
+
+@[expose] public section
+
+universe u v
+
+variable (R : Type u) [CommSemiring R]
+variable (M : Type v) [AddCommMonoid M] [Module R M]
+
+/-! ### A.1. Definition -/
+
+/-- The canonical symmetric multilinear map sending a finite tuple to the product of the
+corresponding generators in the symmetric algebra. -/
+def ιMulti (n : ℕ) : SymmetricMap R M (SymmetricAlgebra R M) (Fin n) :=
+  (mkPiAlgebra R (Fin n) (SymmetricAlgebra R M)).compLinearMap (ι R M)
+
+/-! ### A.2. Computation lemmas -/
+
+/-- Applying `ιMulti` to a tuple gives the product of the corresponding symmetric-algebra
+generators. -/
+lemma ιMulti_apply {n : ℕ} (v : Fin n → M) :
+    ιMulti R M n v = ∏ i, ι R M (v i) :=
+  rfl
+
+/-- The degree-zero symmetric monomial is the multiplicative identity. -/
+@[simp]
+lemma ιMulti_zero_apply (v : Fin 0 → M) : ιMulti R M 0 v = 1 := by
+  rw [ιMulti_apply]
+  exact Fin.prod_univ_zero _
+
+/-- A positive-degree symmetric monomial is its first generator multiplied by the product of the
+remaining generators. -/
+@[simp]
+lemma ιMulti_succ_apply {n : ℕ} (v : Fin n.succ → M) :
+    ιMulti R M n.succ v = ι R M (v 0) * ιMulti R M n (Matrix.vecTail v) := by
+  rw [ιMulti_apply, Fin.prod_univ_succ, ιMulti_apply]
+  rfl
+
+end
+
+/-!
+## B. The lift out of the symmetric algebra
+
+A degreewise family of symmetric multilinear maps is assembled into a single linear map on the
+symmetric algebra, along the pipeline
+
+    ∀ n, SymmetricMap R M N (Fin n)
+      → ∀ n, (n-fold tensor power of M) →ₗ[R] N      (PiTensorProduct.lift)
+      → (⨁ n, n-fold tensor power of M) →ₗ[R] N      (DirectSum.toModule)
+      → TensorAlgebra R M →ₗ[R] N                    (TensorAlgebra.equivDirectSum)
+      → SymmetricAlgebra R M →ₗ[R] N                 (the descent)
+
+The first three steps are assembled as the internal `Lhat`; the last is carried out by the internal
+`descend`, once `Lhat` is shown constant on the symmetric congruence.
+-/
+
+public section
+
+universe u v w w'
+
+/-!
+### B.1. A pure `Fin`-coordinate lemma
+-/
+
+section FinCoordinates
+
+variable {M : Type v}
+
+/-- Swapping the two middle entries of `Fin.append (Fin.append s ![x, y]) t` is exactly the adjacent
+transposition of positions `m` and `m + 1`. -/
+private lemma append_pair_swap (x y : M) (m k : ℕ) (s : Fin m → M) (t : Fin k → M) :
+    Fin.append (Fin.append s ![y, x]) t
+      = fun i => Fin.append (Fin.append s ![x, y]) t
+          (Equiv.swap (Fin.castAdd k (Fin.natAdd m (0 : Fin 2)))
+            (Fin.castAdd k (Fin.natAdd m (1 : Fin 2))) i) := by
+  set U : Fin (m + 2 + k) → M := Fin.append (Fin.append s ![x, y]) t with hU
+  set V : Fin (m + 2 + k) → M := Fin.append (Fin.append s ![y, x]) t with hV
+  set a₀ : Fin (m + 2 + k) := Fin.castAdd k (Fin.natAdd m (0 : Fin 2)) with ha₀
+  set b₀ : Fin (m + 2 + k) := Fin.castAdd k (Fin.natAdd m (1 : Fin 2)) with hb₀
+  set e : Equiv.Perm (Fin (m + 2 + k)) := Equiv.swap a₀ b₀ with he
+  show V = fun i => U (e i)
+  funext i
+  refine Fin.addCases (fun j => ?_) (fun l => ?_) i
+  · refine Fin.addCases (fun p => ?_) (fun q => ?_) j
+    · have hne1 : (Fin.castAdd k (Fin.castAdd 2 p)) ≠ a₀ := by
+        rw [ha₀]; simp [Fin.ext_iff]; omega
+      have hne2 : (Fin.castAdd k (Fin.castAdd 2 p)) ≠ b₀ := by
+        rw [hb₀]; simp [Fin.ext_iff]; omega
+      simp only [hU, hV, he, Equiv.swap_apply_of_ne_of_ne hne1 hne2, Fin.append_left]
+    · by_cases hq0 : q = 0
+      · subst hq0
+        have hsw : e (Fin.castAdd k (Fin.natAdd m (0 : Fin 2)))
+            = Fin.castAdd k (Fin.natAdd m (1 : Fin 2)) := by
+          rw [he, ← ha₀, Equiv.swap_apply_left, ← hb₀]
+        rw [hsw]
+        simp [hU, hV, Fin.append_left, Fin.append_right]
+      · have hq1 : q = 1 := by omega
+        subst hq1
+        have hsw : e (Fin.castAdd k (Fin.natAdd m (1 : Fin 2)))
+            = Fin.castAdd k (Fin.natAdd m (0 : Fin 2)) := by
+          rw [he, ← hb₀, Equiv.swap_apply_right, ← ha₀]
+        rw [hsw]
+        simp [hU, hV, Fin.append_left, Fin.append_right]
+  · have hne1 : (Fin.natAdd (m + 2) l) ≠ a₀ := by
+      rw [ha₀]; simp [Fin.ext_iff]; omega
+    have hne2 : (Fin.natAdd (m + 2) l) ≠ b₀ := by
+      rw [hb₀]; simp [Fin.ext_iff]; omega
+    simp only [hU, hV, he, Equiv.swap_apply_of_ne_of_ne hne1 hne2, Fin.append_right]
+
+end FinCoordinates
+
+variable {R : Type u} [CommSemiring R]
+variable {M : Type v} [AddCommMonoid M] [Module R M]
+variable {N : Type w} [AddCommMonoid N] [Module R N]
+
+open TensorAlgebra
+open scoped DirectSum TensorProduct Pointwise
+
+/-!
+### B.2. Internal helpers (family-independent)
+
+The parts of the construction not mentioning the degreewise family: the quotient descent, the
+identification of a symmetric monomial with the image of a tensor-algebra monomial, and the two
+facts about tensor-algebra monomials - they multiply by concatenation, and they span.
+
+The carrier of `SymmetricAlgebra R M` is definitionally the quotient of the additive congruence
+underlying `symRingCon`, so the `AddCon.lift` in `descend` lands in it directly, with no transport.
+-/
+
+/-- A linear map out of the tensor algebra that is constant on the symmetric congruence descends to
+the symmetric algebra. Module-target analogue of `SymmetricAlgebra.lift`. -/
+private noncomputable def descend
+    (L : TensorAlgebra R M →ₗ[R] N)
+    (h : ∀ x y, symRingCon R M x y → L x = L y) :
+    SymmetricAlgebra R M →ₗ[R] N where
+  toFun := (symRingCon R M).toAddCon.lift L.toAddMonoidHom (fun ⦃x y⦄ hxy => h x y hxy)
+  map_add' := map_add _
+  map_smul' := fun r x => by
+    obtain ⟨a, rfl⟩ := SymmetricAlgebra.algHom_surjective R M x
+    rw [RingHom.id_apply, ← map_smul (SymmetricAlgebra.algHom R M) r a]
+    exact map_smul L r a
+
+/-- The descended map computes on the image of a tensor-algebra element by evaluating the original
+map there. -/
+@[simp]
+private lemma descend_algHom
+    (L : TensorAlgebra R M →ₗ[R] N)
+    (h : ∀ x y, symRingCon R M x y → L x = L y)
+    (a : TensorAlgebra R M) :
+    descend L h (SymmetricAlgebra.algHom R M a) = L a :=
+  rfl
+
+/-- The symmetric monomial `ιMulti` is the `algHom`-image of the tensor-algebra monomial `tprod`. -/
+private lemma ιMulti_eq_algHom_tprod (n : ℕ) (v : Fin n → M) :
+    ιMulti R M n v = SymmetricAlgebra.algHom R M (TensorAlgebra.tprod R M n v) := by
+  rw [ιMulti_apply, TensorAlgebra.tprod_apply, map_list_prod, List.map_ofFn]
+  simp [SymmetricAlgebra.ι, List.prod_ofFn]
+
+/-- A degree-2 tensor-algebra monomial is the product of its two generators. -/
+private lemma tprod_two (x y : M) :
+    TensorAlgebra.tprod R M 2 ![x, y] = TensorAlgebra.ι R x * TensorAlgebra.ι R y := by
+  rw [TensorAlgebra.tprod_apply]
+  simp [List.ofFn_succ]
+
+/-- Concatenation of tensor-algebra monomials. -/
+private lemma tprod_mul (m k : ℕ) (s : Fin m → M) (t : Fin k → M) :
+    TensorAlgebra.tprod R M m s * TensorAlgebra.tprod R M k t
+      = TensorAlgebra.tprod R M (m + k) (Fin.append s t) := by
+  have hfun : (fun i => TensorAlgebra.ι R (Fin.append s t i))
+      = Fin.append (fun i => TensorAlgebra.ι R (s i)) (fun i => TensorAlgebra.ι R (t i)) := by
+    funext i
+    refine Fin.addCases ?_ ?_ i <;> intro j <;> simp
+  rw [TensorAlgebra.tprod_apply, TensorAlgebra.tprod_apply, TensorAlgebra.tprod_apply,
+    ← List.prod_append, ← List.ofFn_fin_append, hfun]
+
+/-- The tensor-algebra monomials span the whole tensor algebra as a module. -/
+private lemma tprod_span :
+    Submodule.span R
+      (Set.range (fun p : (n : ℕ) × (Fin n → M) => TensorAlgebra.tprod R M p.1 p.2)) = ⊤ := by
+  set S : Set (TensorAlgebra R M) :=
+    Set.range (fun p : (n : ℕ) × (Fin n → M) => TensorAlgebra.tprod R M p.1 p.2)
+  have hSmul : S * S ⊆ S := by
+    rintro _ ⟨_, ⟨⟨m, s⟩, rfl⟩, _, ⟨⟨k, t⟩, rfl⟩, rfl⟩
+    exact ⟨⟨m + k, Fin.append s t⟩, (tprod_mul m k s t).symm⟩
+  rw [eq_top_iff]
+  intro z hz
+  clear hz
+  induction z using TensorAlgebra.induction with
+  | algebraMap r =>
+      rw [Algebra.algebraMap_eq_smul_one]
+      exact Submodule.smul_mem _ _
+        (Submodule.subset_span ⟨⟨0, ![]⟩, by simp [TensorAlgebra.tprod_apply]⟩)
+  | ι v =>
+      exact Submodule.subset_span ⟨⟨1, ![v]⟩, by simp [TensorAlgebra.tprod_apply, List.ofFn_succ]⟩
+  | mul u w hu hw =>
+      have h := Submodule.mul_mem_mul hu hw
+      rw [Submodule.span_mul_span] at h
+      exact Submodule.span_mono hSmul h
+  | add u w hu hw => exact Submodule.add_mem _ hu hw
+
+/-!
+### B.3. Internal helpers (family-dependent)
+
+`Lhat` evaluates the degreewise family on tensor words. Symmetry of the family gives permutation
+invariance on monomials, and a span argument extends the generator swap to arbitrary surrounding
+factors `a * _ * b`. Passing to `Qcon`, the largest ring congruence on which `Lhat` is constant,
+then turns that invariance into compatibility with `symRingCon`.
+-/
+
+section Construction
+
+variable (f : ∀ n, SymmetricMap R M N (Fin n))
+
+/-- The linear map on the tensor algebra assembled from the degreewise symmetric maps. -/
+private noncomputable def Lhat : TensorAlgebra R M →ₗ[R] N :=
+  DirectSum.toModule R ℕ N (fun n => PiTensorProduct.lift (f n).toMultilinearMap) ∘ₗ
+    (TensorAlgebra.equivDirectSum (R := R) (M := M)).toLinearMap
+
+/-- `Lhat` sends a tensor-algebra monomial to the value prescribed by the rule of its degree. -/
+@[simp]
+private lemma Lhat_tprod (n : ℕ) (v : Fin n → M) :
+    Lhat f (TensorAlgebra.tprod R M n v) = f n v := by
+  rw [Lhat, LinearMap.comp_apply, AlgEquiv.toLinearMap_apply,
+    TensorAlgebra.equivDirectSum_apply, TensorAlgebra.toDirectSum_tensorPower_tprod,
+    ← DirectSum.lof_eq_of R, DirectSum.toModule_lof, PiTensorProduct.lift.tprod]
+  rfl
+
+/-- Permuting the factors of a tensor-algebra monomial leaves `Lhat` unchanged, because each `f n`
+is symmetric. -/
+private lemma Lhat_tprod_perm (n : ℕ) (v : Fin n → M) (e : Equiv.Perm (Fin n)) :
+    Lhat f (TensorAlgebra.tprod R M n (fun i => v (e i)))
+      = Lhat f (TensorAlgebra.tprod R M n v) := by
+  rw [Lhat_tprod, Lhat_tprod]
+  exact (f n).map_perm e v
+
+/-- The largest ring congruence on which `Lhat f` is constant: it relates `u` and `w` when
+`Lhat f (a * u * b) = Lhat f (a * w * b)` for all `a` and `b`. -/
+private def Qcon : RingCon (TensorAlgebra R M) where
+  r u w := ∀ a b, Lhat f (a * u * b) = Lhat f (a * w * b)
+  iseqv :=
+    { refl := fun _ _ _ => rfl
+      symm := fun h a b => (h a b).symm
+      trans := fun h1 h2 a b => (h1 a b).trans (h2 a b) }
+  add' := fun h1 h2 a b => by
+    simp only [mul_add, add_mul, map_add]; rw [h1 a b, h2 a b]
+  mul' := fun {w x y z} h1 h2 a b => by
+    have k1 := h1 a (y * b)
+    have k2 := h2 (a * x) b
+    simp only [← mul_assoc] at k1 k2 ⊢
+    rw [k1]; exact k2
+
+/-- The generator swap with monomials as the surrounding factors: the three factors fold into one
+`tprod`, and the swap becomes the transposition of two adjacent positions. -/
+private lemma Lhat_contextSwap_monomial (x y : M) (m k : ℕ) (s : Fin m → M) (t : Fin k → M) :
+    Lhat f (TensorAlgebra.tprod R M m s * (TensorAlgebra.ι R x * TensorAlgebra.ι R y)
+        * TensorAlgebra.tprod R M k t)
+      = Lhat f (TensorAlgebra.tprod R M m s * (TensorAlgebra.ι R y * TensorAlgebra.ι R x)
+        * TensorAlgebra.tprod R M k t) := by
+  rw [← tprod_two, ← tprod_two, tprod_mul, tprod_mul, tprod_mul, tprod_mul,
+    append_pair_swap x y m k s t]
+  exact (Lhat_tprod_perm f (m + 2 + k) (Fin.append (Fin.append s ![x, y]) t) _).symm
+
+/-- The generator swap with arbitrary factors `a` and `b` on either side, obtained from
+`Lhat_contextSwap_monomial` by induction over the spanning set of monomials in `a` and `b` at
+once. -/
+private lemma Lhat_contextSwap (x y : M) (a b : TensorAlgebra R M) :
+    Lhat f (a * (TensorAlgebra.ι R x * TensorAlgebra.ι R y) * b)
+      = Lhat f (a * (TensorAlgebra.ι R y * TensorAlgebra.ι R x) * b) := by
+  classical
+  have hspan : Submodule.span R
+      (Set.range (fun p : (n : ℕ) × (Fin n → M) => TensorAlgebra.tprod R M p.1 p.2)) = ⊤ :=
+    tprod_span
+  refine Submodule.span_induction₂
+    (p := fun a b _ _ => Lhat f (a * (TensorAlgebra.ι R x * TensorAlgebra.ι R y) * b)
+      = Lhat f (a * (TensorAlgebra.ι R y * TensorAlgebra.ι R x) * b))
+    ?_ ?_ ?_ ?_ ?_ ?_ ?_ (hspan ▸ Submodule.mem_top) (hspan ▸ Submodule.mem_top)
+  · rintro _ _ ⟨⟨m, s⟩, rfl⟩ ⟨⟨k, t⟩, rfl⟩
+    exact Lhat_contextSwap_monomial f x y m k s t
+  · intro c _; simp
+  · intro c _; simp
+  · intro c d g _ _ _ hc hd; simp only [add_mul, map_add, hc, hd]
+  · intro c d g _ _ _ hd hg; simp only [mul_add, map_add, hd, hg]
+  · intro r c d _ _ hc; simp only [smul_mul_assoc, map_smul, hc]
+  · intro r c d _ _ hd; simp only [mul_smul_comm, map_smul, hd]
+
+/-- `Lhat f` is constant on the whole symmetric congruence, and so descends. -/
+private lemma well_defined : ∀ u w, symRingCon R M u w → Lhat f u = Lhat f w := by
+  have hle : symRingCon R M ≤ Qcon f := by
+    rw [show symRingCon R M = ringConGen (SymRel R M) from rfl]
+    refine RingCon.ringConGen_le.2 ?_
+    intro u v h
+    cases h with
+    | mul_comm x y => exact fun a b => Lhat_contextSwap f x y a b
+  intro u w h
+  simpa using hle h 1 1
+
+/-- The descended map for a fixed family; `liftSymmetric` bundles it linearly in the family. -/
+private noncomputable def liftSymmetricAux : SymmetricAlgebra R M →ₗ[R] N :=
+  descend (Lhat f) (well_defined f)
+
+/-- For a fixed family, the descended map sends a symmetric monomial to the prescribed degreewise
+value. -/
+private lemma liftSymmetricAux_ιMulti (n : ℕ) (v : Fin n → M) :
+    liftSymmetricAux f (ιMulti R M n v) = f n v := by
+  rw [liftSymmetricAux, ιMulti_eq_algHom_tprod, descend_algHom, Lhat_tprod]
+
+end Construction
+
+/-!
+### B.4. Extensionality
+
+Since `algHom` is surjective and the tensor-algebra monomials span, a linear map out of the
+symmetric algebra is determined by its values on symmetric monomials.
+-/
+
+/-- Two linear maps out of the symmetric algebra agreeing on every symmetric monomial are equal. -/
+@[ext]
+lemma lhom_ext ⦃g h : SymmetricAlgebra R M →ₗ[R] N⦄
+    (H : ∀ (n : ℕ) (v : Fin n → M), g (ιMulti R M n v) = h (ιMulti R M n v)) :
+    g = h := by
+  have key : g.comp (SymmetricAlgebra.algHom R M).toLinearMap
+      = h.comp (SymmetricAlgebra.algHom R M).toLinearMap := by
+    refine LinearMap.ext_on_range tprod_span ?_
+    rintro ⟨n, v⟩
+    simp only [LinearMap.comp_apply, AlgHom.toLinearMap_apply, ← ιMulti_eq_algHom_tprod]
+    exact H n v
+  ext x
+  obtain ⟨a, rfl⟩ := SymmetricAlgebra.algHom_surjective R M x
+  simpa using LinearMap.congr_fun key a
+
+/-!
+### B.5. The bundled lift and its API
+
+`liftSymmetric` bundles the construction of section B.3 as a map linear in the degreewise family;
+both linearity obligations reduce through `lhom_ext` to the computation on monomials. The remaining
+results are the computation rule, the two composition laws, the identity case
+`liftSymmetric_ιMulti`, and the packaging as a linear equivalence.
+-/
+
+/-- Assemble a degreewise family of symmetric multilinear maps into a linear map on the symmetric
+algebra, linearly in the family. -/
+noncomputable def liftSymmetric :
+    (∀ n, SymmetricMap R M N (Fin n)) →ₗ[R] SymmetricAlgebra R M →ₗ[R] N where
+  toFun f := liftSymmetricAux f
+  map_add' f g := by
+    refine lhom_ext fun n v => ?_
+    simp only [liftSymmetricAux_ιMulti, LinearMap.add_apply, Pi.add_apply, SymmetricMap.add_coe]
+  map_smul' c f := by
+    refine lhom_ext fun n v => ?_
+    simp only [liftSymmetricAux_ιMulti, RingHom.id_apply, LinearMap.smul_apply, Pi.smul_apply,
+      SymmetricMap.smul_coe]
+
+/-- `liftSymmetric` sends a symmetric monomial to the prescribed degreewise value. -/
+@[simp]
+lemma liftSymmetric_apply_ιMulti (f : ∀ n, SymmetricMap R M N (Fin n))
+    {n : ℕ} (v : Fin n → M) :
+    liftSymmetric f (ιMulti R M n v) = f n v :=
+  liftSymmetricAux_ιMulti f n v
+
+/-- Postcomposing `ιMulti` with the lift recovers the original degreewise map. -/
+@[simp]
+lemma liftSymmetric_comp_ιMulti (f : ∀ n, SymmetricMap R M N (Fin n)) (n : ℕ) :
+    (liftSymmetric f).compSymmetricMap (ιMulti R M n) = f n := by
+  ext v
+  rw [LinearMap.compSymmetricMap_apply, liftSymmetric_apply_ιMulti]
+
+/-- Lifting the canonical family of symmetric monomials yields the identity. -/
+@[simp]
+lemma liftSymmetric_ιMulti :
+    liftSymmetric (ιMulti R M)
+      = (LinearMap.id : SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M) := by
+  refine lhom_ext fun n v => ?_
+  simp only [liftSymmetric_apply_ιMulti, LinearMap.id_coe, id_eq]
+
+variable {N' : Type w'} [AddCommMonoid N'] [Module R N']
+
+/-- Naturality: the lift of a postcomposed family is the postcomposition of the lift. -/
+@[simp]
+lemma liftSymmetric_comp (g : N →ₗ[R] N') (f : ∀ n, SymmetricMap R M N (Fin n)) :
+    liftSymmetric (fun n => g.compSymmetricMap (f n)) = g ∘ₗ liftSymmetric f := by
+  refine lhom_ext fun n v => ?_
+  simp only [LinearMap.comp_apply, liftSymmetric_apply_ιMulti, LinearMap.compSymmetricMap_apply]
+
+/-- `liftSymmetric` as a linear equivalence between degreewise symmetric families and linear maps
+out of the symmetric algebra. -/
+noncomputable def liftSymmetricEquiv :
+    (∀ n, SymmetricMap R M N (Fin n)) ≃ₗ[R] (SymmetricAlgebra R M →ₗ[R] N) :=
+  { liftSymmetric with
+    invFun := fun F n => F.compSymmetricMap (ιMulti R M n)
+    left_inv := fun f => by
+      funext n
+      exact liftSymmetric_comp_ιMulti f n
+    right_inv := fun F => by
+      refine lhom_ext fun n v => ?_
+      show liftSymmetric (fun n => F.compSymmetricMap (ιMulti R M n)) (ιMulti R M n v)
+        = F (ιMulti R M n v)
+      simp only [liftSymmetric_apply_ιMulti, LinearMap.compSymmetricMap_apply] }
+
+end
+
+end SymmetricAlgebra
diff --git a/Physlib/Mathematics/SymmetricAlgebra/SymmetricMap.lean b/Physlib/Mathematics/SymmetricAlgebra/SymmetricMap.lean
new file mode 100644
index 000000000..689ef3f6e
--- /dev/null
+++ b/Physlib/Mathematics/SymmetricAlgebra/SymmetricMap.lean
@@ -0,0 +1,229 @@
+/-
+Copyright (c) 2026 Nathaneal Sajan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nathaneal Sajan
+-/
+module
+
+public import Mathlib.LinearAlgebra.Multilinear.Basic
+
+/-!
+# Symmetric multilinear maps
+
+This module provides a temporary compatibility layer for symmetric multilinear maps.
+
+The declarations follow the root-level names selected in Mathlib PR #41426. This module should be
+removed in favor of the Mathlib implementation once that API is available upstream.
+
+## Main definitions
+
+* `SymmetricMap` is a multilinear map invariant under permutations of its arguments.
+* `SymmetricMap.compLinearMap` precomposes every argument with a linear map.
+* `LinearMap.compSymmetricMap` postcomposes with a linear map.
+* `mkPiAlgebra` is the symmetric multilinear product map into a commutative algebra.
+
+-/
+
+@[expose] public section
+
+universe u u' u₁ v w w'
+
+/-!
+
+## A. Symmetric multilinear maps
+
+-/
+
+/-- A symmetric `R`-multilinear map from `ι → M` to `N` is a multilinear map whose value is
+unchanged by permutations of its arguments. -/
+structure SymmetricMap
+    (R : Type u) (M : Type v) (N : Type w) (ι : Type u')
+    [Semiring R]
+    [AddCommMonoid M] [Module R M]
+    [AddCommMonoid N] [Module R N]
+    extends MultilinearMap R (fun _ : ι => M) N where
+  /-- Permuting the arguments does not change the value of the map. -/
+  map_perm' (v : ι → M) (e : Equiv.Perm ι) :
+    toFun (fun i => v (e i)) = toFun v
+
+namespace SymmetricMap
+
+variable {R : Type u} [Semiring R]
+variable {M : Type v} [AddCommMonoid M] [Module R M]
+variable {N : Type w} [AddCommMonoid N] [Module R N]
+variable {P : Type w'} [AddCommMonoid P] [Module R P]
+variable {ι : Type u'}
+
+/-!
+
+### A.1. Coercions and extensionality
+
+-/
+
+instance : FunLike (SymmetricMap R M N ι) (ι → M) N where
+  coe f := f.toFun
+  coe_injective f g h := by
+    rcases f with ⟨⟨_, _, _⟩, _⟩
+    rcases g with ⟨⟨_, _, _⟩, _⟩
+    congr
+
+lemma coe_injective :
+    Function.Injective ((↑) : SymmetricMap R M N ι → (ι → M) → N) :=
+  DFunLike.coe_injective
+
+/-- Two symmetric multilinear maps are equal when they agree on every input. -/
+@[ext]
+lemma ext {f g : SymmetricMap R M N ι} (h : ∀ v, f v = g v) : f = g :=
+  DFunLike.ext f g h
+
+attribute [coe] SymmetricMap.toMultilinearMap
+
+instance : Coe (SymmetricMap R M N ι) (MultilinearMap R (fun _ : ι => M) N) :=
+  ⟨fun f => f.toMultilinearMap⟩
+
+@[simp, norm_cast]
+lemma coe_coe (f : SymmetricMap R M N ι) :
+    ⇑(f : MultilinearMap R (fun _ : ι => M) N) = f :=
+  rfl
+
+/-- Permuting the arguments of a symmetric multilinear map does not change its value. -/
+@[simp]
+lemma map_perm (f : SymmetricMap R M N ι) (e : Equiv.Perm ι) (v : ι → M) :
+    f (fun i => v (e i)) = f v :=
+  f.map_perm' v e
+
+/-!
+
+### A.2. Additive and module structure
+
+-/
+
+instance : Add (SymmetricMap R M N ι) where
+  add f g := ⟨f.1 + g.1, fun _ _ => by simp⟩
+
+@[simp]
+lemma add_coe (f g : SymmetricMap R M N ι) : ⇑(f + g) = f + g :=
+  rfl
+
+@[simp, norm_cast]
+lemma toMultilinearMap_add (f g : SymmetricMap R M N ι) :
+    (f + g).toMultilinearMap = f.toMultilinearMap + g.toMultilinearMap :=
+  rfl
+
+instance : Zero (SymmetricMap R M N ι) where
+  zero := ⟨0, fun _ _ => rfl⟩
+
+@[simp]
+lemma zero_coe : ⇑(0 : SymmetricMap R M N ι) = 0 :=
+  rfl
+
+@[simp, norm_cast]
+lemma toMultilinearMap_zero :
+    (0 : SymmetricMap R M N ι).toMultilinearMap = 0 :=
+  rfl
+
+section ScalarAction
+
+variable {S : Type u₁} [Monoid S]
+variable [DistribMulAction S N] [SMulCommClass R S N]
+
+instance : SMul S (SymmetricMap R M N ι) where
+  smul c f := ⟨c • f.1, fun _ _ => by simp⟩
+
+@[simp]
+lemma smul_coe (c : S) (f : SymmetricMap R M N ι) : ⇑(c • f) = c • ⇑f :=
+  rfl
+
+@[simp, norm_cast]
+lemma toMultilinearMap_smul (c : S) (f : SymmetricMap R M N ι) :
+    (c • f).toMultilinearMap = c • f.toMultilinearMap :=
+  rfl
+
+end ScalarAction
+
+instance : AddCommMonoid (SymmetricMap R M N ι) := fast_instance%
+  coe_injective.addCommMonoid _ rfl (fun _ _ => rfl) fun _ _ => smul_coe _ _
+
+section DistribMulAction
+
+variable {S : Type u₁} [Monoid S]
+variable [DistribMulAction S N] [SMulCommClass R S N]
+
+instance : DistribMulAction S (SymmetricMap R M N ι) where
+  one_smul _ := ext fun _ => one_smul S _
+  mul_smul c d _ := ext fun _ => mul_smul c d _
+  smul_zero c := ext fun _ => smul_zero c
+  smul_add c _ _ := ext fun _ => smul_add c _ _
+
+end DistribMulAction
+
+section Module
+
+variable {S : Type u₁} [Semiring S]
+variable [Module S N] [SMulCommClass R S N]
+
+instance : Module S (SymmetricMap R M N ι) where
+  add_smul c d _ := ext fun _ => add_smul c d _
+  zero_smul _ := ext fun _ => zero_smul S _
+
+end Module
+
+/-!
+
+### A.3. Composition
+
+-/
+
+/-- Precompose every argument of a symmetric multilinear map with the same linear map. -/
+def compLinearMap (f : SymmetricMap R N P ι) (g : M →ₗ[R] N) : SymmetricMap R M P ι :=
+  ⟨f.1.compLinearMap fun _ => g, fun v e => f.map_perm e (g ∘ v)⟩
+
+@[simp]
+lemma compLinearMap_apply (f : SymmetricMap R N P ι) (g : M →ₗ[R] N) (v : ι → M) :
+    f.compLinearMap g v = f (g ∘ v) :=
+  rfl
+
+end SymmetricMap
+
+namespace LinearMap
+
+variable {R : Type u} [Semiring R]
+variable {M : Type v} [AddCommMonoid M] [Module R M]
+variable {N : Type w} [AddCommMonoid N] [Module R N]
+variable {P : Type w'} [AddCommMonoid P] [Module R P]
+variable {ι : Type u'}
+
+/-- Postcompose a symmetric multilinear map with a linear map. -/
+def compSymmetricMap (f : N →ₗ[R] P) (g : SymmetricMap R M N ι) : SymmetricMap R M P ι :=
+  ⟨f.compMultilinearMap g, fun v e => f.congr_arg (g.map_perm e v)⟩
+
+@[simp]
+lemma compSymmetricMap_apply (f : N →ₗ[R] P) (g : SymmetricMap R M N ι) (v : ι → M) :
+    f.compSymmetricMap g v = f (g v) :=
+  rfl
+
+end LinearMap
+
+/-!
+
+### A.4. Products in commutative algebras
+
+-/
+
+section Product
+
+variable (R : Type u) [CommSemiring R]
+variable (ι : Type u')
+variable (A : Type w) [CommSemiring A] [Algebra R A]
+
+/-- The symmetric multilinear map into a commutative algebra that sends a finite family to the
+product of its entries. -/
+def mkPiAlgebra [Fintype ι] : SymmetricMap R A A ι :=
+  ⟨MultilinearMap.mkPiAlgebra R ι A, fun v e => Equiv.prod_comp e v⟩
+
+@[simp]
+lemma mkPiAlgebra_apply [Fintype ι] (v : ι → A) :
+    mkPiAlgebra R ι A v = ∏ i, v i :=
+  rfl
+
+end Product
diff --git a/Physlib/Particles/StandardModel/HiggsBoson/EFTLagrangianExclDeriv.lean b/Physlib/Particles/StandardModel/HiggsBoson/EFTLagrangianExclDeriv.lean
new file mode 100644
index 000000000..0f93c3092
--- /dev/null
+++ b/Physlib/Particles/StandardModel/HiggsBoson/EFTLagrangianExclDeriv.lean
@@ -0,0 +1,432 @@
+/-
+Copyright (c) 2026 Nathaneal Sajan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nathaneal Sajan
+-/
+module
+
+public import Mathlib.LinearAlgebra.Basis.Prod
+public import Mathlib.LinearAlgebra.Dual.Basis
+public import Physlib.Mathematics.ConjModule
+public import Physlib.Mathematics.SymmetricAlgebra.OfSymmetric
+public import Physlib.Particles.StandardModel.HiggsBoson.Basic
+
+/-!
+# The non-derivative Higgs EFT Lagrangian space
+
+## i. Overview
+
+A Higgs effective Lagrangian, with derivative terms excluded, is a sum of products of the
+components of the Higgs doublet and of its conjugate. Selecting a component is applying a linear
+functional, so each factor in such a product is drawn from `Module.Dual ℂ HiggsVec` or from
+`Module.Dual ℂ (ConjModule HiggsVec)`. Since the Higgs is a boson these factors commute among
+themselves, which makes the free commutative algebra on that pair of duals the natural home for
+the whole Lagrangian. That algebra,
+
+`SymmetricAlgebra ℂ (Module.Dual ℂ HiggsVec × Module.Dual ℂ (ConjModule HiggsVec))`,
+
+is defined here as `EFTLagrangianExclDeriv`.
+
+Each product of generators is recorded by its field content, the multiset of component labels it
+uses. The main construction of the file is `coeff s`, the linear map keeping only the part of a
+Lagrangian with field content `s`. We show it is idempotent, so it is a projection, and that
+everything it produces is a multiple of a single monomial, so it projects onto a line.
+-/
+
+@[expose] public section
+
+namespace StandardModel.HiggsField
+
+noncomputable section
+
+open Module
+
+/-!
+
+## A. The Higgs EFT Lagrangian space
+
+-/
+
+/-! ### A.1. The carrier -/
+
+/-- The type corresponding to a non-derivative term of the Higgs effective Lagrangian: the
+symmetric algebra on the Higgs covectors and conjugate-Higgs covectors. -/
+abbrev EFTLagrangianExclDeriv : Type :=
+  SymmetricAlgebra ℂ (Module.Dual ℂ HiggsVec × Module.Dual ℂ (ConjModule HiggsVec))
+
+/-! ### A.2. The field specification -/
+
+/-- The specification of the field components appearing in a non-derivative Higgs term: the two
+components `φ α` of the Higgs doublet and the two components `barφ α` of its conjugate. -/
+inductive FieldSpecification
+  | φ (α : Fin 2)
+  | barφ (α : Fin 2)
+deriving DecidableEq, Fintype, Repr
+
+namespace FieldSpecification
+
+/-- The equivalence between `FieldSpecification` and `Fin 2 ⊕ Fin 2` sending `φ α` to the left
+and `barφ α` to the right component. -/
+def toSumFin : FieldSpecification ≃ Fin 2 ⊕ Fin 2 where
+  toFun
+    | .φ α => Sum.inl α
+    | .barφ α => Sum.inr α
+  invFun
+    | Sum.inl α => .φ α
+    | Sum.inr α => .barφ α
+  left_inv x := by cases x <;> rfl
+  right_inv x := by cases x <;> rfl
+
+/-! ### A.3. The generator basis -/
+
+/-- The basis of the module underlying `EFTLagrangianExclDeriv`, indexed by `FieldSpecification`:
+`φ α` corresponds to the dual basis of the Higgs doublet and `barφ α` to the dual basis of its
+conjugate. -/
+def moduleBasis : Basis FieldSpecification ℂ
+    (Module.Dual ℂ HiggsVec × Module.Dual ℂ (ConjModule HiggsVec)) :=
+  (HiggsVec.orthonormBasis.toBasis.dualBasis.prod
+    (Basis.conj HiggsVec.orthonormBasis.toBasis).dualBasis).reindex toSumFin.symm
+
+@[simp]
+lemma moduleBasis_apply_φ (α : Fin 2) :
+    moduleBasis (.φ α) = (HiggsVec.orthonormBasis.toBasis.dualBasis α, 0) := by
+  simp [moduleBasis, toSumFin]
+
+@[simp]
+lemma moduleBasis_apply_barφ (α : Fin 2) :
+    moduleBasis (.barφ α) =
+      (0, (Basis.conj HiggsVec.orthonormBasis.toBasis).dualBasis α) := by
+  simp [moduleBasis, toSumFin]
+
+/-! ### A.4. Algebra generators -/
+
+/-- The image of a field specification in `EFTLagrangianExclDeriv`, as the symmetric-algebra
+generator of the corresponding basis vector. Denoted `[f]ₛ`. -/
+def toEFTLagrangianExclDeriv (f : FieldSpecification) : EFTLagrangianExclDeriv :=
+  SymmetricAlgebra.ι ℂ
+    (Module.Dual ℂ HiggsVec × Module.Dual ℂ (ConjModule HiggsVec)) (moduleBasis f)
+
+@[inherit_doc toEFTLagrangianExclDeriv]
+scoped notation "[" f "]ₛ" => toEFTLagrangianExclDeriv f
+
+lemma toEFTLagrangianExclDeriv_φ (α : Fin 2) :
+    [φ α]ₛ = SymmetricAlgebra.ι ℂ
+      (Module.Dual ℂ HiggsVec × Module.Dual ℂ (ConjModule HiggsVec))
+      (HiggsVec.orthonormBasis.toBasis.dualBasis α, 0) := by
+  rw [toEFTLagrangianExclDeriv, moduleBasis_apply_φ]
+
+lemma toEFTLagrangianExclDeriv_barφ (α : Fin 2) :
+    [barφ α]ₛ = SymmetricAlgebra.ι ℂ
+      (Module.Dual ℂ HiggsVec × Module.Dual ℂ (ConjModule HiggsVec))
+      (0, (Basis.conj HiggsVec.orthonormBasis.toBasis).dualBasis α) := by
+  rw [toEFTLagrangianExclDeriv, moduleBasis_apply_barφ]
+
+end FieldSpecification
+
+namespace EFTLagrangianExclDeriv
+
+open FieldSpecification
+
+/-!
+
+## B. Higgs monomials
+
+-/
+
+/-! ### B.1. Monomials from a list -/
+
+/-- The term in the Higgs effective Lagrangian given by the product of the field labels in `l`. -/
+def termOfList (l : List FieldSpecification) : EFTLagrangianExclDeriv :=
+  (l.map toEFTLagrangianExclDeriv).prod
+
+@[simp]
+lemma termOfList_nil : termOfList [] = 1 := by
+  simp [termOfList]
+
+lemma termOfList_cons (f : FieldSpecification) (l : List FieldSpecification) :
+    termOfList (f :: l) = [f]ₛ * termOfList l := by
+  simp [termOfList]
+
+lemma termOfList_singleton (f : FieldSpecification) : termOfList [f] = [f]ₛ := by
+  simp [termOfList_cons]
+
+lemma termOfList_append (l₁ l₂ : List FieldSpecification) :
+    termOfList (l₁ ++ l₂) = termOfList l₁ * termOfList l₂ := by
+  simp [termOfList]
+
+/-! ### B.2. Permutation invariance -/
+
+/-- Permuting bosonic field labels leaves their monomial unchanged. -/
+lemma termOfList_eq_of_perm {l₁ l₂ : List FieldSpecification} (h : l₁.Perm l₂) :
+    termOfList l₁ = termOfList l₂ :=
+  (h.map toEFTLagrangianExclDeriv).prod_eq
+
+lemma termOfList_eq_ιMulti (l : List FieldSpecification) :
+    termOfList l = SymmetricAlgebra.ιMulti ℂ
+      (Module.Dual ℂ HiggsVec × Module.Dual ℂ (ConjModule HiggsVec)) l.length
+      (fun i => moduleBasis (l.get i)) := by
+  induction l with
+  | nil => simp
+  | cons f l h =>
+      simp [termOfList_cons, h]
+      rfl
+
+lemma termOfList_ofFn {n : ℕ} (g : Fin n → FieldSpecification) :
+    termOfList (List.ofFn g) = SymmetricAlgebra.ιMulti ℂ
+      (Module.Dual ℂ HiggsVec × Module.Dual ℂ (ConjModule HiggsVec)) n
+      (fun i => moduleBasis (g i)) := by
+  rw [SymmetricAlgebra.ιMulti_apply, termOfList, List.map_ofFn, List.prod_ofFn]
+  rfl
+
+/-! ### B.3. Monomials from a tuple -/
+
+/-- The term in the Higgs effective Lagrangian given by the product of the field labels in the
+finite tuple `g`. -/
+def termOfTuple {n : ℕ} (g : Fin n → FieldSpecification) : EFTLagrangianExclDeriv :=
+  termOfList (List.ofFn g)
+
+lemma termOfTuple_eq_ιMulti {n : ℕ} (g : Fin n → FieldSpecification) :
+    termOfTuple g = SymmetricAlgebra.ιMulti ℂ
+      (Module.Dual ℂ HiggsVec × Module.Dual ℂ (ConjModule HiggsVec)) n
+      (fun i => moduleBasis (g i)) := by
+  rw [termOfTuple, termOfList_ofFn]
+
+/-- Permuting a bosonic field tuple leaves its monomial unchanged. -/
+lemma termOfTuple_comp_perm {n : ℕ} (g : Fin n → FieldSpecification) (e : Equiv.Perm (Fin n)) :
+    termOfTuple (g ∘ e) = termOfTuple g := by
+  rw [termOfTuple_eq_ιMulti, termOfTuple_eq_ιMulti]
+  simpa [Function.comp_apply] using
+    (SymmetricAlgebra.ιMulti ℂ
+      (Module.Dual ℂ HiggsVec × Module.Dual ℂ (ConjModule HiggsVec)) n).map_perm e
+      (fun i => moduleBasis (g i))
+
+/-!
+
+## C. The field-content projection
+
+We cannot define a basis on `EFTLagrangianExclDeriv` without choosing an ordering on the field
+specification. Instead, given a multiset of field specifications, we define a linear map
+projecting onto the span of the monomials with that field content. That span is one-dimensional,
+which is the sense in which this projection plays the role of a coefficient.
+
+-/
+
+/-! ### C.1. The symmetric coordinate rule -/
+
+/-- The symmetric multilinear rule underlying `coeff s`: a tuple of vectors is sent to
+`termOfTuple g` weighted by the product of the `g`-coordinates of the vectors, summed over the
+tuples `g` of fields with field content `s`. -/
+def coeffOfVectorTuple (s : Multiset FieldSpecification) (n : ℕ) :
+    SymmetricMap ℂ (Module.Dual ℂ HiggsVec × Module.Dual ℂ (ConjModule HiggsVec))
+      EFTLagrangianExclDeriv (Fin n) where
+  toMultilinearMap :=
+    ∑ g : Fin n → FieldSpecification,
+      if Multiset.ofList (List.ofFn g) = s then
+        (LinearMap.toSpanSingleton ℂ EFTLagrangianExclDeriv (termOfTuple g)).compMultilinearMap
+          ((MultilinearMap.mkPiAlgebra ℂ (Fin n) ℂ).compLinearMap
+            fun i => moduleBasis.coord (g i))
+      else 0
+  map_perm' := by
+    intro v e
+    simp only [MultilinearMap.toFun_eq_coe, sum_apply]
+    -- Name the summand family, and the reindexing `g ↦ g ∘ e.symm` of the index set.
+    let F : (Fin n → FieldSpecification) →
+        MultilinearMap ℂ
+          (fun _ : Fin n => Module.Dual ℂ HiggsVec × Module.Dual ℂ (ConjModule HiggsVec))
+          EFTLagrangianExclDeriv :=
+      fun g =>
+        if Multiset.ofList (List.ofFn g) = s then
+          (LinearMap.toSpanSingleton ℂ EFTLagrangianExclDeriv (termOfTuple g)).compMultilinearMap
+            ((MultilinearMap.mkPiAlgebra ℂ (Fin n) ℂ).compLinearMap
+              fun i => moduleBasis.coord (g i))
+        else 0
+    let p : (Fin n → FieldSpecification) → (Fin n → FieldSpecification) :=
+      fun g => g ∘ e.symm
+    have hp : Function.Bijective p := by
+      constructor
+      · intro g h hgh
+        funext i
+        simpa [p, Function.comp_apply] using congrFun hgh (e i)
+      · intro g
+        refine ⟨g ∘ e, ?_⟩
+        funext i
+        simp [p, Function.comp_apply]
+    change (∑ g, F g (fun i => v (e i))) = ∑ g, F g v
+    calc
+      _ = ∑ g, F (p g) v := by
+        apply Finset.sum_congr rfl
+        intro g _
+        simp only [F, p]
+        -- Reindexing the tuple by a permutation preserves its field content.
+        have hms : Multiset.ofList (List.ofFn (g ∘ e.symm)) =
+            Multiset.ofList (List.ofFn g) :=
+          Multiset.coe_eq_coe.mpr (Equiv.Perm.ofFn_comp_perm e.symm g)
+        rw [hms]
+        split_ifs with h
+        · simp only [LinearMap.compMultilinearMap_apply, MultilinearMap.compLinearMap_apply,
+            MultilinearMap.mkPiAlgebra_apply, LinearMap.toSpanSingleton_apply,
+            Function.comp_apply]
+          -- The coordinate product is a finite product, so it is permutation invariant.
+          have hprod : ∏ i, moduleBasis.coord (g i) (v (e i)) =
+              ∏ i, moduleBasis.coord (g (e.symm i)) (v i) := by
+            simpa using
+              Equiv.prod_comp e (fun i => moduleBasis.coord (g (e.symm i)) (v i))
+          rw [hprod, termOfTuple_comp_perm g e.symm]
+        · simp
+      _ = _ := hp.sum_comp (fun g => F g v)
+
+/-! ### C.2. The projection and its value on monomials -/
+
+/-- The projection of a non-derivative Higgs term onto the span of the monomials with field
+content `s`. -/
+def coeff (s : Multiset FieldSpecification) :
+    EFTLagrangianExclDeriv →ₗ[ℂ] EFTLagrangianExclDeriv :=
+  SymmetricAlgebra.liftSymmetric (coeffOfVectorTuple s)
+
+/-- A monomial is preserved by the projection onto its own field content and killed by every
+other. In particular the surviving monomial appears with coefficient one, with no factorial or
+divided-power normalization, and this holds also when field labels repeat. -/
+lemma coeff_apply_termOfList (s : Multiset FieldSpecification) (l : List FieldSpecification) :
+    coeff s (termOfList l) = if Multiset.ofList l = s then termOfList l else 0 := by
+  have hterm : termOfTuple l.get = termOfList l := by
+    rw [termOfTuple, List.ofFn_get]
+  rw [coeff, termOfList_eq_ιMulti, SymmetricAlgebra.liftSymmetric_apply_ιMulti]
+  change (coeffOfVectorTuple s l.length).toMultilinearMap
+    (fun i => moduleBasis (l.get i)) = _
+  simp only [coeffOfVectorTuple, sum_apply]
+  refine (Finset.sum_eq_single l.get ?_ ?_).trans ?_
+  · intro g _ hg
+    obtain ⟨i, hi⟩ := Function.ne_iff.mp hg
+    split_ifs with h
+    · simp only [LinearMap.compMultilinearMap_apply, MultilinearMap.compLinearMap_apply,
+        MultilinearMap.mkPiAlgebra_apply, LinearMap.toSpanSingleton_apply]
+      -- Coordinate orthogonality kills every tuple other than the matching one.
+      have hzero : ∏ k, moduleBasis.coord (g k) (moduleBasis (l.get k)) = 0 :=
+        Finset.prod_eq_zero (Finset.mem_univ i) (by
+          rw [Basis.coord_apply, Basis.repr_self, Finsupp.single_eq_of_ne hi])
+      rw [hzero, zero_smul]
+    · simp
+  · intro h
+    exact absurd (Finset.mem_univ _) h
+  · rw [List.ofFn_get]
+    split_ifs with h
+    · simp only [LinearMap.compMultilinearMap_apply, MultilinearMap.compLinearMap_apply,
+        MultilinearMap.mkPiAlgebra_apply, LinearMap.toSpanSingleton_apply, hterm]
+      have hprod : ∏ i, moduleBasis.coord (l.get i) (moduleBasis (l.get i)) = 1 := by
+        simp
+      rw [hprod, one_smul]
+      exact termOfList_eq_ιMulti l
+    · simp
+
+/-!
+
+## D. Properties of the projection
+
+-/
+
+/-! ### D.1. Monomials span the space -/
+
+/-- Every element of `EFTLagrangianExclDeriv` is a linear combination of Higgs monomials. -/
+lemma mem_termOfList_span (V : EFTLagrangianExclDeriv) :
+    V ∈ Submodule.span ℂ (Set.range termOfList) := by
+  induction V using SymmetricAlgebra.induction with
+  | algebraMap r =>
+      rw [Algebra.algebraMap_eq_smul_one]
+      exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨[], termOfList_nil⟩)
+  | ι v =>
+      rw [← Basis.sum_repr moduleBasis v, map_sum]
+      refine Submodule.sum_mem _ fun f _ => ?_
+      rw [map_smul]
+      exact Submodule.smul_mem _ _
+        (Submodule.subset_span ⟨[f], by rw [termOfList_singleton]; rfl⟩)
+  | mul a b ha hb =>
+      induction ha using Submodule.span_induction with
+      | mem x hx =>
+          obtain ⟨l₁, rfl⟩ := hx
+          induction hb using Submodule.span_induction with
+          | mem y hy =>
+              obtain ⟨l₂, rfl⟩ := hy
+              exact Submodule.subset_span ⟨l₁ ++ l₂, termOfList_append l₁ l₂⟩
+          | zero => simp
+          | add y z _ _ hy hz => rw [mul_add]; exact add_mem hy hz
+          | smul c y _ hy => rw [mul_smul_comm]; exact Submodule.smul_mem _ _ hy
+      | zero => simp
+      | add x y _ _ hx hy => rw [add_mul]; exact add_mem hx hy
+      | smul c x _ hx => rw [smul_mul_assoc]; exact Submodule.smul_mem _ _ hx
+  | add a b ha hb => exact add_mem ha hb
+
+/-! ### D.2. Idempotence -/
+
+/-- `coeff s` is idempotent, and is therefore genuinely a projection on the whole algebra. -/
+@[simp]
+lemma coeff_coeff_self {s : Multiset FieldSpecification} (V : EFTLagrangianExclDeriv) :
+    coeff s (coeff s V) = coeff s V := by
+  have hV := mem_termOfList_span V
+  induction hV using Submodule.span_induction with
+  | mem W hW =>
+      obtain ⟨l, rfl⟩ := hW
+      rw [coeff_apply_termOfList]
+      split_ifs with h
+      · rw [coeff_apply_termOfList, if_pos h]
+      · rw [map_zero]
+  | zero => rw [map_zero, map_zero]
+  | add W X _ _ hW hX => rw [map_add, map_add, hW, hX]
+  | smul c W _ hW => rw [map_smul, map_smul, hW]
+
+/-! ### D.3. One-dimensionality of the image -/
+
+/-- The image of `coeff s` is the line spanned by the monomial with field content `s`: every
+projected term is a scalar multiple of a single monomial. Since permutations act without a sign,
+the choice of ordering `l` of the content is immaterial. -/
+lemma coeff_eq_termOfList {s : Multiset FieldSpecification} (V : EFTLagrangianExclDeriv)
+    {l : List FieldSpecification} (hl : Multiset.ofList l = s) :
+    ∃ c : ℂ, coeff s V = c • termOfList l := by
+  have hV := mem_termOfList_span V
+  induction hV using Submodule.span_induction with
+  | mem W hW =>
+      obtain ⟨l', rfl⟩ := hW
+      rw [coeff_apply_termOfList]
+      split_ifs with h
+      · refine ⟨1, ?_⟩
+        rw [one_smul]
+        exact termOfList_eq_of_perm (Multiset.coe_eq_coe.mp (h.trans hl.symm))
+      · exact ⟨0, by rw [zero_smul]⟩
+  | zero => exact ⟨0, by rw [map_zero, zero_smul]⟩
+  | add W X _ _ hW hX =>
+      obtain ⟨c₁, hc₁⟩ := hW
+      obtain ⟨c₂, hc₂⟩ := hX
+      exact ⟨c₁ + c₂, by rw [map_add, hc₁, hc₂, add_smul]⟩
+  | smul a W _ hW =>
+      obtain ⟨c, hc⟩ := hW
+      exact ⟨a * c, by rw [map_smul, hc, smul_smul]⟩
+
+/-!
+
+## E. The Higgs norm-squared term
+
+-/
+
+/-- The formal Higgs norm-squared term, the component sum of a conjugate-Higgs generator times
+the corresponding Higgs generator. It has the component shape of `H†H`. -/
+def normSqTerm : EFTLagrangianExclDeriv :=
+  ∑ α : Fin 2, [barφ α]ₛ * [φ α]ₛ
+
+/-- Projecting the formal Higgs norm square onto one of its two component contents returns
+exactly that component bilinear, with coefficient one. -/
+lemma coeff_normSqTerm (α : Fin 2) :
+    coeff {barφ α, φ α} normSqTerm = [barφ α]ₛ * [φ α]ₛ := by
+  have hterm (β : Fin 2) : [barφ β]ₛ * [φ β]ₛ = termOfList [barφ β, φ β] := by
+    rw [termOfList_cons, termOfList_singleton]
+  rw [normSqTerm, Fin.sum_univ_two, hterm 0, hterm 1, hterm α, map_add,
+    coeff_apply_termOfList, coeff_apply_termOfList]
+  fin_cases α
+  · rw [if_pos (by decide), if_neg (by decide), add_zero]
+    rfl
+  · rw [if_neg (by decide), if_pos (by decide), zero_add]
+    rfl
+
+end EFTLagrangianExclDeriv
+
+end
+
+end StandardModel.HiggsField