Reality of a scalar CP source

A small algebraic control: if the quartic coefficient λ and both Higgs-wall backgrounds v₁, v₂ are real, the imaginary part of the relative-phase scalar source λ (conj v₁ · v₂)² vanishes. It says nothing about CP violation in the full six-dimensional SU(4) model, which also depends on its fermion and boundary sectors; it is the scalar-sector statement only.

Main results

• real_scalar_wall_source_vanishes: Im (λ (conj v₁ · v₂)²) = 0 for real λ, v₁, v₂.
• real_scalar_wall_source_with_prefactor_vanishes: the same after multiplication by any real radial prefactor.

theorem GaugeHiggsUnification.ScalarCPSource.real_scalar_wall_source_vanishes (lambda v₁ v₂ : ℝ) : (↑lambda * ((starRingEnd ℂ) ↑v₁ * ↑v₂) ^ 2).im = 0

If the quartic coefficient and both Higgs-wall backgrounds are real, the imaginary part of the relative-phase scalar source vanishes.

theorem GaugeHiggsUnification.ScalarCPSource.real_scalar_wall_source_with_prefactor_vanishes (prefactor lambda v₁ v₂ : ℝ) : prefactor * (↑lambda * ((starRingEnd ℂ) ↑v₁ * ↑v₂) ^ 2).im = 0

The same conclusion after multiplication by any real radial prefactor.