Central action in the hidden (1, 5, 4) basis

Finite integer arithmetic in the basis (1, 5, 4) of hidden-sector multiplicities (a, b, c): dimension a + 5b + 4c, central action a + 5b − 4c. The central actions assigned to the Lie representations are input data; no Wilson loop, topology or anomaly cancellation is formalized.

Main results

• center_original, center_alternative, center_jump: the central actions −3 and 13 of the two candidate contents, which differ by 16.
• center_resolves_integer_kernel: dimension, second moment and central action together determine the multiplicities (augmented determinant −32).
• simultaneous_central_descent: both central signs are trivial iff both markers are trivial.

def GaugeHiggsUnification.HiddenCentreBasis.center (a b c : ℤ) : ℤ

The central action of the content (a, b, c).

Equations

• GaugeHiggsUnification.HiddenCentreBasis.center a b c = a + 5 * b - 4 * c

theorem GaugeHiggsUnification.HiddenCentreBasis.center_original : center 0 1 2 = -3

The central action of the original content.

theorem GaugeHiggsUnification.HiddenCentreBasis.center_alternative : center 3 2 0 = 13

The central action of the alternative content.

theorem GaugeHiggsUnification.HiddenCentreBasis.center_jump : center 3 2 0 - center 0 1 2 = 16

The two central actions differ by 16.

theorem GaugeHiggsUnification.HiddenCentreBasis.center_augmented_determinant : 1 * (4 * -4 - 2 * 5) - 5 * (0 * -4 - 2 * 1) + 4 * (0 * 5 - 4 * 1) = -32

The determinant of the system (dimension, second moment, central action).

theorem GaugeHiggsUnification.HiddenCentreBasis.center_resolves_integer_kernel (a b c : ℤ) (hd : a + 5 * b + 4 * c = 0) (h2 : 4 * b + 2 * c = 0) (hz : a + 5 * b - 4 * c = 0) : a = 0 ∧ b = 0 ∧ c = 0

Dimension, second moment and central action have trivial common integer kernel.

theorem GaugeHiggsUnification.HiddenCentreBasis.simultaneous_central_descent (a b : Bool) : a = false ∧ (a ^^ b) = false ↔ a = false ∧ b = false

With a, b marking nontrivial central elements of Spin(11) and USp(4), the sign on (32, 5) is a and on (32, 4) it is a xor b; both vanish iff a and b do.