3 Background results

This chapter collects theorems that the proof relies on but whose proofs appear in other papers. Each entry gives a full statement, a pointer to the literature, and comments on its role and on formalization. The project may initially assume these as axioms; discharging them are independent sub-projects. Three of these results are larger sub-projects and are developed in their own sections: the computability results in Section 4 and parallel repetition in Section 5; they are included in the summary table below for completeness. Statements are given in the form closest to how they will be used. The compression pipeline carries bipartite soundness in \(\mathrm{val}^*\); synchronous and tracial results appear as internal ingredients with their own transfer obligations.

Each entry carries an estimate of the formalization effort: [\(\bullet \) easy] for self-contained arguments of at most a few pages, [\(\bullet \bullet \) medium] for substantial but well-delimited developments, and [\(\bullet \bullet \bullet \) hard] for results whose formalization is a project in itself; [\(\checkmark \) (mostly) in Mathlib] marks statements essentially available in Mathlib. The estimates are for the statement as it will be used (including any required interface translation) and are of course provisional. Independently of the effort estimate, the [\(\uparrow \) QuantumLib] badge (introduced in Section 2) marks results of general quantum-information interest that are intended to be upstreamed to QuantumLib.

The anchored parallel repetition theorem of  [ 10 ] , and the entropy and fidelity toolkit its proof needs, are not on the path to the main theorem and are not stated in this blueprint (Remark 5.11).

3.1 The Gowers–Hatami theorem

[\(\uparrow \) QuantumLib]

Source.

Gowers and Hatami  [ 7 ] . A quantitative form suited to applications in nonlocal games, and a version adapted to the tracial setting, is given by de la Salle  [ 8 ] and in  [ 9 ] .

Comments.

This is the stability result underlying all rigidity (self-testing) arguments in the proof: an approximate representation of the Pauli group \(\mathbb {F}_2^{2k}\) (with its cocycle) is close to an exact one, which forces the presence of EPR pairs. The statement above is fully formalized (statement and proof) in MIPRE/Background/GowersHatami/Basic.lean, following the regular-representation argument sketched in the proof; the intermediate statement, with the exact representation living on the concrete index set \(G \times \{ 1, \dots , d\} \), is MIPRE.gowers_hatami_prod. Two remarks on the statement. (i) It asserts only \(d' \geq d\), with witness \(d' = |G| d\); it does not include the dimension bound \(d' \leq (1 + C\varepsilon ) d\) of  [ 7 ] , whose proof goes through the Fourier-analytic route via irreducible representations. Whether the sharper bound is needed downstream (in the Pauli-group application feeding Theorem 3.38) is to be revisited; if so it will be added as a separate strengthening. (ii) In the Lean encoding the isometry is stored as the \(d \times d'\) matrix of its adjoint, so the isometry condition reads \(V V^\dagger = I\) and the compression is written \(V \rho (x) V^\dagger \). The normalized Hilbert–Schmidt norm is the tracial form needed for the synchronous framework  [ 8 , 9 ] .

3.2 Almost-synchronous correlations

[\(\bullet \bullet \bullet \) hard] [\(\uparrow \) QuantumLib]

Source.

Vidick  [ 9 ] , building on  [ 20 , 21 ] ; the statement above is the corollary needed here, with constants independent of the game’s size. What the source controls is not the game’s value directly but the synchronicity defect of a strategy — its inconsistency (Definition 2.37) at equal questions, taken against the common marginal \(\nu \); the two-sided correlation replacement uses that common marginal. The diagonal-weight hypothesis is what turns the game’s rejection probability \(\varepsilon \) into the bound \(\varepsilon /\kappa \) on that defect, the pairs \((x,x)\) carrying at least a \(\kappa \) fraction of the weight of \(x\). Without it the two values are unrelated (Remark 3.4).

Comments.

The proof uses the orthonormalization lemma (Section 3.3) and a rounding argument. Used contrapositively, the theorem turns a bound \(\mathrm{val}^{s}(\mathfrak {G}) \leq 1 - \delta \) into \(\mathrm{val}^*(\mathfrak {G}) \leq 1 - \Omega (\kappa \delta ^{1/c})\): the diagonal weight multiplies the gap recovered, so a small \(\kappa \) is a loss. The hypothesis is also not preserved by repetition. The pipeline instead carries soundness in \(\mathrm{val}^*\) throughout and uses direct bipartite repetition.

3.3 The orthonormalization lemma

[\(\bullet \bullet \) medium] [\(\uparrow \) QuantumLib]

Source.

de la Salle  [ 8 ] , which gives a dimension-free bound with explicit constants; earlier versions with worse parameters appear in  [ 20 ] and in  [ 1 ] . The Lean proof is vendored from the orthogonalization package of the commuting-repetition repository (the same upstream as Theorem 5.5) by scripts/vendor-repetition.py; see that directory’s README.md for what the copy changes (import prefixes, nothing else).

Comments.

Used constantly: soundness analyses produce POVMs that are only approximately projective, and this lemma replaces them by genuinely projective measurements on the same space, which is what makes the “projective strategies throughout” convention of Section 1.3 viable (avoiding Naimark dilation). The finite-dimensional case suffices for the main theorem and is a clean, self-contained formalization target in linear algebra.

The first of the two claims about the source made by the verification campaign  [ 33 ] — that this statement was over-hypothesized, the result needing only a normal state rather than a normal faithful tracial one, with constant \(9\) and exponent \(1\) — is now settled in the direction the campaign predicted, and settled by proof rather than by reading: the statement above carries neither faithfulness nor traciality and is checked. That matters beyond bookkeeping, because the tracial hypothesis excluded the bipartite vector-state applications that several of the projectivization sites of Section 6 need; those sites can now use this lemma, where before they needed Naimark dilation or the projective-by-definition convention of Section 1.3. What is settled is the mathematics, not the attribution: the campaign’s second claim, that crediting the weaker predecessor to  [ 20 ] and  [ 1 ] is wrong and the source credits the low individual degree paper and Kempe–Vidick instead, is still unchecked here, [ 8 ] not being vendored in this repository. The campaign also offers a consistency-to-projectivity step giving \(O(\delta )\) in place of \(O(\delta ^{1/4})\), which would sharpen the proof of Theorem 3.3.

The formalized hypothesis and conclusion are both strict. For a POVM, completeness identifies the defect with \(1-\varphi (\sum _a M_a^2)\), but does not turn a non-strict bound into a strict one. A compactness argument in finite dimension would retain the constant \(9\) at the non-strict bound — apply the theorem at every larger error, then pass to a convergent subsequence of projective measurements and use continuity — and would also cover zero defect. Corollary 3.45, the one application in this chapter, does not need it: its Cauchy–Schwarz step produces slack \(\gamma ^2\) over the bound it has to clear, so the strict hypothesis holds as stated. The comments after that corollary record the repair. That corollary is no longer on the formalized route: the analysis of the Pauli basis test is stated for projective strategies in a bipartite model, whose measurements need no orthonormalization, so nothing outside the vendored tree applies this theorem at present.

For the commuting-operator track this repository adds the fourth case of Remark 3.6: algebras without abelian projections, factor or not.

3.4 Magic Square rigidity

[\(\bullet \) easy] [\(\uparrow \) QuantumLib]

Source.

Wu, Bancal, McKague and Scarani  [ 14 ] ; the game is the Mermin–Peres magic square. The form above is  [ 1 , Section 8 ] .

[\(\bullet \bullet \) medium]

Comments.

This lemma is why Theorem 3.9 is no longer an assumption of this blueprint (Remark 3.81). Full two-EPR self-testing is strictly stronger and is not proved by this route — but the pipeline never needed it: what the Pauli basis test consumes is one anticommutation bound on the original observables, and the argument above delivers it from the game alone, with an explicit constant and without any of the structural hypotheses rigidity would impose. For a formalization this is a much better target than Theorem 3.9: the ingredients are the projectivity of one player’s measurements, a telescoping substitution bound, and one six-step word identity in a group generated by nine reflections with six relations.

One player is projective, which is a choice, not a correction. An earlier statement here, following the paper, allowed arbitrary POVM families on both sides, and its proof dilated the constraint measurements to projective ones on one ancilla shared by the six constraints (Lemma 2.30). The formalization is now stated in a bipartite model, where every strategy of the Pauli basis test is projective from the start (Definition 8.62), and Lemma 3.46, the one consumer, applies the bound with the constraint player projective; so the repaired measurement is used as it is, on the model’s own state, and the dilation has no consumer. The POVM form would follow from the projective one by dilating the constraint player alone on a one-sided ancilla extension (Definition 8.75, Lemma 8.77), which changes neither the other player’s observables nor their norms on the state; that step is not formalized. The paper was not consulted for this revision.

Comments.

The direct bound is the elementary anticommutation input that the Pauli test amplifies to many qubits. Its bipartite form already matches the soundness proof’s use; a tracial specialization is optional and is not an additional pipeline prerequisite.

One clause moved out of the statement. An earlier revision also asserted the transfer to the point observables of the Pauli basis test: if \(P, Q\) have cross-party consistency errors \(s_X, s_Z\) against \(B_1, B_5\) then \(\left\| {\{ P,Q\} |\psi \rangle } \right\| \leq 2 s_X + 2 s_Z + \left\| {\{ B_1,B_5\} |\psi \rangle } \right\| \). That is not a statement about the Magic Square game at all — \(P\) and \(Q\) are the Pauli test’s observables — so it belongs to Lemma 3.46, which is where it is used, and it is stated there. The argument is two substitutions across the parties: \(P\) and \(Q\) sit on one factor and \(B_1, B_5\) on the other, so \(PQ|\psi \rangle \approx _{s_Z} P B_5 |\psi \rangle = B_5 P |\psi \rangle \approx _{s_X} B_5 B_1 |\psi \rangle \), and symmetrically for \(QP\).

The game this lemma is about is the one of Definition 2.17 at the magic square’s layout, and that definition is symmetric in the players: an equation, a variable of it, and a uniform orientation, so \(36\) equiprobable oriented incidences. That is what makes the statement’s Alice half expressible at all — a one-directional game would never send Alice a variable, so \(A^{\textsc{Variable}_j}\) would not exist — and it is where the constant comes from: \(\sum _{c,j} \ell _{c,j} \leq 36\varepsilon \) gives \(\gamma ^2 \leq 144\varepsilon \) and \(36^2 \cdot 144 = 186624\), the paper’s constant. An earlier revision of the formalization had the one-directional game, where the same argument gives \(18\varepsilon \), \(\gamma ^2 \leq 72\varepsilon \) and \(36^2 \cdot 72 = 93312\, \varepsilon \); either serves Lemma 3.46, which needs only \(O(\varepsilon )\), but the game and the constant must match.

3.5 The classical low individual degree test

[\(\bullet \bullet \bullet \) hard]

Comments.

This is Figure 1 of  [ 2 ] . The direction \(v\) of the diagonal lines test may be zero, in which case the “line” is the single point \(u\); this degenerate case is part of the test as stated. In the formalization, line questions are the lines themselves, presented canonically (the direction is rescaled so that its first nonzero coordinate is \(1\), and the base point is the point of the line whose corresponding coordinate vanishes), so that the same line asked by two sub-tests is the same question; a line answer is a polynomial in the parameter of that canonical parametrization.

Source.

