The notch decouples the fermion sector from the leading curvature

The leading Kaluza–Klein order of the curvature at the half point is 𝒟 = π² (∑_{m ≡ 2 (4)} m² δ(m) − ∑_{m ≡ 0 (4)} m² δ(m)), with δ(m) = mult(m,0) − mult(m,1) over a finite set of levels. It is linear in δ and vanishes when δ(m) = 0 at every even m (the notch), so the fermion sector drops out and 𝒟 is the gauge part alone. On range (2N) it is the plain alternating weight −4π² ∑_{m' < N} (−1)^{m'} m'² δ(2m'). That 𝒟 is the leading curvature is physics and is not formalized here.

Main results

• GaugeHiggsUnification.NotchDecoupling.curv_add: 𝒟 is additive in δ.
• GaugeHiggsUnification.NotchDecoupling.curv_eq_zero_of_even: δ = 0 on even levels gives 𝒟 = 0.
• GaugeHiggsUnification.NotchDecoupling.curv_decoupling: the fermion imbalance drops out.
• GaugeHiggsUnification.NotchDecoupling.curv_range_eq_alternating: the alternating form.

References

• C. Marín, A Centre-Charge Selection Rule for the Wilson-Line Potential: The Fundamental Domain of Gauge-Higgs Unification Is Representation-Dependent (Part III), Zenodo (2026), doi:10.5281/zenodo.21466370, Corollary cor:decoupling and eq. (Dstruct).

noncomputable def GaugeHiggsUnification.NotchDecoupling.curv (S : Finset ℕ) (δ : ℕ → ℝ) : ℝ

The leading Kaluza–Klein curvature built from the imbalance δ over the levels S.

Equations

• GaugeHiggsUnification.NotchDecoupling.curv S δ = Real.pi ^ 2 * (∑ m ∈ S with m % 4 = 2, ↑m ^ 2 * δ m - ∑ m ∈ S with m % 4 = 0, ↑m ^ 2 * δ m)

theorem GaugeHiggsUnification.NotchDecoupling.curv_add (S : Finset ℕ) (δ₁ δ₂ : ℕ → ℝ) : curv S (δ₁ + δ₂) = curv S δ₁ + curv S δ₂

theorem GaugeHiggsUnification.NotchDecoupling.curv_eq_zero_of_even {S : Finset ℕ} {δ : ℕ → ℝ} (h : ∀ m ∈ S, Even m → δ m = 0) : curv S δ = 0

theorem GaugeHiggsUnification.NotchDecoupling.curv_decoupling {S : Finset ℕ} (δG δF : ℕ → ℝ) (h : ∀ m ∈ S, Even m → δF m = 0) : curv S (δG + δF) = curv S δG

Decoupling: if the fermion imbalance vanishes on every even level, 𝒟 is the gauge part alone.

theorem GaugeHiggsUnification.NotchDecoupling.curv_range_eq_alternating (N : ℕ) (δ : ℕ → ℝ) : curv (Finset.range (2 * N)) δ = -4 * Real.pi ^ 2 * ∑ k ∈ Finset.range N, (-1) ^ k * ↑k ^ 2 * δ (2 * k)

The paper's rewriting m = 2m': a plain alternating weight.