The Pauli basis test as controlled linear constraints #

The tailored question reduction keeps the Pauli basis test's answers as the introspection kernel reads them (MIPRE.Tailored.Intro.pauliLen): a label T has count T m 1 blocks of width T k bits, each block of width k the canonical bits of an element of the effective field shoupBinField k hk, all readable at the Z-basis Pauli label and all linear otherwise (pauliRead). A tailored game may decide only by controlled linear constraints: vectors c over the answer bits of both players and an affine coordinate J, chosen from the questions and the readable bits, each satisfied when ⟨c, (a, b, 1)⟩ = 0 over F₂. This file presents the kernel's Pauli conjunct --- QLD.accepts on the decoded questions and answers --- in that form, pauliCons.

That is possible because every rule of fig:decider_pauli (QLD.pairTest) is a conjunction of F₂-affine equations in the answer bits whose coefficients are computed from the questions, and its disjunctions branch only on the questions:

equal labels compare the answers (sameChecks): bit l of a is bit l of b;
a line against a point (lineChecks): whether the point lies on the line is a question condition (if it fails, LinCheck.reject), and f(τ) = a is F_q-linear in the coefficients of f and in a, with τ the point's parameter;
the point probe of the Pauli outcome (pauliChecks): g_h(y) = ∑_z h(z) ind_z(y) = a, F_q-linear in h and a;
the commutation and Magic Square rules (bitEq, prbCheck, conVarChecks, pointVarChecks) are gated on γ(ω) and on the labels, and check equalities of answer bits, a parity, and the probe tr(a · r) = b, which is F₂-linear in a.

An F_q-equation is the k equations of its coordinates in the canonical basis, under which the field's bit encoding is F₂-linear (MIPRE.Tailored.Intro.fieldChecks). Each check is an F₂-linear functional on the answer bits with a target (LinCheck), and its constraint is the functional on the unit vectors followed by the target (LinCheck.toCon), so pauliCons never reads the readable bits: the readable answer is the Z-basis outcome, compared and probed linearly like the others. The answer bits are read by position: the field element at block i of an answer at offset o is fldAt (o + i k), a bit is getv.

pairChecks_iff: the checks of a pair of questions hold exactly when pairTest accepts the formatted answers read off the bit vector;
pauliCons_iff, the main theorem: for answers of the label lengths, the constraints are satisfied exactly when QLD.accepts holds of the decoded questions and answers, which is the form program_pauli_iff gives the kernel; length_of_mem_pauliCons gives every constraint the length |a| + |b| + 1;
endpointValid_iff: the kernel's endpoint validity is the label's answer length.

The kernel itself is rewritten in PauliConsKernel.lean. pauliCons is a structural function of the questions: the coefficients are the values of explicit field operations (multiplication by question-determined elements, the trace, coordinates) at unit vectors, and the branching is on question data only, so a polynomial-time program computes it by evaluating each check at the |a| + |b| unit vectors.

The Pauli basis test as controlled linear constraints #

The checks of each rule #

Reading the answers #

Each rule's checks hold exactly when the rule accepts #

Reading each answer format #

The checks of pairTest #

Equal types #

The constraints #

The checks of `pairTest` #