Axiom audit for the Pauli basis test

MIPRE/Background/QLD/ is this project's own mathematics, like the seeded-CL adapter of MIPRE/Background/LIDT/Adapter/; it sits under MIPRE/Background/ because it reaches into the vendored developments, and its guards are cheapest here, where the imports are already paid for. scripts/lean-coverage.py reads every guard file and checks that the names guarded are exactly the names the blueprint marks with a proof-level \leanok, so which file a name sits in does not change what is claimed.

The Magic Square's anticommutation input

Blueprint lem:ms-direct-anticomm. Both halves and the averaged form; anti is the anticommutator the statement is about.

What winning the Pauli basis test implies

Blueprint lem:qld-win. The seven items, and the supporting vocabulary the proof of each one runs through. #guard_sorry_free rather than #print axioms here: the list mixes definitions with theorems, and their axiom lists differ.

Signed commutation, the anticommuting case

Blueprint lem:qld-obs-commutation-acomm. The two point observables and the two variable observables they are tied to, the sub-probability weight the items carry, item 7 in observable form, the identification of item 6's anticommutator, and the lemma.

The expansion stage's commutation

Blueprint lem:qld-expanded-commutation. The sign the strategy carries and the sign the ancilla carries are the same sign, and they cancel identically.

The expansion stage: the hatted line measurements

Blueprint lem:qld-expanded-lines. The convolution of the strategy's line measurement with the ancilla measurement that reports the restriction of the encoding to the line; its projectivity, its self-consistency, and its consistency with the hatted point measurements.

Signed commutation: both halves

Blueprint lem:qld-obs-commutation, lem:qld-obs-commutation-comm and lem:qld-obs-commutation-acomm. The commuting half runs the chain through the Pair measurement, projectivizes it, and applies the commutation analysis; the anticommuting half is the Magic Square's anticommutator carried across the tensor factors.

The combining stage: the joint XZ point measurement

Blueprint lem:qld-combined-points. The hatted point measurement re-indexed by the point, its observable family and the transform between them, Parseval for the commutator, the content split that makes the probe average free, the two players' commutation inputs, and the lemma.

The padded point measurement

Blueprint lem:qld-padded-points. The combined measurement coarse-grained along (a, b) |-> alpha a + beta b, Bob's two ordered products and their completeness, the Parseval identity for the coarse-graining, and the lemma.

Pairs of lines

Blueprint lem:qld-pairs-of-lines. The bridge from coefficient vectors to Mathlib's polynomials and the collision count it gives; the content shift, which is what turns the content distribution into the product the pasting lemma's collision term needs, and the same device applied to the raw direction, which is what makes a degenerate diagonal line rare; the line presentations and their invariances; the marginal step at the QLD point measurements; and the lemma, both for an arbitrary pair of presentations and with every input discharged from the game.

The sublines of a padded line

Blueprint lem:qld-sublines. The seed's block and offset; the blocks of the padded space and the four-way case distinction on a coordinate position; the sampling procedure and the containment it is built to satisfy; and the law, as four identities of averages, one per case of the construction.

The padded line measurement

Blueprint lem:qld-padded-lines. The content/product transfer and the product form of the pairs-of-lines lemma; the combining map, its two degree bounds and the measurement it defines; the restricted laws and the domination of the padded law by the product law; and the consistency bound in both register versions.

The axis-parallel degree bound

Blueprint lem:qld-axis-degree: the degree computation, the legalization of a strategy that makes the paper's format convention available at no cost, and the exact support of the expanded and padded axis-line measurements on degree at most d.

The padded strategy and its value

Blueprint lem:qld-global-setup: mixtures and uniform averages of POVMs, the support-aware conditional-failure bounds, the seeded test's value sample by sample, and the padded strategy on the seeded test at (q, 4m, d, 1) with the two invariances that let the decider's reading be the quantity lem:qld-padded-lines controls.

Blueprint lem:qld-global-setup, continued: the divisibility 4m | q from m | q and 4m <= q, which the regime 48md <= q supplies (MIPRE/Background/QLD/Regime.lean).

Blueprint lem:qld-global-success: the agreement triangle, the conditional failure of the padded strategy at each of the nine ordered type pairs, and the value bound.

