The argument below is the paper proof, and the unrestricted Lean theorem now formalizes it directly. Let \(H\) be the submeasurement from Lemma 9.6, and fix an arbitrary polynomial \(h^* \in \mathcal{P}(m+1,q,d)\). Define a measurement \(H_{\mathrm{meas}} \in \mathrm{PolyMeas}(m+1,q,d)\) by

Then \(\sum _h (H_{\mathrm{meas}})_h = H + (I-H) = I\). Moreover,

Thus \(A_a^u \otimes I \simeq _\sigma I \otimes (H_{\mathrm{meas}})_{[h(u)=a]}\).

This is exactly 4, with 5.

This is not a separate paper assertion. It is the representation of the same estimate obtained by replacing the complete vertical-line measurement family with its underlying submeasurement family, which is the form needed in the degree-zero branch.

Let \(H\) be the pasted submeasurement constructed in Definition 9.13. Lemma 9.31 implies

Applying 3.20 to 7 and 3 gives

Since \(\sqrt{8m\varepsilon +4\delta }\le 3m(\varepsilon ^{1/32}+\delta ^{1/32})\) for \(\varepsilon ,\delta \le 1\), the total error is at most

which proves 1. The completeness claim is exactly Corollary 9.44.

The total variation distance is exactly the probability mass of the collision event for a uniformly random tuple, because the distinct-tuple distribution is the uniform distribution conditioned on landing in \(\mathsf{Distinct}_k\). A uniformly random tuple lies outside \(\mathsf{Distinct}_k\) only if two coordinates collide, so a union bound gives

and this bounds the total variation distance.

Compare \(1-\lambda ^d\) with \((1-\lambda )(1+\lambda +\cdots +\lambda ^{d-1})\) and use that \(d^{1/(d+1)} \le 2\).

Apply Lemma 9.9 pointwise to the spectral distribution of \(G\), and then use the concavity of \(a \mapsto a^{1/(d+1)}\). The displayed operator expression is the same quantity written in the eigenbasis of \(G\).

The compatibility calculation for the restriction and evaluation maps used in the construction of \(H\) expands the vertical restriction, the interpolation support condition, postprocessing, and averaging over indexed submeasurements.

Because \(G\) is projective, 3.36 identifies the assumed strong self-consistency of the outcome-level family with

Hence

by 12.

Since \(G_\bot ^x = I-G^x\),

so the claim is immediate from Lemma 9.16.

After expanding the fourth switcheroo term, the inserted complete part forms a positive contraction. The left and right Cauchy–Schwarz side conditions are therefore the corresponding sums of \(X_gX_g^\ast \) and \(X_g^\ast X_g\), where \(X_g=\sum _o G_{\bot }^x M_o^yG_g^xM_o^y\). Orthogonality of the projective slice family and the submeasurement inequalities for \(M\) and \(G_{\bot }\) bound both sums by the identity. These are precisely the two contraction witnesses used in the fourth-term switcheroo chain.

Let \(M = \mathbb {E}_y \sum _o M_o^y\). The error to bound is

We compare all four terms with \(\langle \psi \rvert G \otimes M \lvert \psi \rangle \).

For the first term in 15,

For the second term,

For the third term, first

This is the Cauchy–Schwarz estimate coming from 14. Next,

Here the error is bounded using 3. Then

again by strong self-consistency of \(G_g^x\). Since \(G\) is projective,

Finally,

Therefore

The fourth term in 15 is the Hermitian conjugate of the third term, so it satisfies the same bound. Summing the four errors gives

By 6,

Applying Lemma 9.19 to 21, with \(\{ M_o^y\} \) equal to the outcome family \(\{ G_h^y\} \), gives

where \(\theta _1 = 12\sqrt{\zeta } + 4\sqrt{\nu _{\mathrm{com}}}\). Applying Lemma 9.19 again to 22, now with the one-outcome family \(M_o^y = G^y\), gives

where \(\theta _2 = 12\sqrt{\zeta } + 4\sqrt{\theta _1}\).

Since \(\nu _{\mathrm{com}}=30m(\gamma ^{1/4}+\zeta ^{1/4}+(d/q)^{1/4})\), these errors satisfy

The identities

and

reduce both claims to Corollary 9.21.

For 23, split the outcome set into the genuine outcomes and \(\bot \):

