The blind set of the boundary-condition sign and its count

A bulk SU(4) irrep is a partition λ = (l₁, l₂, l₃, 0) with l₁ ≥ l₂ ≥ l₃ ≥ 0. The reflection-coset character is D_λ(t) = s_λ(1, −1, t, 1/t) and the boundary-condition sign η acts by D ↦ η D, so η is unobservable on λ iff D_λ = 0. In Dynkin coordinates (a, b, c) with λ = (a+b+c, b+c, c, 0), GaugeHiggsUnification.NotchCentreCharge.notch_degenerate_iff gives the vanishing criterion N a b c = 0 ↔ Odd b ∧ ((Odd a ∧ Odd c) ∨ a = c). This file writes that set (the blind set) in partition coordinates and counts it.

Main results

• Blind: the blind set as two branches: (a) l₁ odd, l₂ even, l₃ odd; (b) l₁ odd, l₂ odd, l₃ even with l₂ + l₃ = l₁.
• blind_iff_notch: on l₁ ≥ l₂ ≥ l₃ this is the Dynkin-coordinate criterion.
• blind_iff_N_zero: Blind holds iff the bialternant determinant N vanishes.
• blind_l1_odd: l₁ is odd on the whole blind set.
• card_shell: the blind partitions with l₁ = 2k+1 number ⌈(k+1)²/2⌉. The parity of l₂ splits them into the two branches: branch (a) is the strict pairs q < p ≤ k (a triangular number, via Finset.sum_range_id_mul_two) and branch (b) is the interval m ≤ k/2.

References

• C. Marín, What the Higgs Potential Cannot See: Bulk Matter That Cannot Help Select a Boundary Condition (Part V), Zenodo, doi:10.5281/zenodo.21727094.

The blind set in partition coordinates

def GaugeHiggsUnification.BlindCount.Blind (l₁ l₂ l₃ : ℕ) : Prop

Blind l₁ l₂ l₃: the boundary sign η is unobservable on λ = (l₁,l₂,l₃,0). Branch (a) is l₁ odd, l₂ even, l₃ odd; branch (b) is l₁ odd, l₂ odd, l₃ even with l₂ + l₃ = l₁. Stated with % 2 rather than Odd/Even so that the predicate is decidable by decide and native to omega.

Equations

• GaugeHiggsUnification.BlindCount.Blind l₁ l₂ l₃ = (l₁ % 2 = 1 ∧ l₂ % 2 = 0 ∧ l₃ % 2 = 1 ∨ l₁ % 2 = 1 ∧ l₂ % 2 = 1 ∧ l₃ % 2 = 0 ∧ l₂ + l₃ = l₁)

@[instance_reducible]

instance GaugeHiggsUnification.BlindCount.instDecidableBlind (l₁ l₂ l₃ : ℕ) : Decidable (Blind l₁ l₂ l₃)

Equations

• GaugeHiggsUnification.BlindCount.instDecidableBlind l₁ l₂ l₃ = id inferInstance

theorem GaugeHiggsUnification.BlindCount.blind_l1_odd {l₁ l₂ l₃ : ℕ} (h : Blind l₁ l₂ l₃) : Odd l₁

l₁ is odd on the whole blind set: half the bulk spectrum cannot be blind.

theorem GaugeHiggsUnification.BlindCount.blind_iff_parity (l₁ l₂ l₃ : ℕ) : Blind l₁ l₂ l₃ ↔ Odd l₁ ∧ Even l₂ ∧ Odd l₃ ∨ Odd l₁ ∧ Odd l₂ ∧ Even l₃ ∧ l₂ + l₃ = l₁

The Odd/Even restatement, for reading against the paper.

The dictionary to Dynkin coordinates

theorem GaugeHiggsUnification.BlindCount.blind_iff_notch {l₁ l₂ l₃ : ℕ} (h₃ : l₃ ≤ l₂) (h₂ : l₂ ≤ l₁) : Blind l₁ l₂ l₃ ↔ Odd (l₂ - l₃) ∧ (Odd (l₁ - l₂) ∧ Odd l₃ ∨ l₁ - l₂ = l₃)