lem:qld-global-pvm (MIPRE/Background/QLD/PaddedLIDT.lean: the seeded test's soundness, a hypothesis on the model, applied in the padded model of MIPRE/Background/QLD/PhysModel.lean).

lem:lidt-ldc-extraction, its coefficient-vector algebra (MIPRE/Background/LIDT/Coefficients.lean), which stage 4 of the Pauli basis test shares; the lemma's other declarations are guarded in MIPRE/Axioms.lean.

lem:qld-global-dummy (MIPRE/Background/QLD/Dummy.lean, and its specialization in MIPRE/Background/QLD/PaddedLIDT.lean).

lem:qld-global-products (MIPRE/Background/QLD/Products.lean, and its specialization to a GlobalPair in MIPRE/Background/QLD/PaddedLIDT.lean).

lem:qld-global-linear (MIPRE/Background/QLD/Linear.lean, and its specialization to a GlobalPair in MIPRE/Background/QLD/PaddedLIDT.lean).

Actual Pauli CL sampler content and honest measurements

lem:qld-global-separate (MIPRE/Background/QLD/Separate.lean, and its specialization to a GlobalPair in MIPRE/Background/QLD/PaddedLIDT.lean).

lem:qld-global-complete (MIPRE/Background/QLD/Complete.lean).

lem:qld-global-sandwich (MIPRE/Background/QLD/Complete.lean).

lem:qld-global-robustness (MIPRE/Background/QLD/Complete.lean for the marginals, MIPRE/Background/QLD/PaddedLIDT.lean for the errors).

lem:qld-simultaneous (MIPRE/Background/QLD/Simul.lean for the structure, MIPRE/Background/QLD/PaddedLIDT.lean for the instance).

lem:qld-helper (MIPRE/Background/QLD/Helper.lean, with the state-norm transfers in MIPRE/Background/QLD/Simul.lean).

lem:qld-exact-paulis. The exact half is MIPRE/Background/QLD/{ExactPauli,SwapUnitary}.lean, the approximate half MIPRE/Background/QLD/{NonMultilinear,PauliBasis,Multilinear}.lean, and the reading of the latter as a closeness of two measurements MIPRE/Background/QLD/MTilde.lean.

lem:qld-pauli-selfcons: the self-consistency of the exact Pauli observables (MIPRE/Background/QLD/{Pulling,Chain,ChainProbe,ChainAssembly,SelfCons}.lean and the files they build on). Formalized in #183; the marks and this guard were added with thm:qld, which rests on it through lem:qld-swap.

lem:qld-swap: the swap isometry, both items relative to one auxiliary state. The exact pieces are MIPRE/Background/QLD/SwapUnitary.lean, item 1 MIPRE/Background/QLD/{SwapState,SwapItemOne}.lean, the endgame's steps MIPRE/Background/QLD/{SwapMeasure,SwapEndgame}.lean, and item 2's threading and the joint statement MIPRE/Background/QLD/SwapItemTwo.lean.

lem:qld-error: the error of thm:qld, named once (qldErr, MIPRE/Background/QLD/QLDError.lean), and the closure calculus showing it is of the closed form (MIPRE/Background/QLD/ErrorShape.lean); the seeded soundness error's link is guarded with the declarations added in the bipartite restatement, below.

thm:qld: the Pauli basis test, in a bipartite model, from the soundness of the seeded test in its extensions (MIPRE/Background/QLD/Soundness.lean: soundIn_of_lidt, with the legalization, the trivial extraction outside the regime, and the extraction by the swap isometry inside it).

cor:qld-valid: thm:qld at the genuine full-register answers, for a strategy supported on correctly formatted Pauli answers, at the universal constants of the closed form of the error (MIPRE/Background/Introspection/QLDExtractionAdapter.lean; the conclusion FieldExtraction is in MIPRE/Background/Introspection/BinaryExtraction.lean).

cor:qld-binary: the field-register extraction read on qubits, along a self-dual basis (MIPRE/Background/Introspection/BinaryExtraction.lean).

Declarations added when the chain was restated in a bipartite model

Phase 5 of planning/mipco-track.md, by blueprint node.

lem:ms-direct-anticomm

lem:qld-combined-points

lem:qld-error

lem:qld-exact-paulis

lem:qld-expanded-lines

lem:qld-global-dummy

lem:qld-global-products

lem:qld-global-pvm

lem:qld-global-setup

lem:qld-global-success

lem:qld-obs-commutation-comm

lem:qld-pairs-of-lines

lem:qld-padded-lines

lem:qld-pauli-selfcons

lem:qld-simultaneous

lem:qld-swap

lem:qld-win