Matter: the Yukawa term plus its hermitian conjugate is real
ProvedEveryday.yukawa_realThe image's matter label is the fermion kinetic term together with the Yukawa coupling ψ̄_L V Φ ψ_R and its hermitian conjugate — the sector by which fermions acquire mass from the Higgs field. The item is the "+ h.c." of the source equation: the Yukawa term of the discrete arena — the contraction of the left-handed fermion field with the coupling constant and the Higgs field against the right-handed fermion field, summed over the spacetime — is a complex number with no reason to be real; but the Yukawa term plus its hermitian conjugate, exactly the combination the source equation writes, is a real number. The matter contribution to the action is real.
Formalization Note The hermitian conjugate is the complex conjugate, the arena being a scalar (one-component) fragment of the source's matrix contraction. The proof: the imaginary part of a sum is the sum of the imaginary parts, and the imaginary part of a conjugate is the negation of the imaginary part, so the goal reduces to the sum of a real number and its negation, which vanishes. The conclusion is the vanishing of the imaginary part.
import Mathlib import Definitions.Def_Everyday_spacetime import Definitions.Def_Everyday_sectors
open ComplexConjugate
namespace Everyday
/-- Matter: the Yukawa coupling plus its hermitian conjugate is real —
the "+ h.c." of the source equation makes the matter contribution to
the action a real number. -/
theorem yukawa_real {X : Type} [Fintype X] (ψL ψR : X → ℂ) (V : ℂ) (Φh : X → ℂ) :
(yukawaTerm ψL ψR V Φh + conj (yukawaTerm ψL ψR V Φh)).im = 0 := by sorry
end Everyday
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
The statement says: for every type X equipped with the structure of a finite type, all complex-valued functions ψL, ψR, and Φh on X, and every complex number V, the imaginary part of the complex number (yukawaTerm ψL ψR V Φh plus the complex conjugate of yukawaTerm ψL ψR V Φh) is zero. Unfolding the definition, yukawaTerm is the sum over x of the complex conjugate of ψL x, times V, times Φh x, times ψR x. The conclusion is an equation between real numbers.