The dictionary. With a = l₁ - l₂, b = l₂ - l₃, c = l₃ (the inverse of λ = (a+b+c, b+c, c, 0)), the partition-coordinate description of the blind set is the Dynkin-coordinate criterion certified in NotchCentreCharge.

theorem GaugeHiggsUnification.BlindCount.blind_iff_N_zero {l₁ l₂ l₃ : ℕ} (h₃ : l₃ ≤ l₂) (h₂ : l₂ ≤ l₁) : Blind l₁ l₂ l₃ ↔ NotchCentreCharge.N (l₁ - l₂) (l₂ - l₃) l₃ = 0

The bridge: η is unobservable on λ exactly when the bialternant determinant certified in NotchCentreCharge vanishes.

The shell at l₁ = 2k+1

def GaugeHiggsUnification.BlindCount.shell (k : ℕ) : Finset (ℕ × ℕ)

The blind partitions with λ₁ = 2k+1, recorded as the pair (λ₂, λ₃).

Equations

• GaugeHiggsUnification.BlindCount.shell k = {p ∈ Finset.range (2 * k + 2) ×ˢ Finset.range (2 * k + 2) | p.2 ≤ p.1 ∧ GaugeHiggsUnification.BlindCount.Blind (2 * k + 1) p.1 p.2}

theorem GaugeHiggsUnification.BlindCount.mem_shell {k : ℕ} {p : ℕ × ℕ} : p ∈ shell k ↔ p.1 ≤ 2 * k + 1 ∧ p.2 ≤ p.1 ∧ Blind (2 * k + 1) p.1 p.2

Membership in the shell, unfolded.

def GaugeHiggsUnification.BlindCount.shellA (k : ℕ) : Finset (ℕ × ℕ)

Branch (a): λ₂ even. Parametrised by q < p ≤ k via (λ₂,λ₃) = (2p, 2q+1).

Equations

• GaugeHiggsUnification.BlindCount.shellA k = (Finset.range (k + 1)).biUnion fun (p : ℕ) => Finset.image (fun (q : ℕ) => (2 * p, 2 * q + 1)) (Finset.range p)

def GaugeHiggsUnification.BlindCount.shellB (k : ℕ) : Finset (ℕ × ℕ)

Branch (b): λ₂ odd. Parametrised by m ≤ k/2 via (λ₂,λ₃) = (2k+1-2m, 2m).

Equations

• GaugeHiggsUnification.BlindCount.shellB k = Finset.image (fun (m : ℕ) => (2 * k + 1 - 2 * m, 2 * m)) (Finset.range (k / 2 + 1))

theorem GaugeHiggsUnification.BlindCount.mem_shellA {k : ℕ} {p : ℕ × ℕ} : p ∈ shellA k ↔ ∃ (a : ℕ), ∃ b < a, a ≤ k ∧ p = (2 * a, 2 * b + 1)

theorem GaugeHiggsUnification.BlindCount.mem_shellB {k : ℕ} {p : ℕ × ℕ} : p ∈ shellB k ↔ ∃ m ≤ k / 2, p = (2 * k + 1 - 2 * m, 2 * m)

theorem GaugeHiggsUnification.BlindCount.filter_even_shell (k : ℕ) : {p ∈ shell k | p.1 % 2 = 0} = shellA k

The parity of λ₂ splits the shell into exactly the two branches: the even part is branch (a).

theorem GaugeHiggsUnification.BlindCount.filter_odd_shell (k : ℕ) : {p ∈ shell k | ¬p.1 % 2 = 0} = shellB k

... and the odd part is branch (b).

The two cardinals

theorem GaugeHiggsUnification.BlindCount.card_shellA (k : ℕ) : (shellA k).card * 2 = (k + 1) * k

theorem GaugeHiggsUnification.BlindCount.card_shellB (k : ℕ) : (shellB k).card = k / 2 + 1

The count

theorem GaugeHiggsUnification.BlindCount.card_shell (k : ℕ) : (shell k).card = ((k + 1) ^ 2 + 1) / 2

Proposition (Part V). The blind partitions with λ₁ = 2k+1 number ⌈(k+1)²/2⌉. Together with blind_l1_odd (no even λ₁ is ever blind) this is the complete census of the blind set shell by shell.

Sanity checks