by 3 and 9.17. For 24, the same decomposition yields four cases: polynomial–polynomial, \(\bot \)–\(\bot \), polynomial–\(\bot \), and \(\bot \)–polynomial. These contribute \(\nu _{\mathrm{com}}\) and three copies of \(\nu _2\), so

This is the monotonicity estimate for the completed part of \(\widehat G\): the completed contribution is one summand of the corresponding slice squared-distance defect, and the remaining summands are nonnegative.

The split identities follow from the completed-outcome equivalences. The normalization inequalities are the corresponding submeasurement bounds for the left and right half-products after reindexing the sums.

For the one-step commutation move, rewrite the relevant head–tail split, apply the self-consistency and commutation estimates for \(\widehat G\), and assemble the resulting comparison by the triangle inequality for \(\approx _\delta \).

Repeatedly move the leftmost factor across the remaining product, using 23 and 24 at each step and summing the resulting errors with 3.27. The paper’s calculation gives

The proof first identifies a failed vertical-line interpolation with a particular active coordinate whose slice value disagrees with the line answer. The operator sum over all such failures is then bounded by the sum of the corresponding one-coordinate line defects, using the vertical restriction identities above.

The proof compares the distinct-tuple average with the independent-tuple average, paying the total-variation cost from Proposition 9.8. The independent average separates into the one-coordinate line defects from the previous lemma, and the scalar inequality \(1/q\le (d/q)^{1/32}\) absorbs the sampling error into the stated pasting parameter.

Summing out the coordinates to the right of \(i\) gives

Write \(\widehat G_{g_{{\lt}i}}^{x_{{\lt}i}} = \widehat G_{g_1}^{x_1}\cdots \widehat G_{g_{i-1}}^{x_{i-1}}\). Then

The Cauchy–Schwarz argument uses

which is at most \(\nu _4\) by Lemma 9.27. A second Cauchy–Schwarz step gives

Summing over \(g_1,\dots ,g_{i-1}\) collapses the middle factor to \(I\), so 28 becomes

by 4. Thus the total error is

The inconsistency with \(B^u\) expands as

If \(|w|\ge d+1\) and \(f \ne h|_u\), then some active coordinate \(i\) must satisfy \(g_i \ne \bot \) and \(g_i(u)\ne f(x_i)\). Hence

Passing from independent tuples to distinct tuples costs at most \(k^2/q\) by Lemma 9.8. A union bound over the offending coordinate then gives

Therefore

Lemma 9.31 implies

Applying 3.20 to this relation and 3 gives

Since

the claim follows.

The proof transports the vertical-line consistency estimate to point evaluations and combines it with the good-strategy point-to-line comparison. The displayed numerical assumptions are used only to absorb the intermediate errors into the final parameter \(\nu \).

Corollary 9.32 gives

Corollary 9.44 bounds the missing mass of \(H\) by

Adding this completion mass to the \(\nu \)-bound gives

The completed measurement differs from the original submeasurement only at the fallback polynomial. The additional term is bounded by the missing-mass estimate and then added to the given point-consistency error.

Let \((y_1,\dots ,y_k)\sim \mathsf{Distinct}_k\). By definition,

We now remove the restriction to globally consistent tuples:

Since the right-hand side is at least the left-hand side, it suffices to bound the difference:

We next insert an indicator recording consistency along the sampled line:

The discarded part is

and after switching to independent tuples and applying Lemma 9.30 coordinatewise, this contributes at most \(k^2/q + k\nu _5\).

Let \(\mathsf{Consistent}_\tau (g,y,u)\) denote the event that there exists a degree-\(d\) polynomial \(f\) with \(f(y_i)=g_i(u)\) for all \(i\in \tau \). Then

so 35 is bounded by

For a fixed globally inconsistent tuple, choose \(d+1\) active coordinates and let \(h^*\) be the unique interpolant through them. Since the tuple is not globally consistent, some active coordinate \(i^*\) satisfies \(g_{i^*} \ne h^*|_{y_{i^*}}\), and then Schwartz–Zippel gives

Therefore 37 is at most \(md/q\), which proves 33. A final application of Lemma 9.8 replaces distinct tuples by independent tuples, giving a total error of

Every summand is a polynomial in the commuting positive operators \(G\) and \(I-G\), so \(S_{\tau _{\ge \ell }}\) is Hermitian and positive semidefinite. Summing over all prefixes gives

