The sign of a bit

sgn x = (-1)^x for x : ZMod 2, as a complex number. It is the character group of 𝔽₂ written multiplicatively, and it is what every ±1-observable in this development is built from: the observable of a two-outcome measurement, the phase of a Weyl operator in characteristic two, and the sign a Magic Square constraint carries.

Characteristic two is why this is a sign and not a root of unity. Over 𝔽_p the generalized Pauli operators carry phases e^{2πi/p}; this project's fields are always of admissible size q = 2^k, so p = 2 and every phase is real. That collapse is worth having in one place.

def MIPRE.sgn (x : ZMod 2) : ℂ

(-1)^x for a bit x.

Equations

• MIPRE.sgn x = if x.val = 1 then -1 else 1

theorem MIPRE.sgn_add (x y : ZMod 2) : sgn (x + y) = sgn x * sgn y

theorem MIPRE.sgn_mul_self (x : ZMod 2) : sgn x * sgn x = 1

theorem MIPRE.star_sgn (x : ZMod 2) : star (sgn x) = sgn x

@[simp]

theorem MIPRE.sgn_zero : sgn 0 = 1

@[simp]

theorem MIPRE.sgn_one : sgn 1 = -1

theorem MIPRE.sgn_sum {α : Type u_1} (s : Finset α) (f : α → ZMod 2) : sgn (∑ i ∈ s, f i) = ∏ i ∈ s, sgn (f i)

sgn turns a sum of bits into a product of signs: it is a character of 𝔽₂.

theorem MIPRE.norm_sgn (x : ZMod 2) : ‖sgn x‖ = 1

sgn takes values ±1, hence modulus one.

theorem MIPRE.sum_sgn : ∑ x : ZMod 2, sgn x = 0

Summing sgn over both bits gives zero: the character is nontrivial.