Generalized Pauli operators over a field of characteristic two #
The paper's sec:generalized-pauli: for a ∈ F_q^n the X-type operator shifts the
computational basis of (C^q)^{⊗ n} by a, the Z-type operator is diagonal with the phase
ω^{tr(a · b)}, and the two families twisted-commute,
τ^X(a) τ^Z(b) = ω^{-tr(a · b)} τ^Z(b) τ^X(a).
This is the missing half of the Pauli basis test's infrastructure. MIPRE/LCS/Pauli.lean is the
2 × 2 Pauli matrices for the Magic Square; what the appendix's expansion stage and its swap
isometry both run on is the F_q Weyl system, and that is this file.
Two deliberate restrictions #
Characteristic two. The paper states the construction over F_p with ω = e^{2πi/p} and
then specializes. This file is only the p = 2 case, where ω = -1 and every phase is the real
sign MIPRE.sgn of MIPRE/Foundations/Sign.lean. That is not a loss for this project: the
Pauli basis test's parameters are admissible (def:admissible), which means q = 2^k, and no
consumer instantiates it elsewhere. What it buys is large — there are no roots of unity, the
operators are self-adjoint involutions rather than order-p unitaries, so they are genuine
±1-observables, and (τ^W(a))² = 1 is where the paper needs (σ^W(a))^p = I.
One matrix, not an iterated Kronecker product. (C^q)^{⊗ n} is presented as
Matrix (n → F) (n → F) C: the basis of the n-fold tensor power is indexed by the functions
n → F, which is F_q^n. So τ^W(a) is a single matrix and the n-register statements are
the one-register statements with no associativity bookkeeping. The index type n is an arbitrary
finite type rather than Fin n, which is what lets the Pauli basis test use it at
n = (Fin m → Bool), the indexing MIPRE.LowDegree already uses for F_q^M with M = 2^m.
What is here #
wX, wZ, the group laws, self-adjointness, involutivity, unitarity, and the twisted
commutation wX_mul_wZ. Then the Z-eigenbasis projectors, the expansion of wZ in them, and
the Fourier inversion that recovers a projector from an average of operators --- the identity the
expansion stage's E_r (-1)^{tr(ar)} Ŵ^r(u) is an instance of. The X side and the maximally
entangled state come next; they go through the Fourier transform conjugating one family into the
other.
Characteristic two #
Algebra (ZMod 2) F is the whole of the hypothesis: the algebra map from a field is injective,
so F has characteristic two, and every element is its own additive inverse.
The bilinear form #
trDot a b = tr_{q → 2}(a · b), the F_2-valued form the phases are built from. It is the
symmetric bilinear form that decides commutation, and trDotL is it as a linear functional,
which is the shape card_filter_ker_mul' consumes.
tr_{q → 2}(a · b) for a, b ∈ F_q^n.
Equations
- MIPRE.Weyl.trDot a b = (Algebra.trace (ZMod 2) F) (∑ l : n, a l * b l)
Instances For
The form against a fixed b, as an F_2-linear functional.
Equations
- MIPRE.Weyl.trDotL b = { toFun := fun (a : n → F) => MIPRE.Weyl.trDot a b, map_add' := ⋯, map_smul' := ⋯ }
Instances For
The operators #
The section's variables are what Matrix (n → F) (n → F) ℂ needs in order to exist at all ---
DecidableEq (n → F) for the diagonal and the identity, Fintype (n → F) for a matrix product ---
so the rfl-level lemmas below do not each use all of them. The linter is silenced for the
section rather than omit-ed a dozen times.
The Z-type Weyl operator: diagonal, with the sign (-1)^{tr(b · i)}.
Equations
- MIPRE.Weyl.wZ b = Matrix.diagonal fun (i : n → F) => MIPRE.sgn (MIPRE.Weyl.trDot b i)
Instances For
The group laws #
Self-adjointness and unitarity #
Within a family the operators commute #
The twisted commutation relation #
The paper's eq:twisted-fq. In characteristic two the phase ω^{-tr(a·b)} is (-1)^{tr(a·b)}
and there is no sign to track on the exponent.
The anticommuting case: when the form is nonzero the two operators anticommute.
The cancellation lemma #
The paper's lem:cancellation (Fact 3.2 of NW19) in the case that matters here: the character
a ↦ (-1)^{tr(a · c)} of F_q^n is trivial exactly when c = 0, and a nontrivial character sums
to zero. Its \cnote warns that the ambient space must be a subspace over the base field; here
it is the whole of F_q^n over F_2, so the hypothesis is met with nothing to check.
The count comes from card_filter_ker_mul', which says the kernel of a nonzero F_2-functional
has index two --- exactly half the vectors give each sign, so they cancel.
A nontrivial sign character sums to zero.
The trivial character sums to the dimension of the space.
The Z-eigenbasis projectors, and the Fourier inversion #
zProj c projects onto the computational basis vector c, and wZ expands in them with the
sign coefficients (eq:pauli-obs-proj). The inversion eq:pauli-inversion-0 recovers a
projector from an average of operators; it is the identity E_r (-1)^{tr(ar)} Ŵ^r(u) of the
expansion stage, with the average over a line r ↦ r · v rather than over the whole space.
The rank-one projector onto the computational basis vector c.
Equations
- MIPRE.Weyl.zProj c = Matrix.diagonal fun (i : n → F) => if i = c then 1 else 0
Instances For
wZ expands in the computational-basis projectors with the sign coefficients: the
paper's eq:pauli-obs-proj.
The Fourier inversion, the paper's eq:pauli-inversion-0: averaging wZ against the
conjugate character recovers the projector onto a single computational basis vector.
The spectral projectors, once for both families #
Everything the appendix does with the eigenbasis projectors of one family uses only three facts
about it: it represents the additive group of F_q^n, its operators are self-adjoint, and the
identity sits at 0. IsWeylFamily is those three, proj is the Fourier average that builds the
projectors out of them, and the spectral statements are then proved once. wZ is one instance and
wX the other, so the paper's Fourier transform conjugating one family into the other is not
needed to reach the X-side projectors --- worth avoiding, since that transform carries a
q^{-1/2} and would put a square root into matrix entries.
A family of self-adjoint operators indexed by F_q^n representing its additive group. The
two Weyl families are the instances, and the spectral theory needs nothing else.
The family is a homomorphism from the additive group.
The identity sits at
0.Every operator is self-adjoint.
Instances For
The spectral projector of a Weyl family at the eigenvalue pattern e: the Fourier average
of the family against the character of e. For wZ it is zProj e (proj_wZ); for wX it is
the projector onto the X-eigenbasis vector the paper writes |e_X⟩.
Equations
- MIPRE.Weyl.proj w e = (↑(Fintype.card (n → F)))⁻¹ • ∑ a : n → F, MIPRE.sgn (MIPRE.Weyl.trDot a e) • w a
Instances For
The defining Fourier average, as a rewrite.
The Z-family's spectral projectors are the computational-basis ones.
A projector absorbs its own family's operators, up to the sign: one reindexing.
The projectors are mutually orthogonal idempotents.
The projectors of a Weyl family sum to the identity.
A Weyl operator expands in its own projectors with the sign coefficients: the paper's
eq:pauli-obs-proj for either family.
The group law is not used: this is pure Fourier inversion on the index group, and holds for any
family at all. What the group law buys is that the projectors are then mutually orthogonal
(proj_mul_proj), which is what makes them a measurement.
The projectors are self-adjoint.
The X-side projectors, the paper's |e_X⟩⟨e_X|.
Equations
Instances For
The syndrome projectors #
The expansion stage does not average the Weyl family over the whole of F_q^n: it averages over
the line r ↦ r · v for a fixed v ∈ F_q^n, against the character of a field element a. What
comes out is the projector onto the eigenvectors whose F_q-valued pairing with v is a --- the
paper's τ^{W,u}_a = τ^W_{[g_·(u) = a]} of eq:qld-point-obs-def, at v = ind_m(u).
The F_q-valued pairing, before the trace.
Equations
- MIPRE.Weyl.dotF a b = ∑ l : n, a l * b l
Instances For
Scaling one argument of the pairing pulls the scalar out.
The trace against a fixed field element, as an F_2-linear functional on F_q.
Equations
- MIPRE.Weyl.trMulL x = { toFun := fun (r : F) => (Algebra.trace (ZMod 2) F) (r * x), map_add' := ⋯, map_smul' := ⋯ }
Instances For
A nonzero sign character of a finite F_2-space sums to zero. sum_sgn_trDot and
sum_sgn_trMul are its two instances; the content is the index-two kernel of
card_filter_ker_mul'.
The one-field cancellation: the r-average of the sign of tr(r x) vanishes unless x = 0.
A coarse-graining of the eigenbasis measurement: the sum of the spectral projectors over
a level set of an arbitrary label φ. The syndrome projector below is this at
φ = ⟨·, v⟩, and the expansion stage's line measurements are this at the label ``restriction of
the low-degree encoding to the line''.
Equations
- MIPRE.Weyl.synOf w φ o = ∑ e : n → F with φ e = o, MIPRE.Weyl.proj w e
Instances For
The syndrome projector: onto the eigenvectors whose pairing with v is a. The paper's
eq:qld-point-obs-def.
Equations
- MIPRE.Weyl.syn w v a = ∑ e : n → F with MIPRE.Weyl.dotF e v = a, MIPRE.Weyl.proj w e
Instances For
The syndrome projector is the coarse-graining along the pairing.
Coarse-graining a level-set family again is the level-set family of the composite label.
The level sets of g ∘ φ are the unions of the level sets of φ along the level sets of g, so
relabelling a coarse-grained eigenbasis measurement never leaves the family.
The identity the expansion stage calls. Averaging the family along the line r ↦ r · v
against the character of a gives the syndrome projector: the paper's
E_r (-1)^{tr(ar)} \qp^W(r \cdot v) = \qp^W_{[\cdot v = a]}. As with eq_sum_proj, the group law
is not used.