Splitting the next type bit according to whether \(\tau _\ell =1\) or \(\tau _\ell =0\) gives the stated recurrence.

For a type \(\tau \in \{ 0,1\} ^k\), write \(\tau _{{\lt}\ell }\), \(\tau _{{\gt}\ell }\), \(\tau _{\le \ell }\), and \(\tau _{\ge \ell }\) for the obvious truncations, and similarly for tuples \(g\). Also write

Then

and

Write \(\mathsf O_\tau = \mathsf{Outcomes}_\tau \). The main iterative step is that for each \(1\le \ell \le k\),

Iterating 40 for \(\ell =1,\dots ,k\) produces the Bernoulli polynomial

and the accumulated error is

This corrects the displayed arithmetic in the paper: the iterated adjacent estimate contributes \(k\) copies of the \(2\sqrt{\nu _4}\) term, and the definition of \(\nu _4\) already contains a factor \(k^2\).

To prove 40, define for each \(1\le \ell \le k+1\) and each tail type \(\tau _{\ge \ell }\),

Then 40 may be rewritten as

The operators \(S_{\tau _{\ge \ell }}\) are Hermitian and positive semidefinite, and

For any \(\tau _\ell \in \{ 0,1\} \),

Therefore, for every \(\tau _{{\gt}\ell }\),

Moreover,

because \(S_{\tau _{\ge \ell }}\) commutes with \(G\) and \((I-G)\) and is bounded by \(I\).

We now prove 42. Writing \(\widehat H\) as a sandwich of \(\widehat G\) operators and moving the rightmost \(\widehat G_{g_\ell }^{x_\ell }\) to the second tensor factor gives

The corresponding Cauchy–Schwarz bound is

The first square root is at most \(1\) because \(S_{\tau _{\ge \ell }}\le I\) and \(\widehat H\) is a submeasurement, and the second is at most \(2\zeta \) by 23.

Next, commute the leftmost \(\widehat G_{g_\ell }^{x_\ell }\) across the left half-sandwich:

The associated Cauchy–Schwarz estimate is

The first square root is bounded by \(\nu _4\) via Lemma 9.27, and the second by \(1\) since \(S_{\tau _{\ge \ell }}\le I\).

Continue commuting:

This time the Cauchy–Schwarz step is

By 46, the first square root is at most \(1\), and the second matches the first square root in 51, hence is at most \(\nu _4\).

Finally move the remaining \(\widehat G_{g_\ell }^{x_\ell }\) to the second tensor factor:

The omitted Cauchy–Schwarz bound reuses the first square root from 54 and the second square root from 48. Since \(\widehat G\) is projective,

which is exactly 42.

These are direct specializations of the two preceding construction theorems to the notation and numerical hypotheses packaged in the nontrivial-regime pasting context.

Let \(\rho \) be the reduced state of \(\lvert \psi \rangle \) on one prover’s subsystem, and write the eigendecomposition \(X = \sum _i \lambda _i \lvert v_i \rangle \langle v_i \rvert \). This defines a probability distribution \(\mu (i)=\langle v_i \rvert \rho \lvert v_i \rangle \), with

Equivalently, \(\mathbb {E}_{i\sim \mu }(1-\lambda _i)\le \kappa \), so Markov’s inequality shows that most of the spectral mass of \(X\) lies on eigenvalues at least \(\theta \):

For a scalar \(p \in [d/k,1]\), the quantity

is the probability of observing at least \(d+1\) successes in \(k\) Bernoulli\((p)\) trials. Applying the scalar Chernoff bound eigenvalue-by-eigenvalue therefore yields

Hence

Since \((1-b)(1-c)\ge 1-b-c\) for \(b,c\ge 0\), 59 implies

Finally, \(k \ge 2d/\theta \) implies \(d/k \le \theta /2\), hence \((\theta -d/k)^2 \ge \theta ^2/4\), which yields the claimed bound.

Lemma 9.37 gives

Lemma 9.40 turns the right-hand side into

up to error \(\nu _8\). Apply Lemma 9.43 with \(\theta = 1/(200m)\). Since \(k\ge 400md\), the hypothesis \(k \ge 2d/\theta \) is satisfied, and the resulting lower bound is

The paper then absorbs the approximation losses \(\nu _7+\nu _8\) into \(\nu \).