Ji, Natarajan, Vidick, Wright and Yuen  [ 2 ] , Theorem 1.3 (the formal version for general, not necessarily symmetric, strategies). The proof is a formalization by Sirui Lu and collaborators (https://github.com/LionSR/MIPStarRE), vendored into this repository with the authors’ permission at MIPRE/Background/LIDT/MIPStarRE/; the statement above is this project’s own, and is connected to theirs by an explicit bridge.

Comments.

Two hypotheses correct the printed statement, as established by that formalization: the sampling parameter satisfies \(k \geq 400md\) where the paper prints \(k \geq md\), and \(k\) must be positive, since the printed error vanishes at \(k = 0\). The parameter \(k\) remains free: the error carries both a factor \(k^2\) and a term \(e^{-k/(2560000m^2)}\). A chosen-\(k\) corollary in the shape of \(\delta _{qld}\) below is a separate quantitative derivation; it is not part of the displayed Lean theorem.

The paper’s seeded CL test and its tensor-code route

The following is the paper’s route to a different game interface. Its tensor-code reduction and reviewed intermediate statements are not the proof of Theorem 3.12, and have no Lean proof marks here. The seeded game and its theorem are in the pinned paper snapshot  [ 34 ] , ldt.tex, Definition of the game and Theorem lem:ld-soundness.

The single-codeword case of the seeded theorem is proved here, by a different route: an explicit adapter to the canonical-line test, Theorem 3.19 below. It certifies none of the paper’s intermediate statements, and they certify none of it.

Comments.

The formalization is MIPRE.LIDT.CL.clGame (MIPRE/Background/LIDT/CLGame.lean), beside the canonical-line game MIPRE.LIDT.lidtGame of Definition 3.11 whose soundness is proved; keeping both in one vocabulary is what makes Remark 3.15’s adapter expressible at all. Three points.

The base point of a line question is the canonical representative \(L^{\mathrm{Ln}}_w(u)\) of Definition 6.2 — the canonical linear map with kernel \(\mathrm{span}\{ w\} \) — which is why that vocabulary had to come first. The seed function \(\chi \) is the paper’s eq:chi-func, \(0\)-indexed: under the fixed bijection \(\mathbb {F}_q \cong \{ 0, \ldots , q-1\} \), \(\chi (s)\) is the block of \(q/m\) elements that \(s\) falls into, and \(m \mid q\) is where it is used.

The seeding is not cosmetic, and aline_question_ne records it: two seeds in the same block give the same base point and the same direction, hence the same geometric line, and yet are different questions. A strategy may answer them differently, which is exactly the obligation Lemma 3.20 discharges by choosing a seed in each fibre.

The format check is not decoration, and the formalization now separates it from the subtests (Question.fmtOk and subtests, with accepts their conjunction). Two clauses of fig:ld-decider look alike and are opposite: an answer whose format does not match its question’s type is rejected (“If the answers returned by the players do not fit this format the decision procedure rejects”), whereas a well-formatted answer on one of the two cross type pairs is accepted (“in all cases where no action is indicated, accept”). An earlier version of clGame collapsed both into one catch-all that accepted, which made the test vacuous: the constant strategy answering a point-format answer to every question, the two line types included, passes every subtest, so the game has a value-\(1\) strategy whose point measurements are an arbitrary function of the point, and Theorem 3.14 is false for it. That defect and its repair are recorded in reports/clgame-format-check-missing.md; the statement of this definition was correct throughout, which is why the repair changes only the Lean and this paragraph.

Where fig:ld-decider says “\(t \in \mathbb {F}_q\) is such that \(x = u_0 + tw\)”, the point may fail to lie on the line and the condition is then vacuous. The formalization requires membership, as the canonical-line game already does: the two readings agree on the support of the question distribution, and following the convention of the test whose soundness is proved is what keeps the two comparable. The distribution itself is uniform over the nine ordered type pairs and the ambient \((u, s, v)\), so normalization is a single division rather than the per-subtest bookkeeping Definition 3.11 needs.

Each \(\chi \)-fibre has exactly \(q/m\) seeds (card_chi_fiber), so a uniform seed gives a uniform direction index and the induced axis-parallel line distribution is uniform over lines. This is the hypothesis \(m \mid q\) earning its place, and it is the input Lemma 3.21 consumes.

The canonical-line route, and what it certifies.

The adapter and the parameter corollary the remark calls for are built, and the single-codeword case of Theorem 3.14 follows from Theorem 3.12 — which this project has — rather than from the tensor code test, which it does not. planning/lidt-cl-adapter.md records the design, including two corrections found while proving it.

One structural remark before the statements. The canonical-line test’s only same-type subtest is point self-consistency, so a pair of two line questions carries no weight on that side and no line-synchronicity transfer is needed: no Lemma 3.22, no Schwartz–Zippel, and no \(d/q\) term from that source. The paper’s route needs them because the tensor code test has a line synchronicity condition. A \(d/q\) term still appears in \(\delta _{\mathrm{CL}}\), from the canonical-line theorem’s own error.

[\(\bullet \bullet \) medium]

[\(\bullet \bullet \bullet \) hard]

[\(\bullet \bullet \) medium]

[\(\bullet \bullet \) medium]

[\(\bullet \bullet \bullet \) hard]

[\(\bullet \bullet \bullet \) hard]

[\(\bullet \bullet \bullet \) hard]

[\(\bullet \bullet \bullet \) hard]

[\(\bullet \bullet \bullet \) hard]

Comments.

The algebra of coefficient vectors that this lemma shares with the Pauli basis test is in MIPRE/Background/LIDT/Coefficients.lean, below both: the polynomial a coefficient vector denotes (LowIndDegPoly.toMv), Schwartz–Zippel for a nonzero coefficient vector (card_eval_eq_zero_le), and the coefficient of a monomial pattern on a set of coordinates as a coefficient vector in the others (LowIndDegPoly.coef, with the decomposition eval_eq_sum_coef). This lemma uses the first two, and stage 4 of the Pauli basis test uses all three, from Lemma 3.67 on. They are listed here, the lowest of their consumers in the dependency graph, so that every other consumer cites a node it depends on.

3.6 The quantum low individual degree test

[\(\bullet \bullet \bullet \) hard] [\(\uparrow \) QuantumLib]

The game

Source.

The pinned paper  [ 34 ] , ldt.tex: the type set is eq:pauli-type, the sampling procedure and type graph sec:qld-game and fig:type-graph-pauli, and the decision procedure fig:decider_pauli. No definition of this game appeared in this blueprint before; Theorem 3.38 and Lemma 3.46 were statements about an undefined object, which is why this is the campaign’s first definitional obligation.

Comments.

The formalization is MIPRE.QLD.qldGame (MIPRE/Background/QLD/Game.lean). Five points, four of them the consequences of having a second twenty-six-type game in the same vocabulary as Definition 3.13 rather than a fresh one.

The line and point content is read off the sample by the same functions as the seeded CL test — \(\chi \), \(\pi \), \(L^{\mathrm{Ln}}\), all from Definition 3.13 — and rule 2 calls that test’s decider rather than restating it: lowDeg_eq_cl and lowDeg_eq_cl_dline are the two identities, and they hold by rfl. This is what stage 4 of Remark 3.41 needs in order to feed Theorem 3.14 at all, and getting it by sharing definitions rather than by a translation lemma is the reason Definition 3.13 was written first.

The Magic Square indices are the layout’s own, \(0\)-indexed (MIPRE.LCS.MagicSquare.layout), against the paper’s \(1\)-indexed \(\mathtt{Constraint}_1, \ldots , \mathtt{Constraint}_6\) and \(\mathtt{Variable}_1, \ldots , \mathtt{Variable}_9\). The paper’s distinguished pairs \((\mathtt{Point}, X)\)–\(\mathtt{Variable}_1\) and \((\mathtt{Point}, Z)\)–\(\mathtt{Variable}_5\) are therefore variables \(0\) and \(4\) in the Lean, which are also the two the anticommutator of Lemma 3.10 is taken between — the same two cells, and they have to be, since rule 7 is what transfers that lemma’s conclusion to the point observables.

The format check is separated from the rules for the reason recorded at Definition 3.13: leaving it out made that test vacuous (reports/clgame-format-check-missing.md), and the same error is available here with twenty-six types instead of three. Each of the eight rules accordingly carries an explicit pair of formatted answers it rejects (rejects_*). The four rules gated on \(\gamma \) take the gate as a hypothesis, since each of them by design checks nothing on the other value of \(\gamma \) — that division of labour between the commutation check and the Magic Square is what the gate is for.

The remaining vacuity risk is a rule that is simply missing, so that an edge of \(G^\textsc{Pauli}\) falls through to the catch-all. handled_of_adj closes it by decide: every non-loop edge of the type graph has a rule. Together with the rejection witnesses — one per rule — that says no question pair the distribution asks is accepted regardless of the answers. The converse fails harmlessly: some rules also reject pairs the graph does not contain, such as \((\mathtt{Point}, X)\) against \(\mathtt{Variable}_j\) for \(j \neq 1\).

Finally, the answer alphabet for \(\mathtt{Constraint}_i\) is \(\mathbb {F}_2^3\) and not the full assignment \(\mathbb {F}_2^9\) of Definition 2.17. The two give the same value, the decider reading only the three support coordinates either way, and the full assignment would have been markedly easier to work with; the paper’s format is kept because answer lengths are what the introspection of the compression chapter accounts for, and a game whose answers are six bits too long is a statement about a different verifier.

Source.

The pinned paper  [ 34 ] , qld-appendix.tex and its five proof files, states this Pauli theorem and its reduction to the seeded CL test. The reduction follows the architecture of  [ 1 , Section 7 ] ; the canonical-line soundness theorem of  [ 2 ] is related background. Lemma 3.10 supplies the base anticommutation directly.

Comments.

This is the workhorse of question reduction: introspection certifies the players’ sampling of their own questions against Pauli basis measurements. The paper’s reduction uses direct Magic Square anticommutation, linearity and orthonormalization, together with the seeded CL theorem; the formalized proof invokes neither linearity (Theorem 3.55) nor orthonormalization (Corollary 3.45), its strategies being projective. The dependency graph still draws Theorem 3.55 below it, through matrix-level declarations that Lemma 3.56 lists beside its model form and that share that theorem’s Fourier and ancilla-embedding definitions; soundIn_of_lidt reaches none of them. The available canonical-line theorem can replace the paper’s classical route through Remark 3.15’s adapter, which supplies the \(\mathrm{ldc}=1\) case this reduction uses (Theorem 3.19).

The theorem’s bipartite statement matches the pipeline’s \(\mathrm{val}^*\) soundness interface, so its uses require no additional synchronous-value transport. The verification campaign  [ 33 ] further reports three corrections in the tensor-code material the proof passes through — \(\kappa \)-convexity requires \(c_1 \leq 1\), the synchronicity defect obeys \(\delta _{\mathrm{sync}} \leq 4\varepsilon \) rather than \(3\varepsilon \), and one corner block pairs with a transpose — none affecting the statement above. The formal proof is checked end to end with no assumption beyond Lean’s standard axioms — in the tensor-product model hypothesis (L) is discharged by Lemma 8.66 — so it does not rest on the paper’s account of that material.

The formalization. MIPRE.QLD.soundIn_of_lidt (MIPRE/Background/QLD/Soundness.lean) is the theorem: for a bipartite model \(\cal {M}\) with ordered, proper algebras compatible with the scalars and a value model \(\omega \), the two hypotheses give QLD.SoundIn \(\omega \) \(\cal {M}\) (Definition 8.82). For every field \(\mathbb {F}_q\) of characteristic two, every \(m \geq 1\) with \(m \mid q\), every \(d \geq 1\) and every projective strategy in \(\cal {M}\) failing with probability at most \(\varepsilon \), it provides an extraction (QLD.Extraction) at error qldErr (Lemma 3.78): an ancilla model, which \(\omega \) dominates, a local isometry of \(\cal {M}\) into its register model, the state error, and both players’ summed squared errors for both bases. Its tensor-product instance (soundIn_tensor) and its commuting-operator instance (soundCo_of_lidt) are recorded in Chapter 8, as Lemmas 8.83 and 8.99, where their consumers are. Four points of the statement are worth knowing, the first two of them differences from the paper’s.

• The strategy is projective, in a model. The paper states the theorem for POVM strategies on a tensor product of finite-dimensional spaces; here it is about the projective strategies of a bipartite model satisfying the two hypotheses. The restriction is deliberate. The matrix theorem this replaces did cover POVM strategies, by dilating the strategy to a projective one, running the chain on the dilation and carrying item 2 back down to the original POVM through its agreement with \(\tau ^W\) on the other half of the pair, at a cost of \(8\sqrt{\eta }\) for item 1’s bound \(\eta \). That descent was specific to matrices, and its one consumer, introspection, applies the theorem to projective strategies only (Lemma 6.115); so the POVM form is not restated. This is a choice of the formalization, not a discrepancy with the paper, which was not consulted for this revision.

• The conclusion is a local isometry of models into the register model of an ancilla model, in place of a pair of isometries \(\phi _\textsc{A}\otimes \phi _\textsc{B}\) into \(\mathcal{H}' \otimes (\mathbb {C}^q)^{\otimes M}\) and a state \(|\textsc{aux}\rangle \). The players’ operators move by its homomorphisms, as \(X \mapsto \phi _\textsc{A}X \phi _\textsc{A}^\dagger \) does, and the errors are the model’s state norms; in the tensor-product model the two forms coincide (Lemma 8.83).

• It asks less than admissibility: characteristic two, \(m \mid q\) and \(d \geq 1\). The regime where the chain runs is \(48md \leq q\) rather than the paper’s \(16md \leq q\), \(48\) being where Lemma 3.70 is formalized; the regime and the divisibility \(4m \mid q\) are discharged inside the proof, not assumed (Lemma 3.64), and outside the regime the error absorbs the trivial bound (Lemma 3.78), as the paper’s own enlargement of \(a\) does.

• Item 2 is about the strategy’s Pauli measurement read as cube data, (S.PA (.pauli W)).map rdPauliVec, which puts every malformed Pauli answer at \(h = 0\), as the game’s reading does. The paper assumes well-formatted answers; this is a relabelling of outcomes, not a restriction, and it is why legalizing the strategy is free (rdPauliVec_legalize_pauli). Read at the genuine answers instead, item 2 is Corollary 3.39.

Inside the regime the proof is exists_extraction_of_regime: the extraction is the swap isometry MirrorSimul.swapPhi at the MirrorSimul that exists_mirrorSimul builds for the legalized strategy (legalStrat), with the padded extension in the swap lemma’s auxiliary state as its ancilla model. Outside it the proof is Extraction.trivial. Nothing follows the swap isometry, so the matrix route’s explicit embedding of the strategy’s space into the physical state, its descent from the dilation, and its reading of the isometries with the register first are all gone.

The error the proof produces, qldErr, and its closed form are Lemma 3.78, which rests on the chain’s constants alone; QLD.SoundIn is stated at that function.

The ledger node \(1.2.2\) also records completeness of the game. That is Lemma 6.110, formalized separately; this theorem is the soundness half, node \(1.2.2.17\)’s assembly.

A property of the shape itself. Because of the \(2^{-bmd}\) term the right-hand side never falls below \(a \cdot 2^{-bmd}\), so for any bound on \(md\) the theorem is satisfied trivially by a large enough \(a\), the conclusions being about unit vectors and projective measurements. The statement has content only as \(md\) grows, with \(\varepsilon \) small and \(q\) large. That is inherent in the stated form, not a defect of the formalization, but it is worth knowing when reading the constants the proof produces.

Comments.

The paper’s game has no other answers to a \((\textsc{Pauli}, W)\) question; the formal game has one answer type for all questions, and Theorem 3.38 reads every answer that is not a Pauli answer as the outcome \(0\), as the game does. The introspection consumer (Lemma 6.111) sums over the valid answers only, and this corollary is the bridge, in MIPRE/Background/Introspection/QLDExtractionAdapter.lean. FieldExtraction (MIPRE/Background/Introspection/BinaryExtraction.lean) is the conclusion at the genuine answers: the ancilla model, the local isometry, the state error, and the two estimates introspection uses, the first player’s \(X\) and the second player’s \(Z\). FieldExtraction.ofQLD reads an extraction of Theorem 3.38 there under the support hypothesis (PauliSupported, through rdPauliVec_op_of_supported), fieldExtraction_exists is the corollary, and degreeOne_fieldExtraction_exists is its case \(d = 1\), at the error the canonical parameter estimates use.

It costs nothing. The matrix corollary this replaces assumed only that the two Pauli measurements were projective, and paid at \(h = 0\): the answer \(0\) is one element of everything the game reads as \(0\), so the triangle inequality cost twice the weight of the rank-one projector \(\tau ^W_0\) on \(|\textsc{EPR}_q\rangle ^{\otimes M} \otimes |\textsc{aux}\rangle \), at most \(1/q\), and the error became \(2\delta _{qld} + 8/q\). The support hypothesis removes the malformed answers instead, so the fibre at \(0\) is the answer \(0\) alone. It is free where the corollary is used: the decoder of the introspection game leaves only genuine full-register answers at the Pauli questions (ParsedPauliSupported), and the restriction to the Pauli basis test keeps that (completePauliPOVM_invalid_of_supported). The universal constants are fixed once (qldCoefficient, qldExponent), from the closed form exists_qldErr_le of the error (Lemma 3.78), a fact about that function alone, so they are the same in every model (qldErr_le_errShape).

Comments.

The paper’s cor:pauli-binary (ldt.tex), and the form the binary introspection game consumes (Lemma 6.115). FieldExtraction.toBinary (MIPRE/Background/Introspection/BinaryExtraction.lean) composes the extraction’s local isometry with the relabelling of the register along the binary basis (BipartiteModel.regRelabel), and binaryX and binaryZ identify the relabelled honest projectors. Its conclusion is Extraction (MIPRE/Background/Introspection/RestrictedSoundness.lean), the extraction in binary coordinates, whose two estimates read the strategy’s measurements at validAnswer \(x\), the Pauli answer \(\phi ^{-1}(x)\), which the binary game’s reading of answers takes back to \(x\) (project_validAnswer). Like Corollary 3.39 it carries the first player’s \(X\) estimate and the second player’s \(Z\) estimate, the two introspection uses; the matrix form, which covered both players and both bases for an arbitrary relabelling of the register, was removed with the matrix theorem.

The shape of the soundness proof

Preliminaries

[\(\bullet \bullet \) medium]

Comments.

Two departures from the paper’s statement and proof, both recorded in the formalization’s own docstring. First, the paper states the bound as \((1 - q^{-m})(1 - q^{-1})(1 - md/q)/2\); its own correction note removes the case distinction on \(u_X = 0\) that produced the first factor, observing that \(\mathrm{ind}_m(u_X)\) is never the zero vector, and keeps the factor only because it remains a valid lower bound. It is dropped here. Second, the low-degree encoding is multilinear, so Schwartz–Zippel costs \(m/q\) and not \(md/q\); the formalized bounds are \((1 - (m+1)/q)/2\) and \((1 - 1/q)/2\), and the paper’s \((1 - 3md/q)/2\) is derived from them for \(m, d \geq 1\). The ‘\(d\)’ in this fact is therefore inert: it is the individual-degree parameter of the surrounding test, and the bound does not depend on it.

The complementarity statement is not decoration. Each of the two bounds is a lower bound on a probability, so either alone would be implied by the wrong definition of its event; that they hold for complementary events, and add to one, is what pins them down.

[\(\bullet \) easy]

[\(\bullet \) easy]

[\(\bullet \bullet \) medium]

Comments.

The paper closes this proof differently, and the difference is a repair. It derives near-projectivity at \(2\gamma \) for the actual inconsistency \(\gamma \), which is non-strict, so Theorem 3.5 applies only at each \(\varepsilon {\gt} 2\gamma \); it then takes \(\varepsilon \downarrow 2\gamma \) inside the (compact) set of projective measurements with a fixed finite outcome set and extracts a convergent subsequence to reach \(18\gamma \) itself. That limit is not needed. The slack \(\gamma ^2\) in \((1-\gamma )^2 = 1 - 2\gamma + \gamma ^2\) already makes the hypothesis strict at \(\varepsilon = 2\delta \) for any bound \(\delta {\gt} 0\) on the inconsistency, which is the form in which every application supplies it and the form stated above; the compactness argument, and with it the continuity of \(\{ P_a\} \mapsto \sum _a \left\| {((Q_a - P_a)\otimes I)|\psi \rangle } \right\| ^2\) and the sequential extraction, disappears. What the paper’s version additionally gives is the exact case \(\delta = 0\), where the limit produces a projective measurement agreeing with \(\{ Q_a\} \) on \(|\psi \rangle \) exactly. Nothing downstream uses it: every invocation carries a positive error bound. The statement above is therefore weaker only at \(\delta = 0\) and stronger elsewhere, both in being strict and in naming the constant.

Not formalized, and off the formalized route. This corollary was formalized for matrices (exists_projective_of_consistent, through Theorem 3.5), and the formalization was removed when the analysis of the Pauli basis test was restated in a bipartite model: a strategy there is projective from the start (Definition 8.62), and its one consumer, the commuting case of Lemma 3.48, now uses the strategy’s own projective \(\mathtt{Pair}\) measurement (Lemma 3.49). It is kept as the paper’s statement, with the repair above, and carries no formalization marks.

What winning implies

[\(\bullet \bullet \bullet \) hard]

Comments.

Four departures from the paper’s statement ( [ 34 ] , qld-commutation.tex, lem:qld-win-implications), and one from this blueprint’s own earlier text.

The paper’s hypothesis \(6md \leq q\) is not needed and is dropped. It is there to turn the gated items into averages conditioned on \(\gamma \): by Lemma 3.42 each of the two events has probability at least \((1 - 3md/q)/2 \geq 1/4\) under it, so dividing by that probability costs a factor \(4\). The formalization states the gated items in the unconditional form, with the gate’s indicator inside the average, which needs no lower bound on the gate’s probability and is what the machinery produces directly. Whoever needs the conditional form divides, and pays \(6md \leq q\) there.

The constants are named rather than hidden in \(O(\varepsilon )\). They are \(172 = 2 \cdot 86\) for the consistency items — the factor \(2\) of 1 and the selection probability \(1/86\) — and \(16049664 = 186624 \cdot 86\) for the anticommutator. Item 6 in the paper reads \(\mathop{\mathbb {E}}\Lambda _\omega = 1 - O(\varepsilon )\); that intermediate form is one_sub_povmValue_ms_le together with sum_msEps_le, and the item above states the composition with Lemma 3.10 because that is what the expansion stage consumes.

That composition asks the first player’s measurements to be projective, where the paper’s strategy is arbitrary: it inherits the hypothesis of Lemma 3.10, which is stated with the constraint player projective, and whose comments say why. The strategies the later stages apply it to are projective in both players (Definition 8.62), so nothing downstream pays for it; the other six items hold for arbitrary POVM families.

The paper’s item 2 quantifies over the line–point distribution of a separate definition; here it is the two line types of Definition 3.37 separately, at the questions the content actually produces, which is the form Definition 3.13’s own decider is stated in and avoids a second distribution.

Finally, this blueprint’s earlier statement of this lemma bundled into it the transfer of the anticommutation to the point observables. That is the paper’s separate lem:qld-win-implications-obs, it needs items 4, 5, 6 and 7 together, and it is where the sign \((-1)^{\gamma }\) first appears; it belongs with the expansion stage that consumes it and is not part of this lemma.

The point observables

The stage that follows works with the \(\pm 1\)-observables of the two-outcome probes rather than with the measurements themselves, and needs two statements about them: they are cross-party consistent, and they commute up to the sign \((-1)^{\gamma }\). The first is Lemma 3.46 item 1 and costs one factor of two; the second is the synthesis of items 4 to 7 and is where the sign that Lemma 3.51 cancels first appears.

[\(\bullet \) easy]

[\(\bullet \bullet \bullet \) hard]

[\(\bullet \bullet \) medium]

Comments.

Formalized in MIPRE/Background/QLD/Commutation.lean. One departure from the paper’s route, and two from its bookkeeping, both forced by which side an object lives on.

No orthonormalization. The paper’s strategy is a POVM strategy, and it makes the \(\mathtt{Pair}\) measurement projective with Corollary 3.45, at \(18\) times the inconsistency of the two players’ \(\mathtt{Pair}\) measurements and a factor two per marginal. Here the first player’s measurements are projective, as a strategy of a bipartite model is, and so is the joint \(\mathtt{Pair}\) reading, a coarse-graining of hers (isPVMIn_pairPOVM). The inconsistency term is kept at the weight \(72\) the orthonormalization charged, with its bound sum_incQty_le, so that the constant is the matrix formalization’s, unchanged; the strict positivity the corollary asks of its error bound, and the limit that discharged it in the matrix formalization, are gone.

The analysis is run on Bob’s observables and carried back. Lemma 2.31 wants the two commuting families on one side and the joint projective measurement on the other, and the projective \(\mathtt{Pair}\) measurement is Alice’s. So the analysis is applied to Bob’s point measurements against Alice’s \(\mathtt{Pair}\) measurement, and the conclusion is carried to Alice’s observables by the order-reversal rule. Running it on Alice’s side instead would ask Bob’s measurements to be projective too.

The chain is run in the mirrored orientation. Every rule of fig:decider_pauli is stated in both orientations, so items 5 and 1 are available with the players exchanged and item 4 is used as it stands.

Data processing is a consistency-level fact. The chain’s links are converted to the state-dependent distance only after the coarse-grainings are taken, because \(\approx _\delta \) has no data-processing inequality: NW19’s Fact 4.26 is stated for \(\simeq _\delta \), and the remark following it gives a counterexample for \(\approx _\delta \). The paper’s fact:data-processing is the \(\simeq \) form, correctly; a formalization that reached for the \(\approx \) form would be proving something false.

[\(\bullet \bullet \) medium]

Comments.

Formalized in MIPRE/Background/QLD/Commutation.lean.

This half costs \(\varepsilon \), not \(\sqrt{\varepsilon }\). Every input above is a squared-norm bound linear in \(\varepsilon \), and the only inequalities used are the triangle inequality and \((a+b+c)^2 \leq 3(a^2+b^2+c^2)\), so nothing introduces a square root. Correction to an earlier reading of this: the square root in 13 as the paper writes it does not belong to the commuting case either — that case is \(O(\varepsilon )\) too (Lemma 3.49), since 4 is linear in its hypothesis and the paper’s orthonormalization, Corollary 3.45, is linear in the inconsistency, while the formalization needs no orthonormalization at all. The paper’s \(\sqrt{\varepsilon }\) is a uniform weakening, and its own text says so where the anticommuting case is proved: “direct averaging proves the anticommutation relation with squared error \(O(\varepsilon )\). In particular it implies the following weaker bound, retained in the form used below”. Nothing downstream needs the sharper form — lem:qld-comm-cons asks only for \(\mathrm{poly}(\varepsilon )\) — so this is a note about where a square root is not spent, not a repair.

The sign is the double reversal. Both order reversals run in the same direction — a product transferred across the tensor factors comes back reversed — and what sits between them is Bob’s anticommutator, a sum. So the two reversals do not cancel: Alice’s two observables anticommute because Bob’s do, and that is the \((-1)^{\gamma }\) the expansion stage of Lemma 3.51 cancels against the ancillas.

Expansion: approximate commutation of the two bases

[\(\bullet \bullet \bullet \) hard]

Comments.

Both items are formalized, at \(172\varepsilon \) and \(57676416\varepsilon \); the \(\delta _{\mathrm{acom}} = O(\sqrt{\varepsilon })\) of the statement is a weakening, as it is one step earlier (see Lemma 3.50’s comments). The expansion contributes nothing to either constant, which is the point of Definition 2.29’s items 3 and 4.

Comments.

Formalized in MIPRE/Background/QLD/Expanded.lean. The whole estimate runs on Born probabilities and is converted to the state-dependent distance exactly once, at the end. That is not a stylistic choice: the convolution is a coarse-graining, and \(\approx _\delta \) has no data-processing inequality (Definition 2.29’s comments). So the route through agreement probabilities is the only correct one, and it is also the one that makes the ancilla’s contribution visible as an exact \(1\).

Comments.

Formalized in MIPRE/Background/QLD/Expanded.lean. This is what the expansion exists for, and it is worth saying precisely what is bought: the sign is gone, not smaller. Without the ancillas the two bases commute only up to an error carrying \((-1)^{\gamma (\omega )}\), which no amount of soundness improves, because \(\gamma \) is a property of the question and not of the strategy. With them the two signs multiply to one identically, and the error that remains is the strategy’s own.

The constant carries over unchanged. That is the content of items 3 and 4 of Definition 2.29: the expansion is free, in the sense that no step of it loses anything, which is also why it is stated there rather than here.

[\(\bullet \bullet \bullet \) hard]

Comments.

Formalized in MIPRE/Background/QLD/Expanded.lean, with the restriction operation in MIPRE/Foundations/LowDegree/LineRestrict.lean and the two closure properties of projectivity in MIPRE/Foundations/PVM.lean and MIPRE/Foundations/Expanded.lean.

Three things about the statement have changed against the version this replaces, and all three are improvements rather than paraphrases.

\(\delta _{\mathrm{Line}}\) is linear in \(\varepsilon \), at the constant \(172\varepsilon \) of item 1 of Lemma 3.46, not \(O(\sqrt\varepsilon )\) as this lemma previously claimed. The paper says \(\mathrm{poly}(\varepsilon )\) and is consistent with either; the square root was this blueprint’s own and had no source. Nothing in the proof takes a square root, because nothing in it converts an operator inequality into a norm.

Projectivity does not come from Corollary 3.45, and that reference is gone from the uses list. It comes from projectivity of the strategy’s own line measurement, which the paper takes for granted and which is without loss of generality; the formalized statement carries it as a hypothesis rather than hiding it.

The paper’s two forms of item 2 — comparing a line outcome with a point outcome, and comparing the evaluation of the line polynomial at the point — are one statement here. The paper needs a direct calculation to pass between them, because it works with \(\approx \) and Fact fact:data-processing is a statement about \(\simeq \) (a defect it flags itself). At the Born level the passage is free: summing the line outcomes over a fibre of \(\mathrm{eval}_u\) is a coarse-graining, which increases agreement, so the estimate proved is the stronger one and the weaker follows without a separate argument.

One thing is deliberately not claimed. For an axis-parallel line the honest restriction is affine, hence of degree at most \(d\) rather than \(md\); that refinement is what Lemma 3.58 will need in order to keep the padded answers in the degree-\(d\) format, and it needs the individual-degree bound along the line’s own direction, not the total-degree bound proved here. The convolution above is stated at degree \(md\) for both line types, with the axis-parallel answers padded, which is what the paper’s printed definition does too.

Combining the two bases

The point of this stage is a single measurement that returns the \(X\)-polynomial and the \(Z\)-polynomial at once. It is reached by padding the ambient space from \(\mathbb {F}_q^m\) to \(\mathbb {F}_q^{4m}\), so that a point of the padded space encodes a point in each basis together with a pair of coefficients, and then applying the seeded CL theorem to the padded strategy.

[\(\bullet \bullet \bullet \) hard]

Source and correction.

The paper imports this from Natarajan and Vidick  [ 5 ] (Theorem 10 of the arXiv version) and proves nothing about it; the source is vendored in the paper repository, not in this one. An earlier version of this proof text said “the source is vendored and was audited line by line”, which is true of paper/external/nv17/ and false of MIPRE/Background/, whose vendored trees are GowersHatami, LIDT, Orthonormalization and Repetition. A reader would have planned the wrong work. The theorem is therefore proved here, from Parseval and Lemma 2.30; it is formalized in MIPRE/Foundations/Linearity.lean.

The ledger node this statement accounts for records the paper’s status — imported from NV17, with the import audited in its three children: the statement match, the source’s state-dependent-distance toolkit, and the Fourier proof line by line. The mark here records the Lean’s status, which is a proof. The two are consistent claims about different artifacts, and the Lean proof is the argument the third child audits: the same transform, the same Parseval step, the same dilation, the same inversion.

Comments.

Three things are worth separating from the proof.

Theorem 3.2 is not used, and has left this theorem’s uses list. Gowers–Hatami is a statement about the Hilbert–Schmidt distance and approximate representations; the hypothesis here is in the state-dependent distance, and the exact-POVM step above replaces the stability machinery entirely. The two results are about different things and neither implies the other in the form stated.

The conclusion is an equality, which is more than the paper’s statement and more than the application needs. The paper’s own audit note reconciles its \(\delta \) against NV17’s convention and concludes “the closeness exponent is \(1\), with the identical \(\delta \)”; the equality above says where that comes from — the linearity defect is transported term by term, not estimated.

The ancilla is adjoined to one party. That is the asymmetric extension \(|\psi \rangle \otimes |0\rangle _{\textsc{A}'}\) of the source statement, not the two-sided \(|\textsc{EPR}_q\rangle ^{\otimes M}\) of Definition 2.29; the exactly linear observables act on \(\textsc{A}\textsc{A}'\) and the second party is untouched. Its formalization is extVecA, with the compression identity qform_extVecA the only fact about it the proof needs.

[\(\bullet \bullet \bullet \) hard]

In the remaining combining and separating obligations, cross-party consistency estimates use the outcome-summed squared distance of Definition 2.28. When a proof instead bounds the probability of unequal outcomes, convert using Equation 1 and retain the resulting constant. Same-side operator comparisons use Definition 2.27.

Source and correction.

Formalized in MIPRE/Background/QLD/Combined.lean, with the generic mathematics in MIPRE/Foundations/Sandwich.lean, the Fourier dictionary in MIPRE/Foundations/Parseval.lean and the player exchange in MIPRE/Foundations/Swap.lean and MIPRE/Background/QLD/Swap.lean.

The route differs from the paper’s, and the statement is the same. The paper builds \(\widehat{Q}\) in three steps: the sandwich, then orthonormalization (Corollary 3.45) to make it projective, then the quantum linearity test (Theorem 3.55) to turn the resulting binary observables into an \(\mathbb {F}_q^2\)-valued measurement. Given that the strategy may be taken projective — which the paper also assumes — the last two steps are unnecessary: the sandwich is already a POVM, so its Naimark dilation is already the projective joint measurement wanted, and the compression identity carries the estimates. So thm:linearity has left this lemma’s uses list, together with cor:ortho-from-consistency, which was never in it. Theorem 3.55 is consequently used nowhere in this blueprint — Lemma 3.75 says explicitly that it is not used there either — and is kept because it is a statement of the paper’s and is now proved rather than imported, not because anything downstream needs it.

The extra register is explicit. The paper writes “by assuming that \(|\hat\psi \rangle \) has sufficiently many ancilla zero qubits, we do not need to extend the state further”; here the register the dilation needs, two copies of \(\mathbb {F}_q \times \mathbb {F}_q\), is adjoined to each party by name (the ancilla extension BipartiteModel.jointModel), which is the same device with the bookkeeping visible. It is adjoined to both parties, unlike the one-sided extension of Theorem 3.55, because item 1 compares the two players’ copies of the same construction.

The constants are explicit and linear in the inputs. \(\delta _Q\) has a square root because three of the chain’s five links are Cauchy–Schwarz steps; the \(57676416\varepsilon \) under the first two is Lemma 3.48’s constant, unchanged by the expansion, and the \(86\varepsilon \) under the third and in the linear term is item 1 of Lemma 3.46’s, halved by projectivity. Nothing in the chain is a per-outcome estimate, so no constant depends on \(q\).

[\(\bullet \bullet \bullet \) hard]

Comments.

Proved, exactly and at no cost, by legalizing the strategy first. An earlier version of this paragraph costed the support claim as “coarse-grain the ill-formatted answers into a default outcome and re-derive the two items of Lemma 3.54 for the modified measurement at the cost of the format-failure probability, which is \(O(\varepsilon )\) but changes the constants”. That is one legalization too late. Legalizing the strategy rather than the expanded measurement is where the paper’s own convention lives — a “valid strategy” answers in the prescribed format, which is how qld-combining.tex justifies the axis bound — and it costs nothing: the value does not decrease, projectivity is kept, and the readings are unchanged, so every lemma of this appendix applies to the legalized strategy verbatim and its conclusions about point and Pauli measurements are conclusions about the original. The support claim is then exact — zero mass, not \(O(\varepsilon )\) — and no constant moves. MIPRE/Background/QLD/Legalize.lean is the legalization; the support half sits next to the degree computation in MIPRE/Background/QLD/PaddedLines.lean.

Comments.

Formalized in MIPRE/Background/QLD/Lines.lean, on top of Lemma 2.33 in MIPRE/Foundations/Pasting.lean. The headline declaration qld_pairs_of_lines takes only game-level hypotheses — a strategy, its projectivity, and \(1 - \mathrm{val}\leq \varepsilon \) — and bounds by \(\delta _P\) the probability that the first player’s sandwich and the second player’s \(T\), read at the sampled points, disagree on the register model, at the axis-parallel line of each side. That is 15 in agreement form: \(\widehat{Q}\) compresses to the sandwich, so its Born probabilities against \(T\) on the extended state are the sandwich’s on the register model, and 1 converts. pairs_of_lines_gen and pairs_of_lines state the distance form for the dilated \(\widehat{Q}\) itself. pairs_of_lines_of_items is the agreement form for any pair of presentations, and aPres_items, dPres_items and sum_content_collProb_dPres are what the other three pairs of line types need.

The question distribution is a parameter. pairs_of_lines_gen proves the lemma over any finite nonempty sample space carrying a content per side — \(k_X\) presenting the \(X\) line, \(k_Z\) the \(Z\) line — together with a shift of the \(X\) point that both contents see as such; the two contents need share nothing, because no hypothesis of Lemma 2.33 involves both lines. pairs_of_lines is its instance at one content per sample, the same one on both sides, where the two lines are therefore dependent; pairs_of_lines_prod (Lemma 3.61) is its instance at a pair of line–point data, where they are independent. pasteLine and pasteJ_eq_pasteLine accordingly take the \(X\) line and the \(Z\) line from two contents rather than one.

Per pair of line types, not for the mixture. The paper states the lemma on average over the line–point distribution, which is an equal mixture of the axis-parallel and diagonal branches. Here the line type is a parameter and the statement is proved for each of the four pairs, which is stronger: the mixture is a convex combination of the four.

A degenerate diagonal line makes the collision probability one, and the paper’s \(\varepsilon = md/q\) does not account for it. The seeded test’s diagonal direction is \(\mathtt{zeroBelow}(\chi (s), v)\), which vanishes for a \(1/q\) fraction of the contents at worst; on such a content the “line” is a single point, every polynomial is evaluated at the same parameter, and two distinct ones can agree with probability \(1\). The bound above therefore carries \(md/q + 1/q\) on the diagonal side, and \(\delta _P\) is still \(\mathrm{poly}(\varepsilon , md/q)\). See reports/pasting-degenerate-diagonal-line.md.

The shift replaces the paper’s appeal to lem:alnf and lem:dlnf. Those say that conditioned on the line the point is uniform on it, which is what the collision bound uses. Rather than form the conditional distribution, the formalization shifts the point along the direction and uses that the shift is a bijection of contents for each fixed \(t\) (sum_content_shift_gen); the same device, applied to the raw direction \(v\) instead of the point, is what bounds the probability of a degenerate diagonal line.

What the refined contract still asks for. Three items of the contract recorded for this lemma are not part of what is proved above, and are wanted by the lemmas that consume it: that the outcome polynomials have degree at most \(d\) on an axis-parallel component, which is Lemma 3.57 and an additional target there; and the restriction to specified line types and direction indices, which costs the reciprocal probability of those choices, at most \(4m^2\). That the two lines be drawn independently is no longer one of them: pairs_of_lines_gen leaves the question distribution free, so the padded line–point distribution of Lemma 3.61 is an instance rather than a gap. The version above fixes the line type on each side as a parameter and is proved for each of the four pairs, so the restriction factor is not incurred; the reciprocal cost appears only when a caller wants the statement for the mixture.

[\(\bullet \bullet \) medium]

Comments.

Formalized in MIPRE/Background/QLD/Combined.lean, with Parseval over one and two copies of the field and the coarse-graining identity in MIPRE/Foundations/Parseval.lean and MIPRE/Foundations/Sandwich.lean.

The error is improved, not merely preserved: item 2 comes out at \(\tfrac {q-1}{q}\) times the input, so the factor is below one and there is no \(md/q\) term. That is the paper’s round-12 repair of this step, and the ledger node records it: an earlier orthogonality-and-Cauchy–Schwarz route claimed \(O(\delta _Q^{1/2})\) and was retracted, every direct route paying the fibre multiplicity \(q\). The Lean statement keeps the factor visible rather than absorbing it.

Item 1 holds for every \((\alpha , \beta )\), not only on average, because nothing in its proof averages over the probes — the coarse-graining is free pointwise. Only item 2 needs the \((\alpha ,\beta )\)-average, and it needs it for the bijection \((\alpha , \beta ) \mapsto (r\alpha , r\beta )\).

[\(\bullet \bullet \) medium]

Comments.

Formalized in MIPRE/Background/QLD/Padded.lean, on the block identities of MIPRE/Foundations/Blocks.lean.

The construction. LPData is the triple \((u, s, v)\) a seeded line–point pair is generated from, in either dimension; subX and subZ are the sampling procedure, reading the two \(m\)-dimensional pairs off a padded one together with a fresh seed and raw direction per side. padCase is the four-way case distinction, and seedIn is the retargeting of a seed to a prescribed block keeping its offset — the paper’s “choose \(s_X\) uniformly at random subject to \(\chi (s_X) = i\)”, made a function so that the construction is a function of its randomness rather than a conditional distribution.

The containment is xBlk_dir_sub and zBlk_dir_sub, which say that in each case the relevant block of the padded direction either is the subline’s direction or vanishes, and xBlk_on_subX / zBlk_on_subZ, which turn that into \(u_X \in \ell _X\) and \(u_Z \in \ell _Z\).

The law is stated as four identities, one per case, and they are identities of averages rather than of sums: avgSub_free, avgSub_zc, avgSub_xc and avgSub_xc_dline each say that the average over the sampling space equals the average over a product of two line–point laws, restricted on a side exactly when that side is forced. No constant survives; the multiplicities — the assignments to the coordinates and the fresh randomness the construction does not read — are what the normalization divides out, and they differ from case to case, which is why the four are separate statements. sumAll_eq_sum_sumRestr is the mixture: the unrestricted law is the sum of the \(m\) restricted ones, so a side that is not forced contributes a uniform mixture.

Property 1 is definitional and Property 3 is definitional, for the same reason: the padded line–point pair is an input the construction does not modify, and the line type is a parameter handed to both sides. subX_question_aline and subZ_question_aline record the second of these.

Why \(4m\). \(\alpha \) and \(\beta \) sit at positions \(2m\) and \(2m+1\), so the dummy block is the \(2m-2\) positions above them and every index bound needs only \(m \geq 1\). The asymmetry between the two sides in the diagonal case is what the paper’s round-12 note on this lemma repairs: the missing primes on \(w_X, w_Z\), and the unspecified law of the coordinate registers \(s_X, s_Z\).

[\(\bullet \bullet \bullet \) hard]

Comments.

The statement and its proof are formalized; the consistency bound \(\delta _{\mathrm{combine}}\) was the last piece to close. Everything the statement asserts about the measurement is formalized — the combining map, its two degree bounds, the POVM \(\widehat Q^\ell \) itself and the coarse-graining that turns it into an \(\mathbb {F}_q\)-valued outcome — in MIPRE/Background/QLD/Combine.lean, on top of the transfer in MIPRE/Background/QLD/Product.lean. The transfer is worth separating from the rest because it is where an apparent obstruction turns out not to be one.

The obstruction, and why it is not one. Lemma 3.58 is proved on the Pauli basis test’s own question distribution: one content, carrying both sides’ points but a single seed and a single raw direction, so the \(X\) line and the \(Z\) line it presents are not independent. This lemma needs the same conclusion on a product of two independent line–point laws, which is what Lemma 3.60 delivers. The two distributions are genuinely different — but no hypothesis of the pasting lemma involves both lines. Each marginal consistency involves one line and the two points; the fine self-consistency and the collision term involve one line only. So the only laws that have to agree are one side’s line–point data on its own, one side’s data together with the other side’s point, and the two points; and each of those has the same law under a content as under a product, because a content’s two points and its seed and raw direction are independent and uniform. avg_content_eq_pair_X, avg_content_eq_pair_Z and avg_content_eq_pair_pts are those three identities, each one line on top of avg_comp_equiv_fst: exhibit the splitting of each sample space that isolates the part the quantity depends on, and the marginals match.

The change of variables generalizes for free. The device that makes the point uniform on its line without forming a conditional distribution needs a finite nonempty sample space, a shift action, and a direction the shift does not move — nothing about contents. bijective_shift and sum_shift_gen are that statement, and sum_pair_shift is its instance at a pair with the shift acting on the \(X\) side only.

The combining map, and where its whole geometry sits. combine is built through Mathlib’s Polynomial and truncated back to a coefficient vector: it is \(\alpha (t) f_X(x(t)) + \beta (t) f_Z(z(t))\) with all four substitutions affine in the padded parameter \(t\), so the degree bound \(md+1\) is a product of degrees and nothing more. eval_padCombine is the paper’s parametrization-free defining property: at the padded parameter \(t\) the combined polynomial takes the value \(\alpha \cdot f_X(x) + \beta \cdot f_Z(z)\) at the corresponding point, each side’s polynomial read at the parameter of its own subline.

The only geometric input is xBlk_dir_sub and its \(Z\) twin (Lemma 3.60): the \(X\) block of the padded direction is either the \(X\) subline’s own direction or zero. In the first case the subline parameter moves by exactly the padded shift, in the second it does not move at all — so in both it is \(p_0 + c\, t\) with \(c\) one or zero, and subAff is that pair. The paper’s case analysis over the branches of the subline construction is not needed: the disjunction is proved once and used once.

The axis bound is the same case distinction padCase already makes. A padded direction in the \(X\) or \(Z\) block leaves \(\alpha \) and \(\beta \) constant along the line, so the combined polynomial inherits the degree of \(f_X\) and \(f_Z\) — degree \(d\) exactly when Lemma 3.57 supplies it, which is why degLE_padCombine_aline takes that as a hypothesis. A direction at \(\alpha \), \(\beta \) or a dummy coordinate leaves both blocks constant, so the combined polynomial is affine, and there \(d \geq 1\) is all that is used.

The measurement. padLineMats is \(\widehat Q^\ell \): the uniform average, over the fresh randomness the subline construction draws, of the pasted line measurement \(T^{\ell _X,\ell _Z}\) coarse-grained by padCombine. Conditioning on the padded line is exactly averaging over that randomness and nothing else, so the paper’s conditional expectation is a plain uniform average. sum_padLineMats and posSemidef_padLineMats are that it is a POVM, and sum_filter_padLineMats is the data-processing step the paper’s proof ends with, in the form pairs_of_lines_prod applies to.

Lemma 3.58, on the product. pairs_of_lines_prod is that lemma at \(k_X = \mathtt{pairCX}\), \(k_Z = \mathtt{pairCZ}\) and pairShift as the shift: each side’s content is its own point, seed and raw direction, with the other side’s point filled in as the content’s other point, which no quantity of that side’s line depends on. The two \(\mathtt{rfl}\)s pairCX_pairShift and pairCZ_pairShift are the whole of the instantiation — the generalization it instantiates is recorded under Lemma 3.58, since that is the lemma it proves.

And from the game. pairs_of_lines_prod_of_items takes only game-level hypotheses and delivers the product form, which is what the consistency chain consumes. Two things had to be arranged for it. First, the combined point measurement is re-indexed by the pair of points (combined_points_pts) rather than by the content: all four inputs of the joint-measurement construction see the content only through its two points, so the same construction runs at the pair, and the resulting measurement is usable at any sample space carrying two points — whereas the content-indexed one would have to be fed contents with zeroed probes, whose average is not the content average. Second, FactorsX and FactorsZ say that a line presentation reads the content only through that side’s line-point data; both presentations satisfy them by \(\mathtt{rfl}\), and that is what lets avg_content_eq_pair_X carry each content-level bound to the product (avg_pair_eq_content_X and its three companions).

The restricted laws, and where the factors of \(m\) come from. avgRestr was already the paper’s \(D_{\mathrm{ty},i}\). sum_avgRestr says the \(m\) restricted laws average to the unrestricted one, so each is at most \(m\) times it (avgRestr_le_mul_avgAll) and a product of two is at most \(m^2\) times the product (avgRestr_prod_le_mul_avgAll). The paper’s factor is \(2m\) because it mixes over the two line types; here the type is a parameter, so it is \(m\). This is the whole source of the leading \(m\) in \(\delta _{\mathrm{combine}}\).

The paper’s three Cauchy–Schwarz claims are avoidable here, and this is a finding. The paper proves the consistency by chaining Claims 17-1, 17-2 and 17-3, and says in a comment that the chain is needed because “under the distribution \(D\) the pair is correlated (for diagonal lines both coordinates share the line parameter), so that decomposition is not available”. The correlation is real given the padded line — a uniform point of it moves both blocks with one parameter — but the quantity to be bounded conditions on the two sublines, which know each block’s coset in its own space and not the relative offset of the two blocks. Marginalizing that out restores independence, and avgSub_free and its three companions (Lemma 3.60) already prove the joint law to be exactly a product of the two marginals at a fixed padded seed. avgSub_le_mul_avgAll combines that with the restricted-law transfer: the padded line–point law is at most \(m^2\) times the product of the two unrestricted subline laws, uniformly in the padded seed and the line type. avgSubAB_le_of_forall does the same for \(\alpha \) and \(\beta \) at the sampled point: translating the padded point in those two coordinates alone is a bijection that leaves both sublines fixed, so they are uniform and independent of everything else and a bound holding for each fixed \((\alpha ,\beta )\) holds for the joint law. No refinement of the block decomposition is needed. The report is reports/padded-lines-product-law.md.

The consistency bound is proved, in MIPRE/Background/QLD/PaddedLines.lean. padded_lines_consistency is it: on the padded line–point law, at every padded seed and line type, the combined point measurement read along \((\alpha ,\beta )\) at the sampled point agrees with the pasted line measurement coarse-grained by the combining map, up to \(m^2 \cdot \delta _P\). The proof is the coarse-graining step (sum_bornProb_le_fibre: agreement only increases under a common coarse-graining, for bare matrix families rather than POVM structures, which is what the pasted measurement is) followed by the two domination lemmas.

What of the statement is conditional. Two of the three gaps this paragraph used to list are closed. The error form was corrected to \(\mathrm{poly}(m)\cdot \mathrm{poly}(\varepsilon ,md/q)\) in the statement above, which is what is proved; and the second register version is padded_lines_consistency_swap, by the game’s player symmetry. What remains is the degree bound \(d\) on an axis-parallel line, which is conditional on Lemma 3.57 — an additional target there, and the reason the degree clause is written conditionally above. So the proof mark covers the consistency bound and the measurement’s being a POVM, and the degree clause only given that lemma. reports/padded-lines-product-law.md records the history, together with the size of \(\delta _P\) itself: \(\delta _P \approx 7\cdot 10^3\, \varepsilon ^{1/4} + 1.5\sqrt{md/q}\), so the bound is vacuous unless \(\varepsilon \leq 4\cdot 10^{-16}\) — a property of the whole chain’s constants, not of this step.

[\(\bullet \bullet \) medium]

Comments.

MIPRE/Background/QLD/PhysModel.lean: the padding register is PadAnc, the padded model padModel with soundIn_padModel and soundIn_padModel_swap, the physical model phys on the state physE, the first cut cut1 with its reading lemmas for the two players, the embeddings \(j_1\) and \(\iota _1\), item 1’s cut tgt with the regrouping unassoc, and the exchange of the blocks blockSwapIso. The matrix analysis built each of these states as an explicit vector on a product of index sets — the twice-padded state, the appended second pair, item 1’s regrouped state — and moved between them by reindexing whole spaces. Here every state is an ancilla extension of the strategy’s model by finite registers in a joint vector, only the finite registers are regrouped, and a regrouping is a local isometry or an isomorphism of models. The two cuts are two readings of one state model, so that nothing has to be proved about their states agreeing, and both players’ dilations are taken on one padding register at one common size, so that the two runs of stage 4 read one physical state. The padded model is where stage 4 applies the seeded CL test (Lemma 3.66); the first cut is where stage 5 reads its output (Lemma 3.63); and the physical model is where the two parties’ exact Pauli objects are compared (Lemmas 3.76 and 3.77).

[\(\bullet \bullet \bullet \) hard]

Comments.

The conclusion is formalized as the structure SimulPair (MIPRE/Background/QLD/Simul.lean): for a projective strategy of a bipartite model and an error \(\delta \), a model \(K\) into which the register model embeds (Definition 8.90) — a local isometry carrying the state to the state and keeping both units, along which every expectation of the expanded measurements transfers exactly — projective pair measurements \(S_A\), \(S_B\) in \(K\)’s algebras, with outcomes in pairs of individual-degree-\(d\) polynomials, and the two evaluated-marginal consistencies against the opposite party’s expanded point measurements carried to \(K\). The lemma is the existence of a SimulPair at error \(\delta _S\) in the padded model, along the inert embedding (exists_simulPair). A SimulPair moves along any further embedding (SimulPair.transport), and stage 5 uses it on the first cut of the physical model, along the embedding \(\iota _1\) of Definition 3.62 (CutSimul); the transport along \(j_1\) of the padded model’s SimulPair is one by definition. Two departures from the paper’s statement. The sandwiched joint estimate it also announces is not carried in the structure: stage 5 consumes only the two evaluated marginals, and the sandwich is what Lemma 3.72 passes through on the way to them. And the hypothesis is \(48md \leq q\) rather than the standing \(16md \leq q\), which is what makes the factor \(1 - 2\eta \) of Lemma 3.70 at least \(1/2\); as with \(16md {\gt} q\), the regime \(48md {\gt} q\) is absorbed in the assembly by enlarging the universal constant (Lemma 3.78).

Comments.

The ledger node dilates the line POVMs to projective measurements at this point, “using fresh local product ancillas”. The formalization keeps the strategy as a family of POVMs and dilates once, at the application of the soundness theorem (Lemma 3.66), on the padding register of Definition 3.62: on the padded model the Born rule sees only the reference entries of the dilated measurements, which are the padded strategy’s, so nothing has to be proved about the dilation beyond its compression (Lemma 8.77). The node’s “\(16md {\gt} q\)” clause belongs to the assembly of Theorem 3.38, where the trivial bound is used instead of the padded theorem (Lemma 3.78). The node also lists \(4m \mid q\) beside the regime, as though it were a further hypothesis; here it is derived, and the derivation is worth getting exactly right, because the obvious reading is false: \(m \mid q\) with \(q\) a power of two gives only that \(m\) is a power of two, and at \(m = q\) the conclusion fails. What gives \(4m \mid q\) is \(m \mid q\) together with \(4m \leq q\) (four_mul_dvd_card), which the regime \(48md \leq q\) supplies (four_mul_dvd_card_of_regime, MIPRE/Background/QLD/Regime.lean); stages 4 and 5 derive it there, and outside the regime the trivial bound is used and the divisibility is never needed. Nor is admissibility what the step uses — the oddness of the degree is for the self-dual basis — since a finite field of characteristic two has power-of-two size already (exists_card_eq_two_pow).

Comments.

The decider’s acceptance is only implied by, not equal to, agreement of the relabelled answers: an ill-formatted answer that happens to agree is still rejected. The formalization uses the implication in the one direction it holds and asks it only of answers the strategy can produce (condFail_le_one_sub_sum_bornProb_map). The paper’s proof compares \(f_A(u)\) with \(f_B(u)\) at a uniformly random point \(u\) of the line; the formalization reads the sample’s own point instead, which makes the uniformity of the parameter a change of variables rather than a conditioning.

Comments.

The seeded test enters as a hypothesis on the model, its soundness in every ancilla extension by a unit vector, rather than as Theorem 3.19 applied to matrices; in the tensor-product model the hypothesis is Lemma 8.66, which rests on that theorem, and its error \(\delta _{\mathrm{sim}}\) is the one of the model statement, whose constant is \(40 a_1 4^{a_1}\) for the constant \(a_1\) of Theorem 3.19 (Lemma 3.34). The dilation is the one of Lemma 8.77, in the players’ algebras, so it needs neither finite dimension nor a square root. The second Naimark dilation of the paper’s proof, applied to the recovered polynomial measurement, is not needed: the soundness theorem already returns projective measurements (as the ledger’s challenge history of node 1.2.2.13 records). The recovered polynomials are functions on \(\mathbb {F}_q^{4m}\), while the padded point measurements read only the \(2m+2\) coordinates \((x, z, \alpha , \beta )\); the Schwartz–Zippel argument that the polynomials do not read the remaining dummy coordinates is Lemma 3.67.

Comments.

The paper’s orthogonality step uses that the point measurements are projective, which the dilation’s are; the formalization works with the padded point measurements of the original strategy, which are POVMs, and replaces orthogonality by \(P_b + P_{b'} \leq I\) for \(b \neq b'\), valid for any POVM. Schwartz–Zippel is applied with individual degrees, on two copies of the \(4m\) coordinates; the formalization states Lemma 3.111 for any finite variable type (prob_agreeOn_le_individualDegree) and bridges the seeded test’s coefficient vectors to MvPolynomial (LowIndDegPoly.toMv, listed with Lemma 3.33, which uses it first). The outcomes are not relabelled: the projective submeasurement is the restriction of the global measurement to the \(w\)-independent outcomes, and its complement’s weight is the bound above.

Comments.

The paper restricts to \(w\)-independent outcomes and goes through the projective joint measurement of Lemma 3.56; the formalization works with the sandwich combination itself, which is a POVM and needs no projectivity, and proves the estimate for all outcomes, so Lemma 3.67 is not needed here. The two orders are one abstract theorem (sum_snorm_sq_ordComb_le), which takes the identity \(\sum _{a, b} \mathrm{ord}(a, b) = I\) and the contraction bound as hypotheses. The error is \(2\delta _{\mathrm{ld}} + 2 \cdot 57676416\, \varepsilon \), linear in both.

Comments.

The paper (eq:qld-g-prime-bound) states the bound as \(O((\delta _{\mathrm{ld}} + \delta _Q)^{1/2} + md/q)\) for the \(w\)-independent outcomes, and remarks that the quadratic expansion used here supports the linear bound; the formalization proves the linear bound, for all outcomes and with an explicit constant, so Lemma 3.67 is not needed here. The paper goes through the projective joint measurement of Lemma 3.56 and drops the \(\beta = 0\) pairs at a cost of \(1/q\); here the products estimate is used directly and the \(\beta = 0\) pairs are bounded by the contraction property. The two Schwartz–Zippel applications are card_eval_eq_zero_le (a nonzero coefficient vector in \(4m\) variables, at \(4md/q\)) and sum_agree_two_le (two distinct bivariate coefficient vectors, at \(2d/q\)), both through the bridge LowIndDegPoly.toMv. The coefficient vectors are LowIndDegPoly.coef, the coefficient of a monomial pattern on a set of coordinates as a polynomial in the others (eval_eq_sum_coef). The bridge, the first estimate and the patterns are in MIPRE/Background/LIDT/Coefficients.lean, below the seeded test, and are listed with Lemma 3.33.

Comments.

The paper states the excluded weight as \(\delta _G = O((\delta _{\mathrm{ld}} + \delta _Q)^{1/2} + md/q)\); the formalization proves the linear bound, as for Lemma 3.69, and with its own constants: both Schwartz–Zippel applications are over all \(4m\) coordinates (card_eval_eq_zero_le), where the paper counts \(2m\) or \(2m + 2\). The good outcomes exclude the dummy coordinates as well, so this lemma subsumes Lemma 3.67 for the purposes of stage 4c. The conditioning on a block is one generic statement (sum_uniform_bornProb_readOn_le), for an operator family reading only the coordinates in a set \(T\) and a polynomial reading a coordinate outside \(T\), with LowIndDegPoly.restrictOff the polynomial in the other coordinates obtained by fixing those in \(T\); the assembly is one generic statement (sum_bad_mass_le_of_avg), which Lemma 3.69 could also use.

Separation and the swap isometry

[\(\bullet \bullet \) medium]

Comments.

The paper absorbs the \(\varepsilon \) of the second item into \(\delta _S\); here both constants are explicit, and the second item’s is \(4\delta _S + 344\varepsilon \). Both items are stated for the evaluated marginal at an outcome \(a \in \mathbb {F}_q\) rather than per polynomial \(g\): the two are the same sum, grouped differently, and the outcome form is what the Pauli construction consumes.

[\(\bullet \bullet \bullet \) hard]

Comments.

Both halves are formalized, for a simultaneous pair measurement (Lemma 3.63) of a strategy of failure \(\varepsilon \), and both are about the same objects: \(\tilde{M}^{W,\mathrm{ind}_m(u)}\) and \(\tilde{W}^e(\tilde{u})\) built from that measurement, on that party’s registers. The closeness constant is explicit,

which is the \(O(\delta _S + \sqrt{\varepsilon } + md/q)\) the paper absorbs into \(\delta _S\). The rest of this comment records how it was reached, because two of the obstacles it used to list turned out not to exist.

Of the approximate half’s ingredients, three were in place first: the agreement form of Schwartz–Zippel against every multilinear polynomial at once, the aggregation that turns it into a bound on the mass at non-multilinear outcomes, and the substitution error of two families agreeing off that mass (MIPRE/Background/QLD/NonMultilinear.lean). A fourth is now too: the strategy’s \((\mathtt{Point}, W)\) measurement and the low-degree reading of its \((\mathtt{Pauli}, W)\) answer are close on one party, at \(688\, \varepsilon \) (sum_normSq_point_sub_pauli_le), which is what lets the point be sampled independently of the operators. The two inputs are cross-party items of Lemma 3.46, and they share Alice’s point measurement, so one triangle inequality removes it. A fifth carries such a statement from the strategy’s state to the expanded one: every hatted measurement is a convolution \(\widehat X_c = \sum _{a + b = c} X_a \otimes T_b\) with the ancilla’s Weyl measurement, and for a projective \(T\) the cross terms of \(\widehat X^\dagger \widehat X\) vanish, so the common ancilla factor drops out exactly: \(\sum _c \| (I\otimes \widehat X_c) \widehat\psi \| ^2 = \sum _a \| (I\otimes X_a) \psi \| ^2\) (sum_normSq_stateVecB_conv_eq). The two together put the closeness on the expanded state with the same constant (sum_normSq_hat_point_sub_pauli_le). The aggregation has now been applied to the simultaneous measurement’s outcomes, in MIPRE/Background/QLD/Multilinear.lean, and the bound the appendix’s repair turns on is formalized: with \(\widehat S^W\) a simultaneous pair measurement of error \(\delta _S\) for a strategy of failure \(\varepsilon \),

(SimulPair.sum_bornProb_not_isML_le). Its three inputs are the point-independent family indexed by cube data (hatPauli, the strategy’s \((\mathtt{Pauli}, W)\) measurement convolved with the ancilla’s Weyl measurement, projective and independent of the sampled point, whose reading at a point is the hatted Pauli measurement there — hatPauli_map); the Cauchy–Schwarz that substitutes it for the point measurement at cost \(\sqrt{688\, \varepsilon }\) (abs_sum_weighted_bornProb_le, SimulPair.sum_bornProb_hatPauli_ge); and Lemma 3.111 per non-multilinear outcome, uniformly in the cube datum (sum_uniform_agree_ldEnc_le). The marginal is taken indexed by polynomials rather than by their value at the point (polyMarg), which is what makes the outcome operator independent of the point that Schwartz–Zippel then samples.

And the agreement itself is formalized: expanding \(\tilde{M}^{W,\mathrm{ind}_m(u)}_a\) and contracting the generalized Pauli against the strategy’s point measurement turns the first item’s left-hand side into the outcome sum with the label \(\mathrm{Coded}(g) \cdot \mathrm{ind}_m(u)\), and

(SimulPair.sum_bornProb_cubeData_ge), from the helper’s agreement read by polynomial (SimulPair.sum_bornProb_polyMarg_ge) and the mass bound, through sum_sub_le_of_eq_on.

One outstanding ingredient turned out not to be needed. The chain was stated with the good set “\(g\) is multilinear”, and then agreement of the two labels on it is uniqueness of multilinear interpolation — an independent fact about MvPolynomial that sum_sub_le_of_eq_on took as a hypothesis. Taking the good set to be “\(g\) is the low-degree encoding of its own cube data” (IsInterp) removes it: there the two labels agree by definition (dotF_cubeData_indVec), and off it \(g\) differs from the encoding of every cube datum (ne_ldEnc_of_not_isInterp), which is exactly the hypothesis Schwartz–Zippel wants, uniformly in the datum. Uniqueness of multilinear interpolation would say the two sets coincide; neither inclusion is used.

Formalized, unconditionally, in MIPRE/Background/QLD/ExactPauli.lean: the two marginals of a projective pair measurement (sCoarse, projective by IsPVM.coarse), the measurement \(\tilde{M}^{W,\tilde{u}}_a\) (mTilde) and the observable \(\tilde{W}^e(\tilde{u})\) (wTilde), and the identity everything rests on: wTilde_eq says the observable factorizes as a signed sum of the pair measurement tensor a bare generalized Pauli. Self-adjointness, squaring to the identity, and the twisted commutation relation are then three lines (wTilde_conjTranspose, wTilde_mul_self, wTilde_mul_wTilde), and linearity in the argument a fourth (wTilde_mul_add: both tensor factors are additive, the sign because the pairing is and the generalized Pauli by the Weyl family’s group law), with IsPVM and MIPRE.Weyl.IsWeylFamily the only hypotheses — no game, no error term, and no appeal to Theorem 3.55, exactly as the proof above says. All four are instantiated at a simultaneous pair measurement in MIPRE/Background/QLD/MTilde.lean (SimulPair.wTildeAt and its relations), which is what puts them on the same objects as the closeness below.

The phase is the general one. The pinned paper’s display for the commutation relation used to split into \(e \neq e'\), claiming exact commutation, and \(e = e'\), carrying a phase. That split is false: self-duality gives \(\operatorname {tr}(e_j e_{j'}) = \delta _{j j'}\), but \(\operatorname {tr}(e_j e_{j'} c)\) need not vanish for \(c\) outside \(\mathbb {F}_2\), and the exponent here is \(e e' (\tilde{u} \cdot \tilde{v})\) with an arbitrary field element in the middle. The paper now displays the general phase, and wTilde_mul_wTilde is that phase: no case split, and no reference to a basis, since the relation holds for every pair of field elements.

The critical finding is discharged where it can be, in MIPRE/Background/QLD/NonMultilinear.lean. prob_agree_ldEnc_le_of_not_multilinear is Lemma 3.111 in the agreement direction and uniformly in the interpolated data, which is what the sum over \(\mathbb {F}_q^M\) needs; nonMultilinear_mass_le is the aggregation that turns it into the bound on the mass the simultaneous measurement places on non-multilinear outcomes; and sum_sub_le_of_eq_on is the substitution error given that mass, taking agreement on the good set as a hypothesis — which is why the choice of good set below matters.

And it is read as a closeness of two measurements, which is how the paper states item 1. \(\tilde{M}^{W,\mathrm{ind}_m(u)}\) is a projective measurement (isPVM_mTildeAt, through sTensor_mul, so through projectivity of the simultaneous measurement and nothing else), and

(SimulPair.sum_bornProb_mTilde_ge, and SimulPair.inconsistency_mTilde_le for the \(\simeq _\delta \) form). The two are the same statement grouped differently: expanding \(\tilde{M}\) and contracting the generalized Pauli against the point measurement is sum_kron_syn_eq_hatMats, one characteristic-two shift.

The second entangled pair is not needed here. The paper’s expanded state \(|\hat\psi \rangle = |\psi \rangle _{\textsc{A}\textsc{B}} \otimes |\textsc{EPR}\rangle _{\textsc{A}'\textsc{A}''} \otimes |\textsc{EPR}\rangle _{\textsc{B}'\textsc{B}''}\) carries two entangled pairs, each local to one party, and is read along two cuts — \(\textsc{A}\textsc{A}' \mid \textsc{B}\textsc{A}''\) for one orientation of Lemma 3.63 and \(\textsc{B}\textsc{B}' \mid \textsc{A}\textsc{B}''\) for the other — while the register model of the strategy’s model has one pair, along one such cut. That is all Lemmas 3.63 and 3.74 need. Writing \(\tilde{M}^{W,\tilde{u}} = \sum _g \widehat S^W_g \otimes \tau ^W_{\mathrm{Coded}(g) \cdot \tilde{u} - a}(\tilde{u})\) as one operator wants \(\widehat S^W\) and the generalized Pauli on the disjoint registers \(\textsc{A}\textsc{A}'\) and \(\textsc{A}''\), and needs no new pair: the register \(\textsc{A}''\) is already there, on the far side of the cut. In the formalization \(\widehat S^W\) is an operator of the first player of the first cut, on \((E_A, A')\), and \(\tilde{M}\) one of the first player of the physical model, on \((A'', E_A, A')\) with the Pauli register outermost (Definition 3.62). The first cut and the physical model are two readings of one state model, so every Born probability is read on the physical model by the reading lemmas (phys_bornProb_compHom_smulKron), the strategy’s own measurements entering with the registers inert (physInert). No second pair, no transport between cuts, and no new estimate.

A ledger discrepancy worth recording. Node \(1.2.2.15\) declares its dependencies as \(\{ 1.2.2.13, 1.2.2.14, 1.2.2.7\} \) — the last being Theorem 3.55 — and does not declare \(1.2.2.4\), Lemma 3.46. The paper’s current proof of this step is the other way round: it does not use exact linearity at all, and it does use the win implications, at enu:qld-pauli-basis-cons and enu:qld-cons. The uses list above follows the paper. reports/qld-stage5-blueprint-repairs.md records it.

[\(\bullet \bullet \bullet \) hard]

Comments.

This statement is not in the pinned paper’s Lemma 3.75; it is the second item of that lemma in the paper, and the blueprint’s paraphrase of Lemma 3.75 dropped it. That was found by formalizing: Lemma 3.77’s item 1 needs the two twirls to be near-invariances of the state, and the only thing that supplies them is this self-consistency at a uniform \(\tilde{u}\) — not at \(\tilde{u} = \mathrm{ind}_m(u)\), which is all Lemma 3.75 gives. So the dependency graph was missing an edge, and worse, a node. It is separated out here rather than folded back into Lemma 3.75 so that the latter’s leanok marks stay honest: what is formalized there is exactly what it states.

The exact steps of the chain are formalized. Its eleven displays are of two kinds: steps marked \(\approx _0\), which are identities, and steps marked \(\approx _\delta \), which are estimates. All the identities are in place.

syn_mul_syn is display eq:qld-pulling-2b: the syndrome projectors of one Weyl family at two different probes multiply to the projector onto the outcomes satisfying both conditions — off the diagonal the spectral projectors annihilate each other, so only the eigenvalue patterns in both level sets survive.

SimulPair.stateVec_ancSyn is eq:qld-pulling-3a: a generalized Pauli moves from one party’s ancilla half to the other’s at no cost, the two halves being maximally entangled and the syndrome projectors symmetric. The point worth recording is that this is available at all. Lemma 3.63 does not say that the model of the pair measurement is the register model, only that the register model embeds in it, carrying its expectations, so a vector identity about its state looks out of reach. It is not: the identity to be proved is the vanishing of a squared norm, and a squared norm is an expectation, so SimulPair.xSqNorm_aOp carries it across with no loss.

SimulPair.sum_ancSyn_mulVec is eq:qld-pulling-4: summing the matched pairs of syndrome projectors, one on each party, leaves the state unchanged, since by the transport each matched pair acts as the projector on one side alone and those sum to the identity.

And what the estimates consume is in place. Two of the \(\approx _\delta \) displays, eq:qld-pulling-7 and eq:qld-pulling-11, are the second item of Lemma 3.74 — but not in the indexing that lemma is stated in. The helper is stated at an outcome \(a \in \mathbb {F}_q\), which is what the expansion stage produces, while the chain sums over the polynomial outcomes \(g\), because the label \(\mathrm{Coded}(g) \cdot \tilde{u}\) it carries is a function of \(g\) and not of \(g(u)\). The two sums are equal, not merely comparable: within a fibre of the evaluation the pair measurement’s outcomes are orthogonal projectors, so every cross term of the squared norm vanishes (snorm_sq_sum_orthogonal), and the fibres partition the outcomes. That gives SimulPair.sum_snorm_sq_polyMarg_one_sub_le, at the helper’s own constant \(4\delta _S + 344\, \varepsilon \).

Display eq:qld-pulling-12 is Lemma 3.111 again, in the form sum_uniform_agree_mass_le: restricting a weighted sum to the tuples where two distinct outcome polynomials agree at the sampled point costs \(md/q\), the weights being Born probabilities of a projective family and so summing to at most one. No lower bound on \(d\) is needed here, unlike at prob_agree_ldEnc_le_of_not_multilinear: both polynomials carry the same degree bound, so the hypothesis is already met.

And the near-identity is a projection. Display eq:qld-pulling-1 right-multiplies by \(\sum _g (\widehat S^W_g)_{\textsc{A}\textsc{A}'} \otimes (\widehat M^{(\mathtt{Point},W),u}_{g(u)})_{\textsc{B}\textsc{A}''}\), which the first item of Lemma 3.74 says is close to the identity on the state. What makes the step cheap is that this operator is a projection (agreeOp_mul_self): the pair measurement’s outcomes are orthogonal, so the cross terms vanish, and the opposite party’s factors are projectors. Its deficit from the identity is then exactly one minus the agreement (snorm_sq_one_sub_agreeOp) — linear in the operator, with no Cauchy–Schwarz anywhere — and a contraction on the left cannot amplify it (snorm_sub_mul_agreeOp_le). The package asks only the first party’s family to be projective, which is what lets it apply here, where the second party’s factors are indexed by \(g\) through \(g(u)\) and so are not a measurement in \(g\).

And the two ends of eq:qld-pulling-10’s justification. That display is argued by bounding the magnitude of a difference, and the argument runs from fact:add-a-proj at the top to the helper at the bottom. Both ends are in place. The top is sum_kron_le_one: a family of projectors on one factor, tensored with a projective measurement on another, sums to at most the identity, because the complement \(\sum _x (I- B_x) \otimes T_x\) is a sum of positive semidefinite terms; against a positive operator on the other party that discards the index the sandwich runs over (sum_bornProb_kron_le). The bottom is eq:qld-pulling-14, SimulPair.sum_bornProb_polyMarg_one_sub_le: the complement of the helper’s agreement, read by polynomial outcome, is at most \(\delta _S\), the marginal’s outcomes summing to the identity.

And the middle of that justification, which is the only Cauchy–Schwarz in the chain. The estimate expands a squared norm over the orthogonal outcomes of a projective family into a sum of sandwiches, one per outcome (snorm_sq_sum_proj_sandwich); drops the constraint on the outcomes, every sandwich being nonnegative (sum_qform_sandwich_le_of_subset); and then moves the sandwiched measurement from one party to the other. That is abs_sum_qform_swap_le, display eq:qld-pulling-13: the difference of the two sandwiches is two terms each carrying the deviation on one side, and each is bounded by \(\sqrt{\varepsilon }\) against a mass at most one, so the substitution costs \(2\sqrt{\varepsilon }\). The side that is left as a single factor rather than a sandwich is the one whose measurement commutes with what it sandwiches, where \(XSX = XS\).

And eq:qld-pulling-3. The expansion leaves one party’s projector beside the other party’s point measurement, and the chain inserts a copy of that measurement on the first party’s side, spending the self-consistency of Lemma 3.46. Two things make the step cost that and no more. The deficit of the insertion is the cross-party deviation itself (snorm_one_sub_aOp_mul_bOp_le): \((I- A)B = B(B - A)\), the outcome inserted beside being a projection and the parties commuting, and a projection in front costs nothing. And the family in front is indexed through a map to the measurement’s own outcomes, so the sum sees only the fibres of that map (sum_snorm_sq_proj_comp_le). Without the fibres the step would be false: the family’s index is far larger than the outcome set, and paying one deviation per index would multiply the bound by the size of a fibre. The display is sum_snorm_sq_insert_le.

And the final passage was already in the library. Coarse-graining two projective measurements the same way costs nothing — which is Item 2 of fact:agreement, then fact:data-processing, then Item 1 of fact:agreement — and Foundations has it as sum_xSqNorm_map_le, on bundled POVMs. The chain speaks IsPVM; IsPVM.toPOVM and sum_xSqNorm_fibre_le bridge the two.

And the probe it runs at. This chain is stated at a uniform \(\tilde{u} \in \mathbb {F}_q^{M}\), and that is not a point’s low-degree encoding — the encodings are a tiny subset of \(\mathbb {F}_q^M\). Confusing the two is the omission that created this node, so the two probes are kept apart by name: SimulPair.mTildeAnc is the exact Pauli measurement at an arbitrary probe, mTildeAt_eq_mTildeAnc is the one place it meets Lemma 3.75’s, and swapU_conj_mTildeAnc says that conjugation by the swap unitary strips the pair measurement off it whatever the probe — the cancellation is between the outcome’s shift and the conjugation’s, and both are written with the same pairing.

And a strategy has one. MirrorSimul is the pair of cuts the chain runs on, and exists_mirrorSimul constructs it: a legal projective strategy of value \(1 - \varepsilon \), in a model in which the seeded CL test is sound in every ancilla extension by a unit vector, has both cuts, on one state, in the regime \(48md \leq q\). The construction is two runs of Lemma 3.63, one at the strategy and one at the strategy with the players exchanged, in the model with the players exchanged, at one padding size (mirrorOfGlobalPairs); each run’s pair measurement is carried to the first cut of its physical model along the embedding \(j_1\) of Definition 3.62. The interface does not ask the two cuts’ pair measurements to be related — the paper does not either, its simultaneous-measurement lemma giving one measurement per player’s space — and it has nothing to say about their states: the physical model of the exchanged model is the physical model with the two players’ algebras exchanged, so the two cuts read one state by construction.

And the conclusion is expressible. Both sides of this statement are exact Pauli objects, one per party, so writing it down at all needs each party’s whole triple on its own side of one cut: Alice’s \(\textsc{A}\textsc{A}' \textsc{A}''\) against Bob’s \(\textsc{B}\textsc{B}' \textsc{B}''\). That cut is the physical model, and the shape MirrorSimul takes was decided by three sentences of the paper rather than by the Lean types.

The registers are partitioned two ways — \(\textsc{A}\textsc{A}'\) against \(\textsc{B}\textsc{A}''\), and \(\textsc{B}\textsc{B}'\) against \(\textsc{A}\textsc{B}''\) — and qld-commutation.tex’s sec:expanding records that every bipartite relation derived for one holds for the other with the registers changed. Lemma 3.63 gives \(\widehat{S}\) on \(\textsc{A}\textsc{A}'\) and on \(\textsc{B}\textsc{B}'\), one per player’s space, and it is the second that \(V_\textsc{B}\) conjugates by. So the second reading is not data of a new kind: the mirror of a SimulPair is a SimulPair, at the exchanged players and the exchanged strategy. A MirrorSimul is the padding size and the two cuts’ pair measurements, first and second, and every lemma already proved about a SimulPair — mTildeAnc, swapA, swapU_conj_mTildeAnc — becomes Bob’s by instantiation at second, with no mirror lemma to prove. bobSwap_conj_bobMTilde is the paper’s “an entirely analogous calculation shows” discharged that way.

Each cut’s pair measurement acts on its own player’s registers only, \((E_A, A')\) for the first and \((E_B, B')\) for the second, so \(\widehat{S}\) never acts on the other player’s registers — a non-local \(\widehat{S}\) would make \(\tilde{M}\) and the swap unitary non-local, and then the two sides of this lemma would not lie on opposite sides of any cut. And \(\tilde{M}\) writes its Pauli register outermost, which is where the physical model puts the far half of the player’s own pair: mTildeAnc, flattened, lands on Alice’s physical registers \((A'', E_A, A')\) with nothing to reindex, and the second cut’s on Bob’s. aliceMTilde and bobMTilde are the two sides, operators of the two players of the physical model, and selfConsGap is this lemma’s left-hand side. A statement proved on the physical model of the exchanged model reads on the physical model along the exchange of the blocks (phys_swap_bornProb, phys_swap_inconsistency and their companions). The matrix formalization appended each cut’s missing pair to the other cut’s state and proved the two appendings equal; planning/qld-two-pairs-scope.md keeps the designs it discarded on the way.

And the chain’s two ends are formalized, which leaves only its middle. The chain’s arithmetic frame is MIPRE/Background/QLD/Chain.lean, and it holds no estimate at all: it is the index algebra the eleven displays are bookkeeping for.

At the near end, mTildeAnc_eq_sum_chainIdx is eq:qld-pulling-2 and eq:qld-pulling-2b: the exact Pauli measurement, written not as ‘eq:tilde_M‘’s sum over pair outcomes \(g\) with a syndrome projector attached, but as the chain’s sum over pairs \((g,h)\) cut out by \((\mathrm{Coded}(g) - h) \cdot \tilde{u} = a\). The two are the same sum, the syndrome projector being the fibre of the spectral family over that pairing; in characteristic two the shift the definition carries is the sum the chain’s label is written with (dotF_chainLabel_eq_iff).

At the far end, endOp is display eq:qld-pulling-12 and endOpMirror_eq is the sentence that makes the whole lemma go through. Both parties’ derivations end at that display, and the reason the two are then close to each other rather than each close to something is that it is symmetric in the two pairs — which is not apparent, its index set being cut out by a coupling that mentions both pairs and a pairing condition that mentions only the first. chainLabel_eq_of_coupled is why: coupled pairs carry the same label, so the condition may be read off either, and the whole index set is invariant under exchanging them (swap_mem_coupledIdx). Evaluating the coupling at a cube point is the entire proof, the encoding of a cube datum being that datum on the cube.

And sum_xSqNorm_le_of_endOp closes it: given the two chains, the triangle inequality for a family of deviations (sum_snorm_sq_triangle’, already in Foundations) gives eq:qld-pulling-cons at twice the cost, which is the factor the paper absorbs into \(\delta _S\).

And the chain’s first step. Display eq:qld-pulling-1 right-multiplies the exact Pauli measurement by the near-identity, and SimulPair.sum_uniform_snorm_sq_nearId_le is that display at item 1 of Lemma 3.74’s own constant. Two things make it cost that and no more. The insertion’s deficit is exactly the near-identity’s, because the measurement’s outcomes are orthogonal, so summing the deviation over them leaves one copy rather than one per outcome (sum_snorm_sq_sub_mul) — without that, the bound would carry a factor \(q\). And the near-identity lives on the first cut, where snorm_sq_one_sub_agreeOp turns its deficit into the helper’s Born probability, while \(\tilde{M}\) lives on the physical model, which has \(\textsc{A}''\) with Alice. The two are readings of one state model, with one Hilbert space and one state, so a state norm is the same number on both and the first cut’s reading lemmas move an operator between them. That is what lets each step of the chain be read along whichever of the paper’s three groupings it is local in, rather than forcing one grouping on all of them.

And the expansion that follows it. Displays eq:qld-pulling-2 and eq:qld-pulling-2b carry out the product, and SimulPair.aOp_mTildeAnc_mul_nearId is that computation at the interface. It is an identity, not an estimate, and it runs in three moves. The near-identity expands because the hatted point measurement is the convolution \(\sum _{a'} M^{(\mathtt{Point},W),u}_{a'} \otimes \tau ^{W,u}_{c-a'}\) by construction (sum_kron_syn_eq_hatMats), and the reading lemmas of the first cut send each of its terms to the physical model, where \(\tilde{M}\) lives, putting \(\tau ^{W,u}\) beside Alice and the point measurement alone on Bob (SimulPair.nearId_eq_sum). Multiplying then kills all but one pair outcome, the family being projective, and fuses the two syndrome projectors into the Weyl outcomes meeting both conditions — syn_mul_syn, which is where the chain’s index set first appears (SimulPair.mTildeAnc_mul_kron). Finally the sum over Bob’s outcome collapses: for each Weyl outcome \(h\) exactly one \(a'\) survives, namely \((g - g_h)(u)\), because in characteristic two the condition \(h \cdot \mathrm{ind}_m(u) = g(u) + a'\) determines \(a'\). What is left is a sum over chainIdx, with chainOp as its summand — which is what that definition was introduced for.

And the insertion, eq:qld-pulling-3. The expansion leaves Bob’s point measurement beside each term, and the chain inserts Alice’s copy of it, spending the point measurements’ self-consistency. SimulPair.sum_snorm_sq_insert_chain is that display, and the packaging sum_snorm_sq_insert_le does the work once its two hypotheses are supplied. Both are about the chain’s terms being a projective family in the pair \((g,h)\) (isPVM_chainOp, a marginal of the pair measurement tensored with a Weyl spectral projector — for which isPVM_proj bundles three facts Foundations had only separately). Projectivity is what makes the outcomes not interfere, so the squared norm of the sum over an outcome’s fibre is the sum of the squared norms (snorm_sq_sum_orthogonal’ — the existing common-tail version does not cover the chain, whose tail carries each term’s own point measurement), and it is also what makes the fibres of the outcome map \((g,h) \mapsto (g - g_h)(u)\) be seen once rather than once per index. Summing the display over the measurement outcome \(a\) recovers the whole index set, the sets chainIdx being its fibres, which is Finset.sum_fiberwise.

And the two transports, eq:qld-pulling-3a and eq:qld-pulling-4. Both are \(\approx _0\) steps — identities on the state, not estimates. SimulPair.stateVec_ancProj moves a single Weyl projector from \(\textsc{A}'\) to \(\textsc{A}''\) at no cost, the two halves of the pair being maximally entangled and the projectors symmetric; and SimulPair.sum_ancProj_mulVec is the consequence the chain uses, that summing the matched pairs of them, one on each party, leaves the state alone. AncTransport.lean had both for the syndrome projector, which is a fibre of the spectral family; the chain moves one projector of that family, so it needs the single-projector version, and stateVec_epr_proj — already in Foundations, and already used by the endgame — is the ingredient. The shape of the argument is worth restating because it is what makes these steps available at all: Lemma 3.63 does not say the model of the pair measurement is the register model, only that the register model embeds in it, carrying its expectations, so a vector identity about its state looks out of reach. It is not, because the identity to be proved is the vanishing of a squared norm, and a squared norm is an expectation.

And eq:qld-pulling-3b, which is a definition unfolded the other way. hatMats_mul_proj says the chain’s factor \((M^{(\mathtt{Point},W),u}_r)_\textsc{A}\otimes (\tau _h)_{\textsc{A}'}\) is the hatted point measurement cut down by the Weyl outcome: \(\widehat{M}^{u}_{c}\) times the projector at \(h\) keeps exactly the point outcome \(c - g_h(u)\), because the syndrome factor selects the one term of the convolution whose shift matches \(h\). The supporting fact is syn_mul_proj — a syndrome projector meets a single spectral projector in that projector or in nothing, the syndrome being the fibre of the family over the pairing.

And the last two displays’ common machinery. eq:qld-pulling-5 to -7 and eq:qld-pulling-10 to -12 are the chain’s remaining estimates, and they are the first of its steps to live on all six registers: both compare operators on the physical cut, \(\textsc{A}\textsc{A}' \textsc{A}''\) against \(\textsc{B}\textsc{B}' \textsc{B}''\), which is what MirrorSimul was built to make expressible. They share an outer shape and a way of discharging the far party.

sum_snorm_sq_fiber_sandwich_le is the shape: each display bounds the summed squared norm of the chain’s terms grouped by the measurement outcome, projectivity turns each group into a sum of sandwiches (snorm_sq_sum_proj_sandwich), the groups are the fibres of the outcome map — so the double sum is the single one over the whole index — and what is left to bound carries no outcome at all. sum_bornProb_sandwich_drop_le is the discharge: each sandwich carries, on the far party, a projector times a Weyl outcome, and summed over that outcome these are at most the identity, so the whole sum is bounded by the near party’s sandwiches alone. That is fact:add-a-proj in the form the two displays consume it. MirrorSimul.chainP is the projective family they sum over — Alice’s pair and Weyl outcomes together, against Bob’s Weyl outcome, on the physical cut.

And the first of the two is done. sum_snorm_sq_chainP_le is eq:qld-pulling-5 to -8 and sum_uniform_snorm_sq_chainP_le is eq:qld-pulling-9: the step costs item 2 of Lemma 3.74 and nothing more. Three things had to be arranged, and each is worth recording because the same three recur at eq:qld-pulling-10.

The chain’s tail at this display is chainW, Alice’s gap \(I- \widehat{M}^u_{g(u)}\) against Bob’s point measurement at the shifted outcome \((g - g_h + g_{h'})(u)\) — shifted by both Weyl outcomes, which is what makes the display’s index a triple rather than a pair. chainW_sandwich is where that tail meets the outer shape: conjugating the chain’s projector by it splits across the cut, each party’s factor staying local, so a single rewrite turns the quadratic form the shape produces into a Born probability.

Bob’s side then discharges. bobHat_conj_bobWeyl says his factor is a projector on \(\textsc{B}\textsc{B}'\) tensored with a Weyl outcome on \(\textsc{B}''\), and sum_bornProb_chainW_drop_le sums it away by sum_bornProb_kron_le — the projector varying with the Weyl outcome, which is why the discharge has to be stated with the two indices coupled rather than at a fixed projector.

Alice’s side then collapses and travels. sum_aliceChainOp sums the Weyl outcome out of her summand, the spectral projectors being complete, and sum_aliceChainOp_sandwich carries that through the sandwich, her gap operator not depending on the Weyl index. What is left is on \(\textsc{A}\textsc{A}'\) alone, and bornProb_physVec_aOp reads it on the first cut, where SimulPair.sum_snorm_sq_polyMarg_one_sub_le bounds it: an operator of the first player of the first cut is the physical operator acting as the identity on \(\textsc{A}''\), on the same state.

And Bob’s whole derivation is Alice’s, instantiated. The mirror of a MirrorSimul is a MirrorSimul — at the exchanged players and the exchanged strategy, with the two cuts exchanged. Its two fields give each player’s objects on one cut, which is enough for anything stated there; mirror gives Bob’s objects as the first player’s of the mirror, on the physical model of the exchanged model, which the exchange of the blocks carries to the physical model — what the chain’s last displays compare — so every lemma about the six-register reading becomes Bob’s by instantiation. mirror_sum_snorm_sq_chainP_le is eq:qld-pulling-5 to -8 for Bob, and its proof is one rewrite and one application. The paper’s “an analogous derivation shows” for the second party is discharged that way for the whole chain rather than display by display, and sum_xSqNorm_le_of_endOp, which needs both parties’ chains, will be fed from one.

What makes it go through is that the mirror is an involution by definition (mirror_mirror, by rfl): exchanging the players twice is the identity on models and on projective strategies, and a MirrorSimul carries no state of its own to be exchanged.

And the four-index family. From eq:qld-pulling-9a on, the chain runs over both parties’ pairs: chainQ is that family, projective by isPVM_chainQ, and endOp_eq_sum_chainQ says the chain’s endpoint — in place since the arithmetic frame was built — is exactly its restriction to the coupled index set, so the displays leading there and the endpoint speak about one projective measurement. sum_poly_chainQ is eq:qld-pulling-9a itself: left-multiplying by Bob’s own pair measurement, which is the identity, refines the three-index family into the four-index one, and SimulPair.sum_poly_chainOp is the completeness that makes it so.

And eq:qld-pulling-10 down to its Cauchy–Schwarz step. That display runs over the four-index family and over the pairs whose outcomes disagree at the sampled point, and everything before the swap is now in. sum_snorm_sq_fiber_sandwich_subset_le is the outer shape on a subset of the index — the form the disagreeing pairs need, and the one the first display’s version is now a case of. bobTail_sandwich splits the sandwich across the cut and bobHat_conj_bobChainOp identifies Bob’s factor as his sandwiched pair-measurement marginal bobSand tensored with his Weyl outcome.

sum_snorm_sq_chainQ_disagree_le is then the relaxation, which is where the paper’s “\(\leq \)” sits: each disagreeing pair contributes one term of a sum over all outcomes that the pair’s own value excludes, the rest of that sum is nonnegative, and the constraint tying the outcome to the index may then be dropped. Note what is not used: no Cauchy–Schwarz, no measurement property beyond projectivity — only that a sandwich is nonnegative. sum_qform_bobTail_eq closes the reduction at eq:qld-pulling-13a: Alice’s whole family and Bob’s Weyl outcome both sum to the identity, so what is left carries neither, and the bound is a statement about Bob’s registers alone.

And the swap, which completes eq:qld-pulling-10. The chain’s only Cauchy–Schwarz, and the one step where the existing package did not fit. abs_sum_qform_swap_le measures the two placements’ deviation bare; this display sandwiches a projector with the measurement it swaps, and the deviation has to be read through that projector, because the index runs over pairs of a pair outcome and a point outcome and the bare form would pay one deviation per pair outcome — a factor of the number of polynomials. abs_sum_qform_swap_proj_le is the same argument with the Cauchy–Schwarz taken against the projector’s own form, which is legitimate because a projector is \(S^*S\), so no square root is needed; abs_sum_qform_conjTranspose_mul_le is the summed Cauchy–Schwarz it uses, the existing one assuming the first family self-adjoint.

SimulPair.abs_sum_qform_ne_swap_le is eq:qld-pulling-13 itself, stated on a SimulPair because that is where both placements are local — the one that sandwiches is the first party’s own, the one that replaces it the second party’s — and the mirror then makes it Bob’s. sum_qform_ne_eq reads the swapped side back as a Born probability, the other party’s point measurement summed over the outcomes its own value excludes being the complement of that value, and sum_uniform_qform_ne_le is eq:qld-pulling-10 complete, at \(\delta _S + 2\sqrt{172\varepsilon }\). The average over the sampled point goes inside the square root by Cauchy–Schwarz against the constant one (sum_weighted_sqrt_le).

And eq:qld-pulling-11. bobLift is any operator of Bob’s extended by the identity on the half of the pair he holds — both remaining displays sandwich the four-index family with one of these, and only which one differs, so bobLift_sandwich_kron and sum_qform_bobLift_eq serve both. sum_snorm_sq_chainQ_agree_le is the display and sum_uniform_snorm_sq_chainQ_agree_le its cost, which is item 2 of Lemma 3.74 at the second cut — available with no new proof, the mirror of a MirrorSimul being a MirrorSimul, and the swapped strategy’s hypotheses coming from swapVec_unit and povmValue_swapped_le. bornProb_physVec_bOp is the bridge those two run through: the mirror image of bornProb_physVec_aOp, carrying an operator that is Bob’s alone back to the state the second cut describes.

And eq:qld-pulling-12, which is the last of the eleven. The chain’s constraint is an equality of polynomial values at the sampled point; passing to equality of the polynomials themselves discards only the tuples where distinct polynomials happen to agree there, and Schwartz–Zippel bounds that by \(md/q\). sum_uniform_chainCoupled_agree_le is that bound at one pair of index pairs and sum_uniform_chainCoupled_mass_le the weighted form, with sum_uniform_snorm_sq_chainQ_notCoupled_le the display itself — the weights being the four-index family’s own Born probabilities, which sum to exactly one (sum_qform_chainQ).

Two things are worth recording. The polynomials compared are not the chain’s pair outcomes but those outcomes shifted by the Weyl outcomes’ encodings, \(g + g_h\) against \(g' + g_{h'}\), and the encoding is multilinear — so the sum keeps the individual-degree bound exactly when \(d \geq 1\), which is the lemma’s one hypothesis and the only place in the chain where a lower bound on \(d\) is needed. And chainQShift_eq_iff is where characteristic two is spent again: the condition the chain carries the shift on one side of is the condition Schwartz–Zippel wants it split across.

All eleven displays are now formalized, and so are the assembly’s two joints.

sum_snorm_sq_chain_le is the triangle inequality along a chain rather than across one step, and it is worth having rather than iterating sum_snorm_sq_triangle’: a chain of \(n\) steps costs a factor \(n\), not \(2^n\), because the total deviation telescopes into the sum of the steps’ and Cauchy–Schwarz against the constant one turns the squared norm of a sum of \(n\) terms into \(n\) times the sum of their squares. For eleven displays that is the difference between eleven and two thousand.

The other joint is between the groupings. Displays eq:qld-pulling-1 to -4 are local in the first cut’s grouping and everything from -5 on is local in the physical one. The matrix chain carried each of the first four across by lifting it through a regrouping of the appended pair; here the first cut and the physical model are two readings of one state model, so the first four terms enter the physical chain as they stand (SimulPair.chainS at the first cut), their operators read by the first cut’s reading lemmas.

And the first step of the chaining, which is the one that had to be read off the paper rather than the Lean. eq:qld-pulling-4 is the step that brings the second pair’s outcome into the chain, and the pair it is about is the appended one — the paper writes \(|\hat\psi \rangle = \sum _{h'} (\tau _{h'})_{\textsc{B}'} \otimes (\tau _{h'})_{\textsc{B}''} |\hat\psi \rangle \), and in the physical grouping both of those halves are Bob’s. So the matched projectors are one operator of his (bobPairProj), not a cross-party pair, and the step is the statement that it fixes the physical state (sum_bobPairProj_mulVec). SimulPair.sum_ancProj_mulVec, which an earlier note here called this display, is the same fact for the first pair and belongs to eq:qld-pulling-3a. The two are genuinely different steps about different pairs, and the registers had to be checked against qld-separating.tex to see it.

What makes the new one go through is the mirror identity of the second player’s pair in the physical model (Definition 3.62): on the physical state the matched Weyl projectors act as the projector on one half alone — the projectors being symmetric matrices — and those sum to the identity (bobPairProj_eq, sum_bobPairProj_mulVec).

And the chaining has started. SimulPair.chainS names the four terms displays eq:qld-pulling-0 to -3 run through, on the first cut, and the three lemmas after it are those displays read as bounds on consecutive deviations — the form sum_snorm_sq_chain_le consumes. Two of the three are the displays applied verbatim; the middle one is free, eq:qld-pulling-2 and -2b being identities (chainS_one_eq_two).

And the chain’s four free steps, which are one step. Displays eq:qld-pulling-3a, -3b, -4 and -5 are all “\(\approx _0\)” or identities, so the chain pays nothing between -3 and -5 and there is no reason to name the three terms between them: SimulPair.chainS_three_mulVec followed by MirrorSimul.chainS3b_mulVec is the whole stretch at once.

What runs through all four is one fact about a maximally entangled pair, used on each of the two pairs in turn: the projector on one half is the projector on the other, on the state. SimulPair.ancProj_mulVec_mVec is that for the pair \(\textsc{A}'\textsc{A}''\), read on the first cut, and MirrorSimul.bobPairProj_mulVec is the same for the pair \(\textsc{B}'\textsc{B}''\), which the physical model gives to Bob entire; both are the mirror identities of the physical state.

Given that, both halves of the step are the same two lines. Insert the projector on the half the chain does not carry; it commutes with everything between it and the state, so it may be moved next to the one the chain does carry, where it is absorbed; and now the point measurement beside it is the hatted point measurement cut down by that projector (hatMats_mul_proj, which is eq:qld-pulling-3b and was already in the tree). SimulPair.ancB_ptA_mulVec is Alice’s half and MirrorSimul.bobPt_mul_bobPairProj is Bob’s. The asymmetry between the two — Alice’s is an identity on the state and Bob’s an identity of operators — is only that Bob’s matched pair is already there, eq:qld-pulling-4 having put it there.

Nothing has to carry the first of the two across: eq:qld-pulling-3a and -3b are local in the first cut’s grouping, and an identity on the first cut’s state is an identity on the physical state, the two being one vector.

And the chaining, which is done. MirrorSimul.chainT is the chain on the physical model: ten terms for nine steps, the four of eq:qld-pulling-0 to -3 entering as the first cut’s terms and everything from -5 on entering directly. Three of the nine steps are free — eq:qld-pulling-2 and -2b, then -3a to -5, then -9a — and the six that are not cost, in order: item 1 of Lemma 3.74, the game’s point–point consistency, item 2 of Lemma 3.74, eq:qld-pulling-10 complete, item 2 again at the second cut, and Schwartz–Zippel. sum_uniform_snorm_sq_chainT_le is their sum at the factor nine that sum_snorm_sq_chain_le charges, and sum_uniform_snorm_sq_mTildeAnc_endOp_le is eq:qld-pulling-cons for Alice: her exact Pauli measurement on \(\textsc{A}\textsc{A}' \textsc{A}''\) is within \(9(10 \delta _S + 860 \varepsilon + 2\sqrt{172 \varepsilon } + md/q)\), in summed squared state distance, of the chain’s endpoint.

The one cost the displays did not already supply is eq:qld-pulling-3’s. SimulPair.sum_uniform_xSqNorm_pt_le supplies it: the game’s point–point consistency, read on the model the chain runs on rather than on the strategy’s own. That reading is free, for the reason the whole SimulPair interface exists — the register model embeds in the first cut carrying every expectation, and the strategy’s model embeds in the physical model with the registers inert — but it has to be done once (bornProb_mVec_ext, xSqNorm_mVec_ext).

And the lemma, which is now proved. Two steps after the chain, and neither is a new derivation.

Bob’s half is Alice’s at the mirror. MirrorSimul.mirror makes the mirror a MirrorSimul again, its physical model is this one with the players exchanged, and sum_coupledIdx_swap says its endpoint is this one read from the other side — which is swap_mem_coupledIdx, the symmetry of the index set that is the whole reason this lemma holds. snorm_sub_endOpMirror carries the norm across the exchange of the blocks, and sum_xSqNorm_le_of_endOp, in the tree since the endpoint was named, puts the two halves together: sum_selfConsGap_le is the two exact Pauli measurements agreeing.

From the measurements to the observable. This is the one place where the obvious route is the wrong one. Lemma 3.44 applied to the whole outcome set costs a factor \(q\), which would turn the chain’s \(md/q\) into \(md\) and lose the lemma. The paper coarse-grains first, along the character the observable reads — free for projective families, and in the tree as sum_xSqNorm_fibre_le — and turns only the resulting two-outcome family into an observable. So the factor is two, and snorm_sq_obs_sub_le is Lemma 3.44 in the state-norm form that step takes. MirrorSimul.snorm_sq_wTilde_le is the lemma. reports/qld-stage5-blueprint-repairs.md records the omission that created this node.

[\(\bullet \bullet \bullet \) hard]

Comments.

Both items are formalized, relative to one auxiliary state, with nothing assumed beyond the game: MirrorSimul.swap_isometry in MIPRE/Background/QLD/SwapItemTwo.lean. The isometry is MirrorSimul.swapPhi, a local isometry of the strategy’s model in the vocabulary of QLD.Extraction: the inert embedding of the model into its physical model, the conjugation by the two swap unitaries (adV), and the regrouping unassoc into item 1’s cut, read in the auxiliary state. It carries the strategy’s state to the swapped physical state regrouped, endState, by definition, item 1 compares that with the register model’s state tgtState, and the summands of item 2 are the physical model’s state norms of the conjugated Pauli measurement minus the honest projector (stateSqNorm_swapPhi_alice, stateSqNorm_swapPhi_bob). The history below is kept because it records where the obstacles were. The exact pieces are in MIPRE/Background/QLD/SwapUnitary.lean, item 1’s assembly in MIPRE/Background/QLD/SwapState.lean and MIPRE/Background/QLD/SwapItemOne.lean, and item 2’s threading in SwapItemTwo.lean.

The Lean statement has two constants where the statement above has one: item 1 is bounded by etaItemOne, which is \(2 - 2\sqrt{1 - \eta }\) with \(\eta = 2\sqrt{X} + 2X\) for the constant \(X\) of Lemma 3.76, and item 2 by deltaItemTwo at that bound, which is \(2\bigl( 11 \delta ' + md/q + 2 \sqrt{\texttt{etaItemOne}} \bigr)\), where \(\delta '\) (deltaLegs) bounds each leg of eq:qld-unitary-5. The error of Theorem 3.38 is built from the two: item 2’s bound plus the square root of item 1’s, capped at \(4\) (Lemma 3.78). Item 2’s distance is the register model’s summed squared state norm, which in the tensor-product model is \(\sum _h \left\| {(V M^{(\textsc{Pauli},W)}_h V^\dagger - I\otimes \tau ^W_h) |\textsc{aux}\rangle \otimes |\textsc{EPR}_q\rangle ^{\otimes M}} \right\| ^2\). That this has the shape Theorem 3.38 asks for is Lemma 3.78 (errSmall_swapItemOne and its companions in MIPRE/Background/QLD/ErrorShape.lean).

Every operator in the construction has the shape \(\sum _p \widehat{S}_p \otimes T_p\) (sTensor), and because \(\widehat{S}\) is projective these compose factorwise (sTensor_mul). That one lemma is where projectivity is used, and it makes the rest arithmetic: the swap map swapU is unitary on both sides (swapU_mul_conjTranspose, swapU_conjTranspose_mul), and conjugation by it strips the measurement off the observable, swapU_conj_wTilde_X and swapU_conj_wTilde_Z being \(V \tilde{W}^e(\tilde{u}) V^\dagger = I\otimes \tau ^W(e \tilde{u})\) exactly. The two signs cancel there because the sign the first factor carries is the very phase the ancilla factor’s conjugation produces (uOf_conj_wX, uOf_conj_wZ).

The estimate rests on an identity about the Weyl system with no measurement in it: twirl_mul_twirl is \(\bigl( \mathop{\mathbb {E}}_{\tilde{u}} \tau ^X(\tilde{u}) \otimes \tau ^X(\tilde{u}) \bigr) \bigl( \mathop{\mathbb {E}}_{\tilde{v}} \tau ^Z(\tilde{v}) \otimes \tau ^Z(\tilde{v}) \bigr) = \bigl( |\textsc{EPR}_q\rangle \langle \textsc{EPR}_q| \bigr)^{\otimes M}\). The paper proves it by an induction over the \(M\) qudits, having presented the ancilla as an iterated tensor product; here \((\mathbb {C}^q)^{\otimes M}\) is one matrix algebra indexed by \(\mathbb {F}_q^M\), so it is a single entry computation and the induction disappears.

The arithmetic that turns the two near-invariances into the closeness is norm_sub_sq_le_of_re_inner_ge, re_inner_ge_of_two_close and norm_sub_normalize_sq_le, and it is the repaired chain: the pinned paper bounded \(\left\| {(H_W - I) v} \right\| \) by \(\delta _S\) where its own preceding display gives \(\delta _S\) for the square, and compared a squared triangle inequality with \(2\sqrt{\delta _S}\) where the bound on the square is \(4 \delta _S\). The conclusion \(O(\sqrt{\delta _S})\) is unchanged; only intermediate constants move. re_inner_ge_of_two_close concludes exactly the paper’s \(1 - 2\sqrt{\delta _S} - 2\delta _S\), and it carries a case split the paper does not: a statement with no hidden “for small enough \(\delta _S\)” has to handle \(\delta _S {\gt} 1\), where squaring \(1 - \sqrt{\delta _S}\) would reverse the inequality and where the trivial bound is already stronger.

The assembly is done. exists_auxVec_close is item 1: a unit state on \(R \times (T \times T)\) — the two parties’ non-ancilla registers as one index, their two ancilla halves adjacent — that is nearly invariant under both Weyl twirls is within \(2 - 2\sqrt{1 - \eta }\) of a product \(|\textsc{aux}\rangle \otimes |\textsc{EPR}_q\rangle ^{\otimes M}\), with \(\eta = 2\sqrt{\delta } + 2\delta \), which is \(O(\sqrt{\delta })\) as the proof above says. Two things made it shorter than expected. The twirl is a projection (twirl_mul_self), not merely a contraction: the Weyl family is a homomorphism, so the double average collapses, for each \(s\) there being exactly \(q^n\) pairs \((u,v)\) with \(u + v = s\). That supplies the contraction hypothesis of norm_sub_sq_le_of_re_inner_ge through snorm_le_one_of_proj, with no operator-norm estimate anywhere. And the range of \(I\otimes |\textsc{EPR}\rangle \langle \textsc{EPR}|\) consists of product vectors by inspection (bOp_eprProj_mulVec), which is where \(|\textsc{aux}\rangle \) comes from — no partial trace and no Schmidt decomposition.

And three of item 2’s displays. Conjugation carries the exact Pauli measurement to the bare syndrome projector exactly, not just the observable: that is eq:qld-unitary-6, swapU_conj_mTilde, and at the interface SimulPair.swapU_conj_mTildeAt. What makes it work is one mechanism, recorded on its own because the observable’s proof did not need it: the twisted commutation relation says conjugation multiplies each Weyl operator by a character, and on the projectors that is a shift — a spectral projector is the Fourier average against a character, and two characters compose by adding their labels (conj_proj_of_sign), so a syndrome projector’s outcome moves by the shift’s own pairing with the probe (conj_syn_of_sign). In \(\tilde{M}^{W,u}_a\) the outcome carried at the pair outcome \(p\) is \(\mathrm{Coded}(g_{\pi p}) \cdot u + a\) and the shift is \(\mathrm{Coded}(g_{\pi p})\), so the two cancel in characteristic two and the pair outcome disappears. That cancellation is the paper’s relabelling \(h' = h + \mathrm{Coded}(g_W)\), the passage its cnote records as repaired; what makes it exact here is that the shift and the outcome are written with the same \(\mathrm{Coded}(g_{\pi p}) \cdot u\) by construction.

The endgame’s opening expansion is sum_snorm_sq_sub_eq_two_sub (eq:qld-unitary-7): the two families compared there act on the same party, so the bipartite one_sub_sum_bornProb_eq does not apply, but the same three-term expansion does. And its one estimate, eq:qld-unitary-8, is Schwartz–Zippel in the packaging eq:qld-pulling-12 already used (sum_uniform_agree_bornProb_le): the index is a pair of Pauli outcomes and the diagonal is excluded by the weight rather than by the index set, which is why sum_uniform_agree_mass_le now asks for the two polynomials to be distinct only where the weight is nonzero.

And the endgame’s own steps, in SwapEndgame.lean. Item 1 leaves a product state \(|\textsc{aux}\rangle \otimes |\textsc{EPR}_q\rangle ^{\otimes M}\), and what the endgame does to it is elementary once said plainly: an operator on the entangled pair acts on the second factor and leaves the first (bOp_mulVec_auxVec, one entry computation), so two operators that agree on \(|\textsc{EPR}_q\rangle ^{\otimes M}\) agree on the product (mulVec_auxVec_congr). That is eq:qld-unitary-7’s last line, where a generalized Pauli’s spectral projector moves from one half of the pair to the other: the projectors are symmetric, being real Fourier averages of a symmetric family, so stateVec_epr_proj moves them across and mulVec_auxVec_proj carries that to the product state (mulVec_auxVec_syn for the syndrome projectors). The display’s first two lines are sum_snorm_sq_sub_le_of_agree: everything after them is a lower bound on one number, the agreement, and the deviation is twice its deficit. And sum_uniform_bornProb_fibre_le is eq:qld-unitary-8 in the form the chain consumes: reading the two families at the value of the encoding at the sampled point rather than at the full outcome raises the agreement by at most \(md/q\), the pairs it adds being the distinct ones whose encodings collide there.

And item 1’s cut, which holds both pairs. exists_auxVec_close concludes about \(|\textsc{EPR}_q\rangle ^{\otimes M}_{\textsc{A}'' \textsc{B}''}\) — one half of each party’s local pair — whereas the register model of one run of stage 4 carries only the pair \(\textsc{A}' \textsc{A}''\), read along the cut \(\textsc{A}\textsc{A}' \mid \textsc{B}\textsc{A}''\), and has no \(\textsc{B}' \textsc{B}''\) in it at all. That was deliberate and correct for Lemma 3.63 and Lemma 3.74, each of which uses one orientation at a time, and it is what reports/qld-stage5-blueprint-repairs.md records as the second entangled pair not being needed for Lemma 3.75’s item 1. Item 2’s threading is the first consumer that does need it. The physical model of Definition 3.62 holds both pairs, the two cuts of a MirrorSimul are readings of it (Lemma 3.76), and item 1’s cut is the register model, with the pair \((A'', B'')\), of the extension of the strategy’s model by the padded registers, into which unassoc regroups the physical model; qform_endVec carries an expectation between the two readings.

And the missing edge, made explicit. Item 1 asks for a near-invariance of the state under the Weyl twirl on its two ancilla halves; what Lemma 3.76 supplies is an agreement of the two parties’ exact Pauli observables averaged over a uniform probe. The twirl is by definition that average, so the two are one rewriting apart: qform_bOp_twirl. That this edge is short is not an accident — it is why the missing node was worth separating out rather than folding into Lemma 3.75.

And item 1 is now unconditional. The near-invariances were hypotheses of exists_auxVec_close; Lemma 3.76 supplies them, and MirrorSimul.exists_aux_close is item 1 with nothing assumed beyond the game’s. Three things had to be said to make the blueprint’s “one rewriting” go through, and each is worth naming.

The cut. The physical model puts the far half of each party’s own pair first among that party’s registers, and item 1’s cut puts the two far halves together as the register; the regrouping between them is unassoc, a local isometry with no condition on the state, and endState is the swapped physical state carried along it.

The conjugation, read backwards. swapU_conj_wTilde_X and _Z say the swap unitary strips the pair measurement off the exact Pauli observable exactly; read the other way (conj_inv_of_unitary) that turns an expectation of the honest Weyl operator on the swapped state into an expectation of the two parties’ observables on the state itself (MirrorSimul.qform_endState_weyl).

And the two involutions. Each party’s exact Pauli observable is self-adjoint and squares to one, so its cross-party deviation and its joint expectation determine each other exactly, the summed squared deviation being \(2 - 2\) times the joint expectation, with no inequality anywhere (MirrorSimul.bornProb_wTilde_ge).

And item 2 is threaded. MirrorSimul.sum_snorm_sq_aliceConjPauli_le is the chain for Alice, on any unit state \(\Delta \) that carries the pair on \(\textsc{A}'' \textsc{B}''\) and is within \(r\) of the swapped physical state. eq:qld-unitary-7 makes the deviation twice the deficit of an agreement; on \(\Delta \), \(\tau ^W_h\) on \(\textsc{A}''\) is \(\tau ^W_h\) on \(\textsc{B}''\), which makes that agreement a bipartite Born probability across the physical cut; eq:qld-unitary-8 coarse-grains it along \(g_h(u)\) at a cost of \(md/q\); and eq:qld-unitary-6 on Bob’s side turns the coarse honest projector into Bob’s exact Pauli measurement conjugated by his swap unitary (bobSwap_conj_bobMTilde). The transport across item 1 (sum_bornProb_conj_ge_of_close) moves the conjugation onto the state, where it undoes the swap, and costs \(2r\); with \(r\) the square root of item 1’s bound this is where \(\delta _S^{1/4}\) enters. The last step is eq:qld-unitary-5 at the mirror instance (sum_bornProb_physVec_ge): Bob’s exact Pauli measurement against Alice’s \((\textsc{Pauli}, W)\) reading is the second cut’s \(\tilde{M}\) against the swapped strategy’s Pauli reading. sum_snorm_sq_alice_le applies the chain at \(\Delta = |\textsc{aux}\rangle \otimes |\textsc{EPR}_q\rangle ^{\otimes M}\) read on the physical model (physAux, the register model’s state carried there by the associativity of item 1’s cut, which unassoc inverts: unassoc_W_physAux), for any \(|\textsc{aux}\rangle \) close to the swapped state. sum_snorm_sq_bob_le is Alice’s at the mirror, relative to the same \(|\textsc{aux}\rangle \): the mirror’s product state and its swapped physical state are this one’s with the parties exchanged (mirror_physSwap_mulVec), so no second auxiliary state is needed. One point of encoding: the Schwartz–Zippel packaging reads its index through coefficient tables of bounded individual degree, and ancPoly is the table of \(\mathrm{Coded}(h)\), faithful because the encoding is multilinear and \(d \geq 1\) (toMv_coeffTable).

And eq:qld-unitary-5. It needed no new estimate: its engine is the paper’s fact:triangle-for-simeq, already in Foundations as agreeSum_triangle (with \(11\delta \) for the paper’s \(9\delta \), as Lemma 3.65 records). Two adapters put it to work. inconsistency_triangle is the estimate in the vocabulary this interface states everything in — an inconsistency rather than an agreement, the two being the same number. The three legs are not read in the same model: \(\tilde{M}^{W,u}\) needs the ancilla half with the first party, which is the physical model, while the strategy’s own measurements live in its own model. They are read on the physical model with the registers inert (physInert), an embedding of models, along which every inconsistency is the same number. SimulPair.inconsistency_mTilde_pauli_le is then the display, with the two middle legs — the game’s point–point and point–Pauli consistencies, the latter read through pauliAtPOVM — as hypotheses, in the same way exists_auxVec_close takes item 1’s near-invariances. They are asked for in the form the game supplies them: an inconsistency of the strategy’s own measurements carried along that embedding is their inconsistency in the strategy’s own model, so inconsistency_mTilde_pauli_le’ takes them on \(|\psi \rangle \), where agree_subtest_le leaves them.

And those two legs are discharged. They are items 1 and 3 of Lemma 3.46 at the point and Pauli types — item_consistency and item_pauli_consistency, both already in — and three steps carry each into the form the triangle wants. The point question a content asks is the point the content carries, so the average over contents of a function of that point is the uniform average over points (sum_content_pt); and for projective families a cross-party deviation is exactly twice the inconsistency (inconsistency_eq_half_xPovmDist — only \(\leq \) holds for general POVMs, and what makes it an equality is that both families’ masses are exactly one). That gives inconsistency_pt_pt_le and inconsistency_pt_pauli_le at \(86\varepsilon \), which is agree_subtest_le’s \(172\varepsilon \) halved, and inconsistency_mTilde_pauli_le_of_win is then eq:qld-unitary-5 from the game’s soundness and item 1 of Lemma 3.75 alone.

And the endgame’s transport. abs_qform_withState_sub_qform_le: moving an expectation from the product state to the swapped physical state costs twice the operator’s bound times the distance between them. Item 1 bounds the squared distance, which is exactly where the fourth root in \(\delta _{qld}\) comes from. reports/qld-stage5-blueprint-repairs.md records the repairs above, including the ledger’s declared dependencies for node \(1.2.2.16\), which name \(1.2.2.4\) (Lemma 3.46) and which the uses list did not.

The error

Comments.

The paper takes the trivial bound outside the regime and enlarges \(a\) until the shape exceeds it; the formalization names the function the proof produces and proves that it has the shape, so the paper’s enlargement of \(a\) becomes a closure property (ErrSmall.of_cases). The lemma rests on the chain’s constants only, not on Theorem 3.38: the soundness of the test in a model (Definition 8.82) is stated at this function, and the theorem proves it.

MIPRE/Background/QLD/QLDError.lean names the bound, qldErr: \(\min (\texttt{qldBound}, 4)\) inside the regime and \(4\) outside. Here qldBound is item 2’s constant of Lemma 3.77 plus \(\sqrt{\eta _1}\), for item 1’s bound \(\eta _1\) on the squared distance: item 2 of Theorem 3.38 is item 2 of the lemma as it stands and \(\sqrt{\eta _1}\) is item 1’s distance, so qldBound dominates both (itemTwo_le_qldBound, sqrt_qldEta_le_qldBound). The cap \(4\) is the trivial bound: two unit vectors are within \(2\) of each other, and two projective measurements on a unit vector within \(4\) in summed squared state-dependent distance (BipartiteModel.sum_stateSqNorm_sub_le_four). le_qldErr is the interface the assembly of Theorem 3.38 uses: a quantity at most \(4\), and at most qldBound inside the regime, is at most qldErr. exists_qldErr_le is the closed form at \(\min (\varepsilon , 1)\), and Corollary 3.39 fixes its two constants once.

MIPRE/Background/QLD/ErrorShape.lean is the shape: ErrSmall says that a family of error terms is dominated by \(a(md)^a(\varepsilon ^b + q^{-b} + 2^{-bmd})\) with \(a \geq 1\) and \(0 {\lt} b {\lt} 1\) chosen before the parameters, on the range \(0 \leq \varepsilon \leq 1\), \(m, d \geq 1\), \(q \geq 2\). The range costs nothing: \(q \geq 2\) because \(q\) is the size of a field, and a failure probability above one may be read as one (ErrSmall.exists_le_min_one). The links of the chain are errSmall_deltaQ through errSmall_swapItemOne, the seeded soundness error enters through ErrSmall.deltaSim_comp, and not_errSmall_one guards the definition against being vacuous. ErrSmall.of_regime and ErrSmall.of_cases are the trivial bound outside the regime, needed for \(48md \leq q\) and for item 1’s smallness hypothesis. The divisibility \(4m \mid q\) that stage 4 needs is derived inside the regime, in Lemma 3.64.

3.7 Undecidability of the halting problem

[\(\checkmark \) (mostly) in Mathlib]

Source.

Turing (1936); in Mathlib as part of the Computability library.

Comments.

Listed to close the dependency graph: combined with the halting reduction (Theorem 6.214) it yields undecidability of approximating the game value, and \(\mathrm{RE}\)-completeness gives \(\mathrm{RE}\subseteq \mathrm{MIP}^*\).

3.8 Cook–Levin and succinct satisfiability

[\(\bullet \bullet \bullet \) hard]

Lean statement.

The theorem is the structure MIPRE.SAT.SuccinctCookLevin: the algorithm a polynomial-time function of the ambient model (PolyTimeFun) from \(((\mathcal{D}, n, T, Q, \sigma ), x, y)\) to circuits as data, “within \(T\) steps” read as cost at most \(T\) in the ambient model, the reading of every time bound of the pipeline, and the five items as fields. An earlier statement asked for a succinct description in the sense of Definition 2.42, which is a program answering bit queries and not the circuit the proof produces and the PCP consumes, and it carried none of the five items, all of which Lemma 6.147 and the PCP parameters depend on. The statement is validated by its consumer (MIPRE.SAT.DecoupledDescriber, Lemma 6.147) before its proof; the route to the proof is planning/succinct-cook-levin.md.

Formalization status.

Complete: statement and proof, the structure inhabited by MIPRE.SAT.succinctCookLevin (MIPRE/TM/CookLevin/). Three things the formalization settled against the first design, all recorded in planning/succinct-cook-levin.md. The index width has \(W = e + 4\), not \(e + 2\), because a position field must hold \(2S + 7\); the state field is \(\lceil \log |Q| \rceil \) bits rather than a fixed four. Two clauses beyond the tableau are needed: soundness needs answers of length at most \(T\), and the tableau alone admits answers of length up to \(2S\). And the canonical index of an answer cell of a free tape is its answer index, not its structured index — that is what ties the extension hypothesis on the first \(4T\) variables to the time-\(0\) row of the tape, and getting it wrong makes the soundness direction unprovable rather than merely awkward.

Two notes on the Lean, both about scale. The check circuit of the interpreter machine is the truth-table circuit of a fixed Boolean function on the window variables, so its gate count is \(7 \cdot 2^{|\mathrm{window}|}\) — an enormous constant, exactly as the paper’s lem:pack-check-size carries one. Nothing unfolds it, and nothing may: the defining terms of the state count and of the check circuit mention a cardinality and a truth table whose evaluation does not terminate in practice, so they are kept opaque (the state width is irreducible and the circuit is taken from an existential). And the program layer is written so that each of the fifty-odd family formulas costs one simp: a field record is a record of readers of the describer’s input whose evaluation is a structure literal of those programs’ own values, which makes every formula match its program definitionally.

Source.

Cook  [ 23 ] and Levin for the tableau reduction; Papadimitriou and Yannakakis  [ 22 ] for succinct representations and their complexity; the explicit form needed here is  [ 1 , Section 10 ] .

Comments.

This is the classical core of answer reduction: the players prove satisfiability of \(\varphi \) (arithmetized over a low-degree extension) instead of sending \((a,b)\). The statement is long but entirely combinatorial. Cook–Levin has been formalized in other proof assistants; a Lean formalization with the explicit-uniformity guarantees above is a substantial but well-specified sub-project.

A caution on the construction, from the verification campaign  [ 33 ] and not checked here: in the Tseitin encoding of  [ 6 ] , which the explicit form of  [ 1 , Section 10 ] follows, the formula is reported to omit the output-wire conjunct, so that it is satisfiable for every input and the central equivalence of the construction fails as written. The statement above is end-to-end and so does not inherit the defect textually, but a formalization of it must supply what the repair needs: the output-wire conjunct, the out-degree-zero hypothesis that yields individual degree \(6\), and the exact variable count on which the later PCP parameters depend — none of which the statement currently fixes.

Source.

The tableau of  [ 1 , Section 10 ] and the standard argument of Cook  [ 23 ] ; the companion paper’s answer_reduction.tex (its lem:correct-tableau).

Comments.

The lemma is Cook–Levin for one fixed machine; the theorem applies it to a fixed interpreter machine for the decider’s program, and the succinct description is a circuit for the clauses of this formula — pieces S2 and S3 of planning/succinct-cook-levin.md. The interpreter machine (S2) is formalized: MIPRE.TM.Interp.U, with accepts_of_acceptsWithin and acceptsWithin_of_accepts (MIPRE/TM/Interp/Run.lean) — on the inputs \((\mathcal{D}, n, T, x, y, a, b)\) with \(\left\vert {a} \right\vert , \left\vert {b} \right\vert \leq T\), it halts having output exactly \(1\), within an explicit polynomial number of steps, if and only if \(\mathcal{D}\) accepts \((n, x, y, a, b)\) within cost \(T\). The local check circuit is a parameter of the formula, with its specification a hypothesis of the lemma, so that the lemma is proved once and the circuit supplied with the describer. The windows are five cells wide: a head at one of the middle three cells then sees, in the window, both the cell it leaves and the cell it reaches, and the clamped moves of an input head at the ends of the input are decided from the window alone.

3.9 Self-dual normal bases

[\(\bullet \bullet \) medium]

blue( Thomas: Is this needed? )

Source.

Items 1 and 2 of the paper’s lem:downsize_field (preliminaries.tex); ledger node 1.1.6.1.11, which also records that neither item needs normality or odd \(k\). The paper’s third item, compatibility of the downsized matrix map with \(\kappa \) (\(\kappa _{\mathrm{m}}(M)\kappa (v) = \kappa (Mv)\)), is not formalized here: it is wanted by the conditionally linear downsizing of Lemma 6.7, which is stated over \(\mathbb {F}_2\) and so has not needed it.

Comments.

These two identities are why the pipeline insists on self-duality rather than on an arbitrary basis: they make \(\kappa \) computable by the trace form, with no matrix inversion, and turn the trace form into the standard inner product on coordinates. They are also what collapses the Pauli phase index \(G_E \kappa (b)\) to \(\kappa (b)\) at \(G_E = I\) (ledger node 1.1.6.1.13).

Source.

Shoup’s deterministic irreducible-polynomial construction  [ 24 ] , and then the companion campaign’s own constructions. The attribution here used to name Lenstra’s isomorphism algorithm  [ 25 ] and the classical characteristic-\(2\) existence results, following the discussion in  [ 1 , Section 3 ] ; the campaign has since proved both steps — ledger node \(1.1.6.1.6\) discharges the normal-basis construction contract “formerly attributed to Lenstra” and node \(1.1.6.1.8\) the self-dualization contract “formerly attributed to Wang” — and the Lean development now proves the remaining Shoup construction as well.

Comments.

Needed so that verifiers can do field arithmetic over \(\mathbb {F}_{2^k}\) using only \(\mathbb {F}_2\)-data (the “downsize” maps), uniformly and deterministically. This is why field sizes are restricted to \(q = 2^k\), \(k\) odd (“admissible”). Self-contained algebra/algorithmics; independent of everything quantum. Two consumers now name it: the admissible field with a bit representation that Theorem 6.164 takes as a parameter (MIPRE.SAT.BinField), and the downsized samplers of Lemma 6.7 once they move past field size \(2\).

The companion ledger retains its historical admission of Shoup’s construction at node \(1.1.6.1.1\). The Lean declaration MIPRE.LowDegree.exists_shoup_irreducible is now a theorem, proved by the explicit program of Lemma 3.103. Its input is the requested degree in unary, so the ambient bound is polynomial in the degree and includes printing all coefficient bits. The proof covers every positive degree in characteristic two, including powers of two, with fixed behavior at degree zero.

The complete effective self-dual normal-basis construction in SAT/EffectiveNormalBasis.lean composes this proved field constructor with the verified normal-element, inverse-Gram self-dualization, and multiplication-table programs. Fixed-space separation is performed directly in the cyclic algebra, as detailed in Lemma 3.108; this avoids materializing polynomial factors while implementing the primitive-projection argument. Exact axiom guards in MIPRE/Axioms.lean check the field constructor, the classical PCP decider, and this effective basis theorem against Lean’s standard axioms alone. This local proof does not rewrite the companion ledger’s events or discharge unrelated unfinished pipeline theorems.

Comments.

This is the self-dualization step of Lemma 3.87, and it is where oddness of \(k\) is used. If \(\alpha \) is a normal element of \(\mathbb {F}_{2^k}/\mathbb {F}_2\) with Galois group \(G\), the trace-form Gram matrix of its orbit is the circulant determined by \(c \in \mathbb {F}_2[G]\), \(c(g) = \mathrm{tr}(\alpha \cdot g\alpha )\): it is a unit, because the Gram matrix of a basis under the nondegenerate trace form is invertible, and it is fixed by the involution \(\tau \) induced by \(g \mapsto g^{-1}\), because that Gram matrix is symmetric. Replacing \(\alpha \) by \(a \cdot \alpha \) replaces \(c\) by \(a \cdot \tau (a) \cdot c\), so a self-dual normal basis is exactly a solution of \(a \cdot \tau (a) = c^{-1}\), which is what the lemma supplies. Nodes \(1.1.6.1.7\) and \(1.1.6.1.8\) carry an explicit circulant Gram manipulation instead; the argument above replaces it, and needs no factorization of \(X^k - 1\) and no norm computation in the factors.

What the lemma does not do is assemble a basis: the group algebra must be made to act on \(\mathbb {F}_{2^k}\), the Gram identity must be proved, and \(c\) must be shown to be a unit. Those three are bookkeeping, and Lemma 3.90 now carries them out; the algorithm is a separate matter again.

Scope.

This completes the square-root operation only. Computing the normal element, the inverse Gram element and the transported field tables remains part of Lemma 3.87.

Comments.

This is existence, not construction, so it is not Lemma 3.87 and does not discharge any ledger node: the normal element comes from Mathlib’s IsGalois.normalBasis, which is a theorem and not an algorithm, and nothing here is claimed to run in \(\mathrm{poly}(k)\). What it does settle is that the three bookkeeping items left open by Lemma 3.88 — making the group algebra act, the Gram identity, and unitness of \(c\) — are genuinely bookkeeping, and that the short self-dualization argument assembles. The formalization indexes the group algebra by \(G\) itself rather than by \(\mathbb {Z}/k\), which is what makes \(\mathrm{ofAlg}\) the inverse of Mathlib’s normalBasis.repr on the nose; the CommGroup instance comes from cyclicity, supplied locally.

Scope.

This generic normalization result is used by the complete irreducible-polynomial constructor in Lemma 3.103.

Scope.

The coordinate maps describe the semantics of the explicit coefficient programs. They do not enumerate a quotient or supply an abstract field conversion as an executable primitive.

Scope.

Computing a spanning family does not enumerate its binary linear combinations. The next lemma extracts and reconstructs the factors.

Source and audit.

This is the characteristic-two construction from Shoup  [ 24 ] , using the squarefree factorization oracle and the two prime-power branches before coprime assembly. Exact guards for the constructor and its effective consumers exclude the former Shoup axiom and any replacement nonstandard axiom. The companion ledger’s historical admission is unchanged.

Scope.

This is the addition and multiplication part of the effective-field node. Lemma 3.105 supplies element inversion and trace computation. Matrix algorithms, the normal-element construction and transport to a self-dual normal basis remain open. The supplied-modulus arithmetic and the uniform field constructor use only Lean’s standard axioms.

Scope.

These are element operations. Effective matrix construction, Lemma 3.108 constructs the normal element, and Lemma 3.109 supplies the effective self-dualizing basis change. They are composed in Lemma 3.87. Lemma 3.107 supplies the Frobenius matrix, inverse Gram computation and multiplication-table transport in any supplied basis. Lemma 3.106 supplies the binary matrix operations, elimination and solves.

Reducing the graph of the original matrix map and retaining the certificate component gives a linear projection onto its kernel. Its images of the standard basis are the computed kernel generators; they number exactly the input dimension and may include zero or dependent vectors.

Scope.

The normal-element construction remains separate. These programs supply the kernels, solves and matrix inverse needed by that construction. The field-matrix applications are assembled in Lemma 3.107.

Scope.

These programs consume a supplied basis. The self-dualizing basis change is assembled in Lemma 3.109; Lemma 3.108 constructs the initial normal element.

Implementation.

This performs the paper’s fixed-space separation directly in the cyclic algebra. It constructs the CRT projections without printing polynomial factors or calling polynomial gcd; no standalone binary squarefree-factorization algorithm is claimed.

Scope.

This constructs a self-dual normal basis from a supplied normal basis. Lemma 3.108 supplies that basis from unary \(k\), and Lemma 3.87 composes the complete algorithm.

Comments.

This removes the field parameter of Theorem 6.164 from the list of things this project assumes. It is deliberately weaker than Lemma 3.87: the basis is whatever Mathlib returns, so it is neither normal nor self-dual, there are no multiplication tables, and nothing is claimed about time. A consumer that needs \(\kappa \) to be computed by the trace form (Lemma 3.86) needs the self-dual normal basis, and MIPRE.SAT.BinField will have to carry more fields before it can be served; shaping that interface should wait until such a consumer exists.

3.10 The Schwartz–Zippel lemma

[\(\checkmark \) (mostly) in Mathlib]

Source.

[ 26 , 27 ] . A version is available in Mathlib (multivariate polynomials over finite fields).

Comments.

Used throughout the low-degree machinery (distance of the Reed–Muller code, soundness of arithmetization). Three shapes are formalized, because three consumers want three different ones: the probability bound \(d/q\) above; the individual-degree variant \(m d / q\), derived from Mathlib’s schwartz_zippel_sum_degreeOf rather than through the lossy \(\text{total degree} \leq m d\); and the univariate case as a count rather than a probability — two distinct polynomials of degree at most \(d\) agree at no more than \(d\) points — which is the form Lemma 3.22 uses. The probabilities are stated over \(\mathbb {R}\), which is where the low-degree machinery’s error terms live, rather than over Mathlib’s \(\mathbb {Q}_{\geq 0}\).

3.11 Approximating the value from below (\(\mathrm{MIP}^*\subseteq \mathrm{RE}\))

[\(\bullet \bullet \) medium]

Source.

Folklore; see  [ 1 , Section 12 ] , and statement (S) in the proof of cor:mip-re of recursive.tex for a complete argument. The statement was previously given for \(\mathrm{val}^{s}\) “and likewise for \(\mathrm{val}^*\)”; it is now the \(\mathrm{val}^*\) statement, which is the one the pipeline consumes (Remark 6.204) and the one the paper proves. The \(\mathrm{val}^{s}\) analogue needs its own enumeration and density argument, since rounding the entries of a synchronous strategy preserves neither projectivity nor synchronicity; it is not needed and not planned. Thresholds are nonnegative rationals written as fractions \(p/q\) of naturals, as in the paper’s (S), where \(t \in [0,1]\); a negative threshold is trivial since \(\mathrm{val}^*\geq 0\). In Lean the game description is HaltingGameValue.GameData (Definition 2.43), read as a game of the foundations by GameData.game, and recursive enumerability is Mathlib’s REPred, the domain of a partial computable function; integers travel as pairs of naturals, because Mathlib’s primitive recursion has no arithmetic on \(\mathbb {Z}\). The form the compressibility criterion consumes (its hypothesis that the complement of \(B\) is the halting set of a program, Lemma 4.11) is MIPRE.exists_semidecider_lt_quantumValue: for a computable family of game descriptions and a threshold \(p/q\), a well-scoped program of the ambient model halting exactly on the strings whose game has value greater than \(p/q\). It comes from the generic passage MIPRE.Cost.exists_semidecider from an REPred on bit strings to a program (Definition 2.41): a ToPartrec code for the predicate, translated into the model by Prog.ofCode, run after an ambient loop has shifted every bit up by one, since a ToPartrec code cannot see trailing zeros of its input and the bit \(0\) encodes as nil.

Comments.

The Lean route to the \(\mathrm{val}^*\) half departs from the paper’s proof of (S). The paper enumerates approximate candidates — tuples with entries in \(\frac1k \mathbb {Z}[i]\) satisfying relaxed POVM constraints, tested by positive semidefiniteness (Lemma 3.115) — and repairs each into an exact POVM by conjugating with \(T_x^{-1/2}\), with the explicit slack \(\Delta (d,k) = 250(\left\vert {\cal A} \right\vert + \left\vert {\cal B} \right\vert )^2 d/k\) (its Claims “Stability” and “Density”; ledger nodes 1.1.7.2.3 and 1.1.7.2.4). The formalization enumerates exact projective strategies instead: every projective measurement is \(U \Pi _a U^*\) for a unitary \(U\) and coordinate projections \(\Pi _a\), and up to a phase every unitary is the Cayley transform of a skew-Hermitian matrix, which is what gets rounded (Lemma 3.113). Every candidate is then a genuine strategy, so only the density half of the argument is needed, with no slack, no matrix square root and no positive-semidefiniteness test, and the biconditional of Lemma 3.114 is sharp. Lemma 3.115 is proved but no longer on the path (the ledger’s node 1.1.7.2.1, exact arithmetic and the decidability of the candidate test, is accounted for by the primitive recursive check itself); Lemma 3.116 is used as stated. The choice was made for the formalization’s sake — the stability claim needs the functional calculus for \(T_x^{-1/2}\) and the candidate test needs decidability of positive semidefiniteness over \(\mathbb {Q}(i)\), both heavier in Lean than the Cayley parametrization — and it proves the same statement (S); it reverses the route decision recorded in Finding 3 of planning/ledger-informed-plan.md, which is annotated accordingly.

Comments.

The lemma is the mathematical content of Lemma 3.112, isolated from the computability: only the right-hand side involves the enumeration. It accounts for the ledger’s stability and density nodes (1.1.7.2.3, 1.1.7.2.4) by a different proof, as explained under Lemma 3.112: stability is vacuous for exact candidates, and density is Lemma 3.113 plus the Lipschitz bound, whose constant \(4\left\vert {\cal A} \right\vert \left\vert {\cal B} \right\vert \) is crude and immaterial. The nonemptiness of the answer alphabets is what makes a strategy exist at all: with it \(\mathrm{val}^*\) is a supremum over a nonempty set, without it the supremum is \(0\) by convention and the equivalence fails for \(t {\lt} 0\). Game descriptions (Definition 2.43) always satisfy it. In Lean the data type ExactStrategy carries no proofs, so that the computability layer can enumerate it and test validity.

Comments.

This is the easy inclusion \(\mathrm{MIP}^*\subseteq \mathrm{RE}\) and one half of Theorem 7.6. The pipeline consumes only the \(\mathrm{val}^*\) half, as the semidecision procedure of Remark 6.204. The commuting-operator analogue (approximating \(\mathrm{val}^{\mathrm{co}}\) from above via the NPA hierarchy  [ 29 ] ) is not needed for the main theorem, but becomes relevant for the downstream consequences in Section 8.