Determinant and energy identities for Higgs walls

Polynomial identities, over any commutative ring, behind the analysis of Higgs walls in six-dimensional gauge-Higgs unification: the rank-one wall determinant, the neutral 3 × 3 Gram determinant and its sum-of-squares decomposition, and the rationalized gap formula. They do not formalize traces in H¹, the Robin boundary problem, the positivity of its spectrum or the physical derivation of the input matrices.

Main results

• amplitude_circle: (p² − q²)² + (2pq)² = (p² + q²)² (the parametrization of Pythagorean triples; Mathlib's PythagoreanTriple is stated over ℤ).
• rank_one_wall_det: det [[a x², a x y], [a x y, a y² + b]] = a b x².
• gap_discriminant, gap_rationalization: (r + t − z)(r + t + z) = 4rt(1 − c) when z² = (r − t)² + 4rtc.
• neutral_three_det: the neutral 3 × 3 Gram determinant is a b x² (k + a(1 − d²)).
• neutral_energy_decomposition: the corresponding quadratic form is a (x u + y v − d w)² + b v² + (k + a(1 − d²)) w².

def GaugeHiggsUnification.WallDeterminants.det2 {R : Type u_1} [CommRing R] (a b c d : R) : R

The 2 × 2 determinant.

Equations

• GaugeHiggsUnification.WallDeterminants.det2 a b c d = a * d - b * c

def GaugeHiggsUnification.WallDeterminants.det3 {R : Type u_1} [CommRing R] (a b c d e f g h i : R) : R

The 3 × 3 determinant, expanded along the first row.

Equations

• GaugeHiggsUnification.WallDeterminants.det3 a b c d e f g h i = a * (e * i - f * h) - b * (d * i - f * g) + c * (d * h - e * g)

theorem GaugeHiggsUnification.WallDeterminants.amplitude_circle {R : Type u_1} [CommRing R] (p q : R) : (p ^ 2 - q ^ 2) ^ 2 + (2 * p * q) ^ 2 = (p ^ 2 + q ^ 2) ^ 2

The amplitude circle.

theorem GaugeHiggsUnification.WallDeterminants.rank_one_wall_det {R : Type u_1} [CommRing R] (a b x y : R) : det2 (a * x ^ 2) (a * x * y) (a * x * y) (a * y ^ 2 + b) = a * b * x ^ 2

The rank-one wall determinant.

theorem GaugeHiggsUnification.WallDeterminants.gap_discriminant {R : Type u_1} [CommRing R] (r t c : R) : (r + t) ^ 2 - ((r - t) ^ 2 + 4 * r * t * c) = 4 * r * t * (1 - c)

The discriminant of the gap.

theorem GaugeHiggsUnification.WallDeterminants.gap_rationalization {R : Type u_1} [CommRing R] (r t c z : R) (hz : z ^ 2 = (r - t) ^ 2 + 4 * r * t * c) : (r + t - z) * (r + t + z) = 4 * r * t * (1 - c)

The cross-multiplied, stable form of the gap formula; no division is involved.

theorem GaugeHiggsUnification.WallDeterminants.neutral_three_det {R : Type u_1} [CommRing R] (a b k d x y : R) : det3 (a * x ^ 2) (a * x * y) (-a * d * x) (a * x * y) (a * y ^ 2 + b) (-a * d * y) (-a * d * x) (-a * d * y) (a + k) = a * b * x ^ 2 * (k + a * (1 - d ^ 2))

The neutral Gram determinant [[a x², a x y, −a d x], [a x y, a y² + b, −a d y], [−a d x, −a d y, a + k]]; b is the coefficient of the bulk field and k the total additional hidden coefficient.

theorem GaugeHiggsUnification.WallDeterminants.neutral_energy_decomposition {R : Type u_1} [CommRing R] (a b k d x y u v w : R) : a * x ^ 2 * u ^ 2 + (a * y ^ 2 + b) * v ^ 2 + (a + k) * w ^ 2 + 2 * a * x * y * u * v - 2 * a * d * x * u * w - 2 * a * d * y * v * w = a * (x * u + y * v - d * w) ^ 2 + b * v ^ 2 + (k + a * (1 - d ^ 2)) * w ^ 2

The neutral quadratic form as a sum of three weighted squares.

theorem GaugeHiggsUnification.WallDeterminants.endpoint_det_factor {R : Type u_1} [CommRing R] (a b k x : R) : a * b * x ^ 2 * (k + a * (1 - 1 ^ 2)) = a * b * x ^ 2 * k

The determinant factor at the endpoint d = 1.

theorem GaugeHiggsUnification.WallDeterminants.balanced_det_factor {R : Type u_1} [CommRing R] (a b k x : R) : a * b * x ^ 2 * (k + a * (1 - 0 ^ 2)) = a * b * x ^ 2 * (k + a)

The determinant factor at the balanced point d = 0.

theorem GaugeHiggsUnification.WallDeterminants.weighted_energy_addition {R : Type u_1} [CommRing R] (a b x y : R) : a * x * x + b * y * y = a * x ^ 2 + b * y ^ 2

The scalar skeleton of the energy addition.