When is a Pauli-test question tuple anticommuting? #
The Pauli basis test samples ω = (u_X, u_Z, r_X, r_Z) and the two Pauli operators it asks
about commute or anticommute according to whether
γ(ω) = tr_{q → 2} \bigl( (r_X · ind_m(u_X)) · (r_Z · ind_m(u_Z)) \bigr)
vanishes. The paper's fact:omega-anticomm-prob says each case has probability at least
(1 - 3md/q)/2; this file is that fact.
ind_m(x) ∈ 𝔽_q^{2^m} is the vector of the subcube indicator polynomials of
MIPRE/Foundations/LowDegree/Encoding.lean evaluated at an arbitrary point x, and the
dot product of two of them is one low-degree encoding evaluated at the other point
(indPair_eq_eval). So the fact is Schwartz--Zippel --- the encoding is a nonzero polynomial,
because ind_m(x) is never the zero vector (sum_indVec, whose value is 1) --- together with
the count of r in the kernel of a nonzero 𝔽-linear functional (card_filter_ker_mul).
Two departures from the paper, both recorded in the blueprint's comments on the fact:
- the wasteful factor is dropped. The paper states
(1 - q^{-m})(1 - q^{-1})(1 - md/q)/2, whose first factor came from a case distinction onu_X = 0that its own\cnotethen removes as vacuous. The bound proved here is(1 - (m+1)/q)/2, which is sharper than the paper's final(1 - 3md/q)/2and needs no such factor. - individual degree, not total degree. The low-degree encoding is multilinear, so the
Schwartz--Zippel step costs
m/qrather than themd/qthe paper spends. The paper's form is recovered inprob_anticommuting_gefor1 ≤ d.
The indicator vector at an arbitrary point #
ind_m(x), the vector of the subcube indicator polynomials evaluated at x. For a subcube
point this is the standard basis vector at that point (eval_ind); the definition is what the
Pauli basis test uses at a general x ∈ 𝔽_q^m.
Equations
- MIPRE.LowDegree.indVec x y = (MvPolynomial.eval x) (MIPRE.LowDegree.ind y)
Instances For
ind_m(x) has coordinate sum 1, hence is never the zero vector: the sum telescopes to
∏_i (x_i + (1 - x_i)) = 1. This is the observation the paper's \cnote adds, and it is what
makes the case distinction on u_X = 0 unnecessary.
The dot product ind_m(x) · ind_m(z), which is the γ of the Pauli basis test up to the
scalars r_X r_Z and the trace.
Equations
- MIPRE.LowDegree.indPair x z = ∑ y : Fin m → Bool, MIPRE.LowDegree.indVec x y * MIPRE.LowDegree.indVec z y
Instances For
The pairing is one low-degree encoding evaluated at the other point. This is the identity the paper's proof opens with, and it is what puts Schwartz--Zippel in reach.
The kernel of a nonzero linear functional #
The kernel-index count is about a finite 𝔽-vector space, not about a field extension: the
proof uses only the module structure and a vector off the kernel. It is stated that way because
the Weyl operators of MIPRE/Foundations/Weyl.lean need it on n → 𝔽, where the phase
(-1)^{tr(a · b)} is summed over a whole register rather than over a single field element. The
field-extension form below is the instance V = K.
A nonzero 𝔽-linear functional on a finite 𝔽-vector space has kernel of index |𝔽|.
Every fibre is a translate of the kernel, and there are |𝔽| of them.
A nonzero 𝔽-linear functional has kernel of index |𝔽|: card_filter_ker_mul' at
V = K.
The trace against a fixed nonzero element is a nonzero functional, so its kernel is again
of index |𝔽|.
The fact #
Over 𝔽₂, exactly half the field is off the kernel.
γ(ω), the quantity of the Pauli basis test whose vanishing says that the two Pauli
operators of the tuple ω = (u_X, u_Z, r_X, r_Z) commute: the trace of the dot product of
r_X · ind_m(u_X) with r_Z · ind_m(u_Z).
Equations
- MIPRE.LowDegree.acGamma F uX uZ rX rZ = (Algebra.trace F K) (rX * rZ * MIPRE.LowDegree.indPair uX uZ)
Instances For
The anticommuting tuples, as a Finset of the sample space.
Equations
- MIPRE.LowDegree.acTuples F m = {ω : (Fin m → K) × (Fin m → K) × K × K | MIPRE.LowDegree.acGamma F ω.1 ω.2.1 ω.2.2.1 ω.2.2.2 ≠ 0}
Instances For
The commuting tuples.
Equations
- MIPRE.LowDegree.cTuples F m = {ω : (Fin m → K) × (Fin m → K) × K × K | MIPRE.LowDegree.acGamma F ω.1 ω.2.1 ω.2.2.1 ω.2.2.2 = 0}
Instances For
At a nonzero pairing value, half the (r_X, r_Z) with r_X ≠ 0 are anticommuting.
The anticommuting count, one question pair at a time.
The Schwartz--Zippel step #
The pairing vanishes at few u_Z. ind_m(u_X) is a nonzero vector, so its low-degree
encoding is a nonzero multilinear polynomial and Schwartz--Zippel costs m/q, not md/q.
The two counts #
The anticommuting pairs (r_X, r_Z) are at least half of those with r_X ≠ 0, and the
pairing is nonzero for all but a m/q fraction of the u_Z.
Over 𝔽₂, exactly half the field is in the kernel.
The same lower bound for the commuting pairs, and this time at every (u_X, u_Z): when
the pairing vanishes every pair is commuting, and otherwise the r_X ≠ 0 pairs already supply
half of (q-1) q.
The two cases partition the sample space. This is what makes the pair of bounds below
informative rather than merely true: they add to at least 1 - (m+2)/q, so neither set can be
much more than half, and in particular neither is everything.
The fact #
fact:omega-anticomm-prob, sharp form: an anticommuting tuple has probability at least
(1 - (m+1)/q)/2.
fact:omega-anticomm-prob, commuting case: a commuting tuple has probability at least
(1 - 1/q)/2, with no m at all.
fact:omega-anticomm-prob in the paper's shape: both cases have probability at least
(1 - 3md/q)/2. The hypotheses 1 ≤ m and 1 ≤ d are what makes m + 1 ≤ 3md; the sharp
forms above need neither.
The commuting case in the paper's shape.