7 Self-improvement

Throughout this chapter, \((\psi ,A,B,L)\) is an \((\varepsilon ,\delta ,\gamma )\)-good symmetric strategy for the \((m,q,d)\) low individual degree test.

7.1 Non-projective Output

A large part of this chapter is devoted to proving Lemma 7.1, which is a slightly weaker form of the projective self-improvement theorem proved in Section 7.2. The key difference is that the output family \(H\) is only required to be a submeasurement, rather than a projective submeasurement. Once this non-projective statement is available, Theorem 4.4 upgrades \(H\) to a projective family without losing control of the four quantitative conclusions.

Compared with the projective theorem, the helper lemma records strong self-consistency using the explicit inequality from Definition 3.34, keeps the boundedness conclusion in terms of an auxiliary operator \(Z\), and produces a much smaller error parameter.

Lemma 7.1 Self-improvement with non-projective output

✓

Let \(G \in \mathrm{PolyMeas}(m,q,d)\) be a measurement with the following property:

(Consistency with \(A\)): On average over \(u \sim \mathbb {F}_q^{m}\),

\[ A^{u}_a \otimes I \simeq _{\nu } I \otimes G_{[g(u)=a]}. \]

Let

\[ \zeta = 100m\cdot \Big(\varepsilon ^{1/2} + \delta ^{1/2} + (d/q)^{1/2}\Big). \]

Then there exists \(H \in \mathrm{PolySub}(m,q,d)\) with the following properties:

(Completeness): If \(H = \sum _h H_h\), then

\[ \langle \psi \rvert H \otimes I \lvert \psi \rangle \geq (1-\nu )-\zeta . \]
(Consistency with \(A\)): On average over \(u \sim \mathbb {F}_q^m\),

\[ A^u_a \otimes I \simeq _{\zeta } I \otimes H_{[h(u) = a]}. \]
(Strong self-consistency):

\[ \sum _{h} \langle \psi \rvert H_h \otimes H_h \lvert \psi \rangle \geq \langle \psi \rvert H \otimes I \lvert \psi \rangle - \zeta . \]
(Boundedness): There exists a positive-semidefinite matrix \(Z\) such that

\[ \langle \psi \rvert Z \otimes I \lvert \psi \rangle -\mathbb {E}_{u} \sum _a \langle \psi \rvert A^{u}_{a} \otimes H_{[h(u)=a]} \lvert \psi \rangle \leq \zeta \]

and for each \(h \in \mathcal{P}(m,q,d)\),

\[ Z \geq \left(\mathbb {E}_{u} A^{u}_{h(u)}\right). \]

Proof ▶

Let \(T=\{ T_g\} \) and \(Z\) be the optimal solutions to the SDPs 25 and 26 given by Lemma 7.8. Then \(T\) is a measurement, and

\begin{align} \forall g \in \mathcal{P}(m,q,d): \qquad Z & \geq \left(\mathbb {E}_{u} A^{u}_{g(u)}\right), \label{eq:Z-greater-than-A}\\ T_g \cdot Z & = T_g \cdot \left(\mathbb {E}_{u} A^{u}_{g(u)}\right). \label{eq:swap-Z-for-A} \end{align}

For each \(u \in \mathbb {F}_q^m\), define \(H^u=\{ H_h^u\} _{h \in \mathcal{P}(m,q,d)}\) by

\[ H_h^u := A^u_{h(u)} \cdot T_h \cdot A^u_{h(u)}, \]

and let

\[ H_h := \mathbb {E}_{u} H_h^u. \]

The pointwise family \(H^u\) is a submeasurement because

\[ \sum _h H_h^u = \sum _a A_a^u \cdot \Big(\sum _{h:h(u)=a} T_h\Big)\cdot A_a^u \le \sum _a (A_a^u)^2 = I, \]

where the inequality uses that \(T\) is a measurement and the last identity uses that \(A\) is projective. Averaging over \(u\) gives

\[ \sum _h H_h = \mathbb {E}_{u} \sum _h H_h^u \le I, \]

so \(H\) is also a submeasurement and therefore lies in \(\mathrm{PolySub}(m,q,d)\).

Set

\[ \zeta _{\mathrm{variance}} = 24m\cdot \Big(\varepsilon + \delta + \frac{md}{q}\Big). \]

Lemma 7.9 below is the technical transfer from the averaged family \(H\) back to the sandwiched operators \(A^u_{h(u)}T_hA^u_{h(u)}\). We use it in the completeness, consistency, strong self-consistency, and boundedness estimates that follow.

We now verify the four conclusions of Lemma 7.1.

Proof of 1. The completeness of \(H\) is

\begin{align} \sum _h \langle \psi \rvert H_h \otimes I \lvert \psi \rangle & = \mathbb {E}_{u} \sum _h \langle \psi \rvert H^{u}_h \otimes I \lvert \psi \rangle \notag \\ & = \mathbb {E}_{u} \sum _h \langle \psi \rvert \bigl(A^{u}_{h(u)} \cdot T_h \cdot A^{u}_{h(u)}\bigr) \otimes I \lvert \psi \rangle . \end{align}

Grouping the polynomials according to their value at \(u\) gives

\begin{equation} \label{eq:group-by-point-value} \mathbb {E}_{u} \sum _h \langle \psi \rvert \bigl(A^{u}_{h(u)} \cdot T_h \cdot A^{u}_{h(u)}\bigr) \otimes I \lvert \psi \rangle = \mathbb {E}_{u} \sum _a \langle \psi \rvert \bigl(A^{u}_{a} \cdot T_{[h(u) = a]} \cdot A^{u}_{a}\bigr) \otimes I \lvert \psi \rangle . \end{equation}

We first move the leftmost copy of \(A^u_a\) across the bipartition:

\begin{equation} \label{eq:first-point-projector-transport} \eqref{eq:group-by-point-value} \approx _{2\sqrt{\delta }} \mathbb {E}_{u} \sum _a \langle \psi \rvert \bigl(T_{[h(u)=a]} \cdot A^{u}_{a}\bigr) \otimes A^{u}_{a} \lvert \psi \rangle . \end{equation}

The difference is bounded by Cauchy–Schwarz as in 37; the first factor is at most \(\sqrt{2\delta }\) by self-consistency of \(A\), and the second is at most \(1\) because \(T_{[h(u)=a]} \le I\). We next remove the remaining copy of \(A^u_a\) on Bob’s side:

\begin{equation} \label{eq:first-moved-completeness} \eqref{eq:first-point-projector-transport} \approx _{\sqrt{\delta }} \mathbb {E}_{u} \sum _a \langle \psi \rvert \bigl(T_{[h(u)=a]} \cdot A^{u}_{a}\bigr) \otimes I \lvert \psi \rangle . \end{equation}

The first Cauchy–Schwarz factor is at most \(1\) because the fiber operators form a submeasurement after grouping \(T\) by the value of \(h(u)\). Here the second Cauchy–Schwarz factor is

\[ \mathbb {E}_{u} \sum _{a\neq b} \langle \psi \rvert A^u_a \otimes A^u_b \lvert \psi \rangle , \]

which is at most \(\delta \) because \(A\) is self-consistent and projective. Reindexing by \(h\) and using 2,

\[ \eqref{eq:first-moved-completeness} = \sum _h \langle \psi \rvert \bigl(T_h \cdot \mathbb {E}_{u} A^u_{h(u)}\bigr) \otimes I \lvert \psi \rangle = \sum _h \langle \psi \rvert (T_h \cdot Z) \otimes I \lvert \psi \rangle = \langle \psi \rvert Z \otimes I \lvert \psi \rangle . \]

Thus

\begin{equation} \label{eq:h-versus-z-lower-bound} \sum _h \langle \psi \rvert H_h \otimes I \lvert \psi \rangle \geq \langle \psi \rvert Z \otimes I \lvert \psi \rangle - 3\sqrt{\delta }. \end{equation}

Since \(G\) is a measurement, 1 and Lemma 3.18 give

\[ \langle \psi \rvert Z \otimes I \lvert \psi \rangle \ge \mathbb {E}_{u} \sum _a \langle \psi \rvert A^u_a \otimes G_{[g(u)=a]} \lvert \psi \rangle \ge 1-\nu . \]

Therefore the completeness is at least \(1-\nu -3\sqrt{\delta }\), which is bounded below by \((1-\nu )-\zeta \).

Proof of 2. The inconsistency of \(H\) with \(A\) is

\begin{equation} \label{eq:point-consistency-expansion} \mathbb {E}_{u} \sum _{a \neq b} \langle \psi \rvert A^{u}_a \otimes H_{[h(u) = b]} \lvert \psi \rangle = \mathbb {E}_{u} \sum _{a, h: h(u) \neq a} \langle \psi \rvert A^{u}_a \otimes H_h \lvert \psi \rangle . \end{equation}

The theorem-side off-diagonal selection used for this ‘add-in-u‘ application is , and the corresponding left/right scalar quantities are and . The selected scalar chain for this specialization is recorded by . Apply Lemma 7.9 with \(\mathcal O=\mathbb {F}_q\), \(M=A\), and \(S_u=\{ (a,h):h(u)\neq a\} \). Then

\[ \eqref{eq:point-consistency-expansion} \approx _{4 \sqrt{\zeta _{\mathrm{variance}}}} \mathbb {E}_{u} \sum _{a, h: h(u) \neq a} \langle \psi \rvert \bigl(A^{u}_{h(u)} \cdot A^{u}_a \cdot A^{u}_{h(u)}\bigr)\otimes T_h \lvert \psi \rangle , \]

and the right-hand side is \(0\) because \(A\) is projective. Hence

\begin{equation} \label{eq:explicit-bound-for-A-consistency} \mathbb {E}_{u} \sum _{a \neq b} \langle \psi \rvert A^{u}_a \otimes H_{[h(u) = b]} \lvert \psi \rangle \leq 4 \sqrt{\zeta _{\mathrm{variance}}}. \end{equation}

Since

\[ 4\sqrt{\zeta _{\mathrm{variance}}} = 4 \sqrt{24 m \cdot \Big(\varepsilon + \delta + \frac{md}{q}\Big)} \le 20 m \cdot \Big(\varepsilon ^{1/2} + \delta ^{1/2} + (d/q)^{1/2}\Big) \le \zeta , \]

this proves 2.

Proof of 3. From the definition of \(H_h^u\) and the projectivity of \(A\),

\begin{align} H^u_h & = A^u_{h(u)} \cdot T_h \cdot A^u_{h(u)} = A^u_{h(u)} \cdot H^u_h \cdot A^u_{h(u)}, \label{eq:h-sandwich}\\ A^u_{h(u)} \cdot H^u_{h'} \cdot A^u_{h(u)} & = H^u_{h'} \cdot A^u_{h(u)} = \bigl(A^u_{h(u)} \cdot T_{h'} \cdot A^u_{h(u)}\bigr)\cdot \mathbf{1}\! \left[h(u) = h’(u)\right]. \label{eq:h-blt} \end{align}

The strong self-consistency expression is

\begin{equation} \label{eq:self-consistency-expansion} \sum _{h\in \mathcal{P}(m,q,d)} \langle \psi \rvert H_h \otimes H_h \lvert \psi \rangle = \mathbb {E}_{u} \sum _{h \in \mathcal{P}(m,q,d)} \langle \psi \rvert H_h^{u} \otimes H_h \lvert \psi \rangle . \end{equation}

Apply Lemma 7.9 with \(\mathcal O=\mathcal{P}(m,q,d)\), \(M=H\), and \(S_u=\{ (h,h):h\in \mathcal{P}(m,q,d)\} \). This gives

\begin{equation} \label{eq:add-point-conditioning} \eqref{eq:self-consistency-expansion} \approx _{4 \sqrt{\zeta _{\mathrm{variance}}}} \mathbb {E}_{u} \sum _{h \in \mathcal{P}(m,q,d)} \langle \psi \rvert \bigl(A^{u}_{h(u)} \cdot H_h^{u} \cdot A^{u}_{h(u)}\bigr) \otimes T_h \lvert \psi \rangle . \end{equation}

We next enlarge the sum from \(h'=h\) to all pairs \(h,h'\):

\begin{equation} \label{eq:enlarge-polynomial-sum} \eqref{eq:add-point-conditioning} \approx _{2\sqrt{\zeta _{\mathrm{variance}}} + \frac{md}{q}} \mathbb {E}_{u} \sum _{h, h' \in \mathcal{P}(m,q,d)} \langle \psi \rvert \bigl(A^{u}_{h(u)} \cdot H^{u}_{h'} \cdot A^{u}_{h(u)}\bigr) \otimes T_h \lvert \psi \rangle . \end{equation}

The added off-diagonal contribution is

\begin{align} \eqref{eq:enlarge-polynomial-sum}-\eqref{eq:add-point-conditioning} & = \mathbb {E}_{u} \sum _{h \neq h'} \langle \psi \rvert \bigl(A^{u}_{h(u)} \cdot H^{u}_{h'} \cdot A^{u}_{h(u)}\bigr) \otimes T_h \lvert \psi \rangle \notag \\ & = \mathbb {E}_{u} \sum _{h \neq h'} \langle \psi \rvert \bigl(A^{u}_{h(u)} \cdot T_{h'} \cdot A^{u}_{h(u)}\bigr) \otimes T_h \lvert \psi \rangle \cdot \mathbf{1}\! \left[h(u) = h’(u)\right], \label{eq:added-indicator} \end{align}

where the second equality is 11. To estimate 15, first replace the left copy of \(A^u_{h(u)}\) by \(A^v_{h(v)}\):

\begin{equation} \label{eq:swapped-u-for-v} \eqref{eq:added-indicator} \approx _{\sqrt{\zeta _{\mathrm{variance}}}} \mathbb {E}_{u,v} \sum _{h \neq h'} \langle \psi \rvert \bigl(A^{v}_{h(v)} \cdot T_{h'} \cdot A^{u}_{h(u)}\bigr) \otimes T_h \lvert \psi \rangle \cdot \mathbf{1}\! \left[h(u) = h'(u)\right]. \end{equation}

The corresponding Cauchy–Schwarz bound is

\begin{multline} \Big|\mathbb {E}_{u,v} \sum _{h \neq h'} \langle \psi \rvert \bigl((A^{u}_{h(u)} - A^{v}_{h(v)}) \cdot T_{h'} \cdot A^{u}_{h(u)}\bigr) \otimes T_h \lvert \psi \rangle \cdot \mathbf{1}\! \left[h(u) = h’(u)\right]\Big|\\ \leq \sqrt{\mathbb {E}_{u,v} \sum _{h \neq h'} \langle \psi \rvert \bigl((A^{u}_{h(u)} - A^{v}_{h(v)}) \cdot T_{h'} \cdot (A^{u}_{h(u)} - A^{v}_{h(v)})\bigr) \otimes T_h\lvert \psi \rangle }\\ \cdot \sqrt{\mathbb {E}_{u,v} \sum _{h \neq h'} \langle \psi \rvert \bigl(A^{u}_{h(u)} \cdot T_{h'} \cdot A^{u}_{h(u)}\bigr) \otimes T_h\lvert \psi \rangle \cdot \mathbf{1}\! \left[h(u) = h'(u)\right]}. \label{eq:swapped-u-for-cauchy-schwarz} \end{multline}

The first factor is bounded by \(\sqrt{\zeta _{\mathrm{variance}}}\) via Lemma 6.6, and the second by \(1\) because \(T\) and \(H^u\) are submeasurements.

Repeating the same argument for the remaining copy of \(A\) yields

\begin{equation} \label{eq:replace-second-point-conditioner} \eqref{eq:swapped-u-for-v} \approx _{\sqrt{\zeta _{\mathrm{variance}}}} \mathbb {E}_{u,v} \sum _{h \neq h'} \langle \psi \rvert \bigl(A^{v}_{h(v)} \cdot T_{h'} \cdot A^{v}_{h(v)}\bigr) \otimes T_h \lvert \psi \rangle \cdot \mathbf{1}\! \left[h(u) = h'(u)\right]. \end{equation}

The same intermediate estimate gives

\begin{equation} \label{eq:swapped-indicator-total-bound} \mathbb {E}_{u,v} \sum _{h \neq h'} \langle \psi \rvert \bigl(A^{v}_{h(v)} \cdot T_{h'} \cdot A^{v}_{h(v)}\bigr)\otimes T_h\lvert \psi \rangle \leq 1, \end{equation}

so Schwartz–Zippel bounds the indicator average by \(md/q\) and proves 14.

Using 11, the right-hand side of 14 is

\begin{equation} \label{eq:remove-point-projector} \mathbb {E}_{u} \sum _{h, h' \in \mathcal{P}(m,q,d)} \langle \psi \rvert \bigl(H^{u}_{h'} \cdot A^{u}_{h(u)}\bigr) \otimes T_h \lvert \psi \rangle . \end{equation}

Replace the remaining copy of \(A^u_{h(u)}\) by \(A^v_{h(v)}\):

\begin{equation} \label{eq:replace-final-point-conditioner} \eqref{eq:remove-point-projector} \approx _{\sqrt{\zeta _{\mathrm{variance}}}} \mathbb {E}_{u,v} \sum _{h, h' \in \mathcal{P}(m,q,d)} \langle \psi \rvert \bigl(H^{u}_{h'} \cdot A^{v}_{h(v)}\bigr) \otimes T_h \lvert \psi \rangle . \end{equation}

Here the first Cauchy–Schwarz factor is at most \(1\) because \(T\) and \(H^u\) are submeasurements, and the second is again bounded by Lemma 6.6. Finally move this last copy of \(A^v_{h(v)}\) to Bob’s side:

\begin{equation} \label{eq:move-over-v} \eqref{eq:replace-final-point-conditioner} \approx _{\sqrt{2\delta }} \mathbb {E}_{u,v} \sum _{h, h' \in \mathcal{P}(m,q,d)} \langle \psi \rvert H^{u}_{h'} \otimes \bigl(T_h \cdot A^{v}_{h(v)}\bigr) \lvert \psi \rangle . \end{equation}

Substituting 2, then 1, and finally the already proved bound 9, one obtains

\[ \eqref{eq:move-over-v} \ge \sum _h \langle \psi \rvert H_h \otimes I \lvert \psi \rangle - 4\sqrt{\zeta _{\mathrm{variance}}}. \]

Combining 13, 14, 23, and 24 gives

\[ \sum _h \langle \psi \rvert H_h \otimes H_h \lvert \psi \rangle \ge \sum _h \langle \psi \rvert H_h \otimes I \lvert \psi \rangle - 11 \sqrt{\zeta _{\mathrm{variance}}} - \sqrt{2\delta } - \frac{md}{q}. \]

The Lean formalization records this step as named internal bounds, starting with the structure and the exact residual-side expansion and then uses the proved lemma together with to recover the final helper-stage self-consistency conclusion. The theorem-level derivation is therefore not moved into an additional hypothesis. The paper’s arithmetic shows that the right-hand error is at most

\[ 57m\cdot \Big(\varepsilon ^{1/2} + \delta ^{1/2} + (d/q)^{1/2}\Big) \le \zeta , \]

which proves 3.

Proof of 4. The helper-stage boundedness quantity is

\[ \langle \psi \rvert Z \otimes I \lvert \psi \rangle -\mathbb {E}_{u} \sum _a \langle \psi \rvert A^{u}_{a} \otimes H_{[h(u)=a]} \lvert \psi \rangle . \]

The reindexing of the sum by \(h\) is the algebraic identity

\[ \sum _a A^u_a \otimes H_{[h(u)=a]} = \sum _h A^u_{h(u)} \otimes H_h, \]

whose averaged scalar form reads

\[ \mathbb {E}_u \sum _a \langle \psi \rvert \, A^u_a \otimes H_{[h(u)=a]}\, \lvert \psi \rangle = \mathbb {E}_u \sum _h \langle \psi \rvert \, A^u_{h(u)} \otimes H_h\, \lvert \psi \rangle . \]

Using \(\sum _a A_a^u=I\), the pointwise difference between the right-placed total \(I \otimes H.\mathrm{total} = \sum _h I \otimes H_h\) and the helper-agreement operator at \(u\) reindexes as the off-diagonal sum

\[ \sum _h I \otimes H_h - \sum _a A^u_a \otimes H_{[h(u)=a]} = \sum _h \sum _{a \neq h(u)} A^u_a \otimes H_h, \]

whose averaged scalar form reads

\[ \sum _h \langle \psi \rvert \, I \otimes H_h\, \lvert \psi \rangle - \mathbb {E}_u \sum _a \langle \psi \rvert \, A^u_a \otimes H_{[h(u)=a]}\, \lvert \psi \rangle = \mathbb {E}_u \sum _h \sum _{a \neq h(u)} \langle \psi \rvert \, A^u_a \otimes H_h\, \lvert \psi \rangle . \]

Combined with 9 this gives

\[ \langle \psi \rvert Z \otimes I \lvert \psi \rangle -\mathbb {E}_{u} \sum _a \langle \psi \rvert A^{u}_{a} \otimes H_{[h(u)=a]} \lvert \psi \rangle \le \langle \psi \rvert Z \otimes I \lvert \psi \rangle - \sum _h \langle \psi \rvert I \otimes H_h \lvert \psi \rangle + 4 \sqrt{\zeta _{\mathrm{variance}}}. \]

By 7, the right-hand side is at most \(3\sqrt{\delta }+4\sqrt{\zeta _{\mathrm{variance}}}\). Substituting the definition of \(\zeta _{\mathrm{variance}}\) and collecting terms gives

\[ 23m\cdot \Big(\varepsilon ^{1/2} + \delta ^{1/2} + (d/q)^{1/2}\Big) \le \zeta . \]

Together with 1, this proves 4.

Remark 7.2 Slackness-carrying self-improvement helper

The formalization records a strengthened helper theorem whose output carries the complementary-slackness equations used in the completeness chain. The previous top-level residual-domination assembly theorems have been removed: the full self-improvement conclusion is now stated only by the paper theorem below. Its proof follows the paper’s expectation-level total-difference transport route; issue #1642 records why the sharper generic operator-total strengthening is not supplied by the present route.

7.1.1 A Semidefinite Program

Lemma 7.3 Uniform SDP feasible witness

✓

The uniform primal family \(T_g=(2|\mathcal{P}(m,q,d)|)^{-1}I\) has total mass \((1/2)I\), and the dual operator \(Z=2I\) is positive semidefinite and dominates the identity.

Proof ▶

This is the elementary Slater-type feasible witness recorded in the basic self-improvement definitions.

Lemma 7.4 Explicit matrix feasible bounds

✓

In every concrete matrix realization, the uniform family \(T_g=(2|\mathcal{P}(m,q,d)|)^{-1}I\) has total mass \((1/2)I\). The dual operator \(Z=2I\) dominates the identity and satisfies \(Z-A_g\geq I\), hence \(Z\geq A_g\), for every polynomial \(g\). In the canonical block SDP, the corresponding block matrix is feasible, its slack block is \((1/2)I\), and the canonical dual slack for the same dual witness also dominates the block identity. More generally, dual feasibility implies positivity of \(Z\), since the averaged point operators \(A_g\) are positive semidefinite.

Proof ▶

The formal proof is the matrix specialization of the uniform SDP witness recorded in the basic definitions. The inequality \(A_g\leq I\) follows by averaging the point-measurement effects and using the submeasurement bound at each point.

Lemma 7.5 Matrix slackness output

✓

From a matrix-level strong-duality witness with complementary slackness of the shape asserted by Lemma 7.8, one obtains a complete measurement \(\{ T_g\} \), a feasible dual operator \(Z\), equality of the primal and dual objectives, and the equations \(T_gZ=T_gA_g\) for all \(g\). Lean isolates the saturated canonical optimal-pair output required from strong duality: a feasible canonical primal matrix, a dual-feasible operator with equal objective value, canonical complementary slackness, and vanishing of the extra canonical slack block. This datum gives the matrix-level slackness-carrying SDP statement, whose witness is already a complete matrix measurement, and is then transported to the abstract Section 9 statement without assuming \(I \le Z\). The displayed measurement witness is read directly from that abstract statement. The canonical saturation datum is now the only matrix-level input used to pass from strong duality to the abstract SDP statement. The paper-facing self-improvement helper consumes the resulting abstract SDP statement.

Proof ▶

The identity \(\sum _gT_g=I\) turns the optimal primal submeasurement into a measurement; Lean performs this completion before storing the matrix and abstract slackness statements. The zero-defect form \(T_g(Z-A_g)=0\) is equivalent, by distributivity, to the displayed equation \(T_gZ=T_gA_g\).

Remark 7.6 Removed residual-dominating construction theorems

Earlier Lean versions exposed top-level conditional construction theorems that combined the matrix slackness output with residual-dominating orthonormalization and QXP-repair inputs. These declarations have been removed. The matrix slackness material is retained only up to the slackness-carrying helper output, and the full projective-output conclusion is represented by the paper theorem MIPStarRE.LDT.SelfImprovement.selfImprovement.

Remark 7.7 Removed reduced SDP interface

Earlier Lean versions also contained a reduced theorem sdp proving only the measurement-total and dual-feasibility fragment used before strong duality was supplied, as well as dominance-carrying declarations with the auxiliary condition \(I\le Z\). These declarations have been removed, and they are not advertised as formalizations of Lemma 7.8. The active Lean route for Lemma 7.8 is the slackness-carrying statement sdp_statement_with_slackness.

Lemma 7.8 Dual SDP and complementary slackness

✓

Let

\[ A_g = \mathbb {E}_{u \sim \mathbb {F}_q^m} A^u_{g(u)}. \]

Then the primal is

\begin{align} \sup & \quad \sum _g \, \operatorname{Tr}(T_g \cdot A_g) \label{eq:primal-objective}\\ \text{s.t.} & \quad T_g \geq 0\qquad \forall g\in \mathcal{P}(m,q,d), \notag \\ & \quad \sum _g T_g \leq I, \notag \end{align}

and the dual is

\begin{align} \inf & \quad \operatorname{Tr}(Z) \label{eq:dual-objective}\\ \text{ s.t.} & \quad Z \geq A_g. \label{eq:dual-constraint} \end{align}

These semidefinite programs are dual to each other. Moreover there is an optimal pair of solutions \(\{ T_g\} \) to 25 and \(Z\) to 26 such that \(\sum _g T_g = I\) and

\begin{equation} \label{eq:slater} T_g Z \, =\, T_g {A_g},\qquad \forall g\in \mathcal{P}(m,q,d). \end{equation}

Proof ▶

Rewrite 25 in canonical block form. Let \(r\) be the dimension of the space on which \(A\) acts, let \(M = |\mathcal{P}(m,q,d)|\), and fix an ordering \(g_1,\ldots ,g_M\) of the polynomials. Consider

\begin{align} \sup & \quad \operatorname{Tr}(C^\dagger X) \label{eq:primal-canonical}\\ \text{s.t.} & \quad \operatorname{Tr}(D_{ij}^\dagger X) = b_{ij} \qquad \forall i,j\in \{ 1,\ldots ,r\} , \notag \\ & \quad X \geq 0, \notag \end{align}

where

\[ C = \sum _{i = 1}^M \lvert i \rangle \langle i \rvert \otimes A_{g_i}, \]

and, for \(i,j \in \{ 1,\ldots ,r\} \),

\[ D_{ij} = \sum _{k=1}^{M+1} \lvert k \rangle \langle k \rvert \otimes \lvert i \rangle \langle j \rvert , \qquad b_{ij} = \left\{ \begin{array}{rl} 1 & \text{if } i = j,\\ 0 & \text{otherwise}. \end{array}\right. \]

Writing \(X=\sum _{i,j=1}^{M+1}\lvert i \rangle \langle j \rvert \otimes X_{ij}\), the constraints say precisely that \(\sum _{i=1}^{M+1} X_{ii}=I\), hence \(\sum _{i=1}^{M}X_{ii}\le I\), and the objective is

\[ \operatorname{Tr}(C^\dagger X)=\sum _{i=1}^M \operatorname{Tr}(A_{g_i}\cdot X_{ii}). \]

Thus 29 is equivalent to 25 under the identification \(T_{g_i}=X_{ii}\).

The canonical dual is

\begin{align} \inf & \quad \sum _i\, z_{ij} b_{ij} \label{eq:dual-canonical}\\ \text{s.t.} & \quad \sum _{i,j} \, z_{ij} D_{ij} \geq C. \label{eq:dual-canonical-constraint} \end{align}

Since

\[ \sum _{i,j=1}^r z_{ij} D_{ij} = \sum _{k=1}^{M+1} \lvert k \rangle \langle k \rvert \otimes \left(\sum _{i,j=1}^r z_{ij}\lvert i \rangle \langle j \rvert \right) =: \sum _{k=1}^{M+1}\lvert k \rangle \langle k \rvert \otimes Z, \]

the constraint 31 is exactly \(Z\ge A_{g_i}\) for every \(i\), and the objective is \(\operatorname{Tr}(Z)\). In Lean, the latter statement is recorded as the trace-pairing identity

\[ \Re \operatorname{Tr}(D(Z)X)=\Re \operatorname{Tr}(Z) \]

for every feasible canonical primal matrix \(X\), where \(D(Z)\) denotes the block-diagonal canonical dual operator. Consequently the canonical primal-dual gap is the real trace pairing of \(X\) with the canonical dual slack \(D(Z)-C\). Since the real trace pairing of positive semidefinite operators is nonnegative, Lean also records the resulting weak-duality inequality for any feasible canonical primal and dual pair. Hence 30 is equivalent to 26.

Slater’s condition holds because

\[ T_g = \frac{1}{2M}\cdot I \qquad \forall g\in \mathcal{P}(m,q,d), \qquad Z = 2I \]

are strictly feasible for the primal and dual respectively. Therefore strong duality holds. For an optimal pair \((X,(z_{ij}))\) in canonical form, complementary slackness gives

\begin{equation} \label{eq:complementary-slackness} X\Big( \sum _{i,j} \, z_{ij} D_{ij} - C \Big) \, =\, 0. \end{equation}

We may assume that \(X\) is block diagonal. Translating 32 back to the variables \(\{ T_g\} \) and \(Z\) yields \(T_g(Z-A_g)=0\) for every \(g\) and \(S Z=0\), where \(S=I-\sum _gT_g\) is the slack block. The paper then treats this as forcing \(S=0\). The Lean development records this saturation as part of the canonical optimal-pair datum for the block SDP. The canonical calculation still uses the auxiliary expression matrixSdpComplementarySlacknessDefect to read off the polynomial blocks of 32. The matrix optimal-witness interface, however, stores the displayed equation \(T_gZ=T_gA_g\) directly; MatrixSdpOptimalWitness.primalMeasurement expresses \(\sum _g T_g=I\) as a complete measurement. The statement MatrixSdpStatementWithSlackness records this matrix-level strong-duality output and the abstract theorem sdp_statement_with_slackness specializes it to the paper’s self-improvement setting. The explicit Slater witnesses used above are isolated in Lemma 7.4 and separately recorded by matrixSdpStrictPrimalSubmeasurement, matrixSdpStrictDualWitness, and matrixSdpFeasibleBounds_canonical; the dual feasibility of \(2I\) follows from matrixAveragedPointOperator_le_one. The block-diagonal reduction is also recorded for arbitrary feasible canonical matrices: extracting the diagonal blocks preserves the objective and transfers canonical complementary slackness to the extracted paper primal submeasurement.

Lemma 7.9 Averaging over the evaluation point

✓

Let \(T=\{ T_h\} \) be an optimal solution of the primal SDP, let

\[ H_h = \mathbb {E}_{u \sim \mathbb {F}_q^m} A^u_{h(u)} T_h A^u_{h(u)}, \]

and set

\[ \zeta _{\mathrm{variance}} = 24m\cdot \Big(\varepsilon + \delta + \frac{md}{q}\Big). \]

Suppose \(M = \{ M^u_o\} \) is a submeasurement with outcomes in some set \(\mathcal O\). For each \(u \in \mathbb {F}_q^m\), let \(S_u\) be a subset of \(\mathcal O \times \mathcal{P}(m,q,d)\). Then

\[ \mathbb {E}_{u} \sum _{(o, h) \in S_{u}} \langle \psi \rvert M^{u}_o \otimes H_h \lvert \psi \rangle \approx _{4\sqrt{\zeta _{\mathrm{variance}}}} \mathbb {E}_{u} \sum _{(o, h) \in S_{u}} \langle \psi \rvert \bigl(A^{u}_{h(u)} \cdot M^{u}_o \cdot A^{u}_{h(u)}\bigr) \otimes T_h \lvert \psi \rangle . \]

The reduced variance-bound specialization keeps only the variance-bound consequence used later in the helper theorem; it is not itself the full formal counterpart of Lemma 7.9.

Proof ▶

We begin by expanding

\begin{align} \mathbb {E}_{u} \sum _{(o, h) \in S_{u}} \langle \psi \rvert M^{u}_o \otimes H_h \lvert \psi \rangle & = \mathbb {E}_{u,v} \sum _{(o, h) \in S_{u}} \langle \psi \rvert M^{u}_o \otimes H^{v}_h \lvert \psi \rangle \notag \\ & = \mathbb {E}_{u,v} \sum _{(o, h) \in S_{u}} \langle \psi \rvert M^{u}_o \otimes \bigl(A^{v}_{h(v)} \cdot T_h \cdot A^{v}_{h(v)}\bigr) \lvert \psi \rangle . \label{eq:expand-that-H} \end{align}

We claim that

\begin{equation} \label{eq:move-first-point-projector} \eqref{eq:expand-that-H} \approx _{\sqrt{2\delta }} \mathbb {E}_{u,v} \sum _{(o, h) \in S_{u}} \langle \psi \rvert \bigl(A^{v}_{h(v)} \cdot M^{u}_o\bigr) \otimes \bigl(T_h \cdot A^{v}_{h(v)}\bigr) \lvert \psi \rangle . \end{equation}

To show this, we bound the magnitude of the difference:

\begin{multline} \Big|\mathbb {E}_{u,v} \sum _{(o, h) \in S_{u}} \langle \psi \rvert \bigl(A^{v}_{h(v)} \otimes I - I \otimes A^{v}_{h(v)}\bigr) \cdot \bigl(M^{u}_o \otimes (T_h \cdot A^{v}_{h(v)})\bigr)\lvert \psi \rangle \Big|\\ \leq \sqrt{\mathbb {E}_{u,v} \sum _{(o, h) \in S_{u}} \langle \psi \rvert \bigl(A^{v}_{h(v)} \otimes I - I \otimes A^{v}_{h(v)}\bigr) \cdot (M^{u}_o \otimes T_h) \cdot \bigl(A^{v}_{h(v)} \otimes I - I \otimes A^{v}_{h(v)}\bigr) \lvert \psi \rangle }\\ \cdot \sqrt{\mathbb {E}_{u,v} \sum _{(o, h) \in S_{u}} \langle \psi \rvert M^{u}_o \otimes \bigl(A^{v}_{h(v)} \cdot T_h\cdot A^{v}_{h(v)}\bigr) \lvert \psi \rangle }. \label{eq:move-first-point-projector-cauchy-schwarz} \end{multline}

The first factor is controlled by summing over the value \(a = h(v)\):

\begin{align*} & \mathbb {E}_{u,v} \sum _{a \in \mathbb {F}_q} \langle \psi \rvert \bigl(A^v_a \otimes I - I \otimes A^v_a\bigr) \cdot \Bigl(\sum _{(o,h)\in S_u,\, h(v)=a} M^u_o \otimes T_h\Bigr) \cdot \bigl(A^v_a \otimes I - I \otimes A^v_a\bigr)\lvert \psi \rangle \\ & \le \mathbb {E}_{u,v} \sum _{a \in \mathbb {F}_q} \langle \psi \rvert \bigl(A^v_a \otimes I - I \otimes A^v_a\bigr)^2 \lvert \psi \rangle , \end{align*}

where the inequality uses that \(M^u\) and \(T\) are submeasurements. By Lemma 3.21 and the self-consistency of \(A\), this is at most \(2\delta \). The second factor is

\[ \mathbb {E}_{u,v} \sum _{(o,h)\in S_u} \langle \psi \rvert M^u_o \otimes H^v_h \lvert \psi \rangle , \]

which is at most \(1\) because \(M^u\) and \(H^v\) are submeasurements.

Next, we claim that

\begin{equation} \label{eq:move-second-point-projector} \eqref{eq:move-first-point-projector} \approx _{\sqrt{2\delta }} \mathbb {E}_{u,v} \sum _{(o, h) \in S_{u}} \langle \psi \rvert \bigl(A^{v}_{h(v)} \cdot M^{u}_o \cdot A^{v}_{h(v)}\bigr) \otimes T_h \lvert \psi \rangle . \end{equation}

Again, we bound the magnitude of the difference:

\begin{align} \label{eq:move-second-point-projector-cauchy-schwarz} & \Big|\mathbb {E}_{u,v} \sum _{(o, h) \in S_{u}} \langle \psi \rvert \bigl((A^{v}_{h(v)} \cdot M^{u}_o) \otimes T_h\bigr) \cdot \bigl(A^{v}_{h(v)} \otimes I - I \otimes A^{v}_{h(v)}\bigr) \lvert \psi \rangle \Big| \notag \\ & \leq \sqrt{\mathbb {E}_{u,v} \sum _{(o, h) \in S_{u}} \langle \psi \rvert \bigl(A^{v}_{h(v)} \cdot M^{u}_o \cdot A^{v}_{h(v)}\bigr) \otimes T_h \lvert \psi \rangle } \\ & \qquad \cdot \sqrt{\mathbb {E}_{u,v} \sum _{(o, h) \in S_{u}} \langle \psi \rvert \bigl(A^{v}_{h(v)} \otimes I - I \otimes A^{v}_{h(v)}\bigr) \cdot (M^{u}_o \otimes T_h) \cdot \bigl(A^{v}_{h(v)} \otimes I - I \otimes A^{v}_{h(v)}\bigr) \lvert \psi \rangle }. \notag \end{align}

The first factor is bounded by

\begin{align*} & \mathbb {E}_{u,v} \sum _h \langle \psi \rvert \Bigl(A^v_{h(v)} \cdot \sum _{o:(o,h)\in S_u} M^u_o \cdot A^v_{h(v)}\Bigr) \otimes T_h \lvert \psi \rangle \\ & \le \mathbb {E}_{u,v} \sum _h \langle \psi \rvert (A^v_{h(v)})^2 \otimes T_h \lvert \psi \rangle \le \mathbb {E}_{u,v} \sum _h \langle \psi \rvert I \otimes T_h \lvert \psi \rangle \le 1, \end{align*}

using first that \(M\) is a submeasurement, then that \(A^v_{h(v)} \le I\), and finally that \(T\) is a submeasurement (\(\sum _g T_g \le I\)). The second factor is exactly the same expression as in 37, hence at most \(\sqrt{2\delta }\).

Having moved both copies of \(A\) to the left-hand side, we next show that

\begin{equation} \label{eq:replace-left-point-conditioner} \eqref{eq:move-second-point-projector} \approx _{\sqrt{\zeta _{\mathrm{variance}}}} \mathbb {E}_{u,v} \sum _{(o, h) \in S_{u}} \langle \psi \rvert \bigl(A^{u}_{h(u)} \cdot M^{u}_o \cdot A^{v}_{h(v)}\bigr) \otimes T_h \lvert \psi \rangle . \end{equation}

The difference is bounded by

\begin{multline} \label{eq:replace-left-point-conditioner-cauchy-schwarz} \Big|\mathbb {E}_{u,v} \sum _{(o, h) \in S_{u}} \langle \psi \rvert \bigl((A^{v}_{h(v)} - A^{u}_{h(u)}) \cdot M^{u}_o \cdot A^{v}_{h(v)}\bigr) \otimes T_h \lvert \psi \rangle \Big|\\ \leq \sqrt{\mathbb {E}_{u,v} \sum _{(o, h) \in S_{u}} \langle \psi \rvert \bigl((A^{v}_{h(v)} - A^{u}_{h(u)}) \cdot M^{u}_o \cdot (A^{v}_{h(v)} - A^{u}_{h(u)})\bigr) \otimes T_h \lvert \psi \rangle }\\ \cdot \sqrt{\mathbb {E}_{u,v} \sum _{(o, h) \in S_{u}} \langle \psi \rvert \bigl(A^{v}_{h(v)} \cdot M^{u}_o \cdot A^{v}_{h(v)}\bigr) \otimes T_h \lvert \psi \rangle }. \end{multline}

The first factor can be rewritten as

\begin{align*} & \mathbb {E}_{u,v} \sum _h \langle \psi \rvert \Bigl((A^v_{h(v)} - A^u_{h(u)}) \cdot \sum _{o:(o,h)\in S_u} M^u_o \cdot (A^v_{h(v)} - A^u_{h(u)})\Bigr) \otimes T_h \lvert \psi \rangle \\ & \le \mathbb {E}_{u,v} \sum _h \langle \psi \rvert (A^v_{h(v)} - A^u_{h(u)})^2 \otimes T_h \lvert \psi \rangle , \end{align*}

because \(M^u\) is a submeasurement. Lemma 6.6 bounds this by \(\zeta _{\mathrm{variance}}\) since \(T \in \mathrm{PolySub}(m,q,d)\). The second factor is exactly the first factor from 39, so it is at most \(1\).

Finally, we show that

\begin{equation} \label{eq:replace-right-point-conditioner} \eqref{eq:replace-left-point-conditioner} \approx _{\sqrt{\zeta _{\mathrm{variance}}}} \mathbb {E}_{u,v} \sum _{(o, h) \in S_{u}} \langle \psi \rvert \bigl(A^{u}_{h(u)} \cdot M^{u}_o \cdot A^{u}_{h(u)}\bigr) \otimes T_h \lvert \psi \rangle . \end{equation}

The same Cauchy–Schwarz estimate as in 41, with the final copy of \(A^v_{h(v)}\) replaced by \(A^u_{h(u)}\), gives the same bound \(\sqrt{\zeta _{\mathrm{variance}}}\). Indeed, the factor containing \(A^u_{h(u)} \cdot M^u_o \cdot A^u_{h(u)}\) is bounded by \(1\) by the same submeasurement argument as above, while the factor containing \((A^v_{h(v)} - A^u_{h(u)})^2\) is unchanged. Summing the four transports gives an error of \(2\sqrt{2\delta } + 2\sqrt{\zeta _{\mathrm{variance}}}\), and the lemma follows from \(2\delta \leq \zeta _{\mathrm{variance}}\).

7.2 Projective Output

This final step applies orthonormalization to the non-projective family produced by Lemma 7.1. The bookkeeping here is entirely about showing that completeness, consistency, self-consistency, and boundedness survive the passage from \(\widehat H\) to a projective submeasurement \(H\).

Remark 7.10 Auxiliary self-improvement lemmas

Several auxiliary results are used to prove Theorem 7.11 from the helper output and the orthonormalization theorem. They record local intermediate estimates and final-field assembly lemmas. The former orthonormalization spectral-transport record has been retired; the spectral-truncation part of the construction is now represented directly by spectralTruncationStatement_of_sourceAlmostProjective. This result is not a locality-preserving repair theorem. The theorem below records the paper-facing conclusion. Its proof follows the expectation-level completeness argument from the paper; the obstruction to a generic operator-total strengthening is recorded in issue #1642.

Theorem 7.11 Self-improvement

✓

Let \(G \in \mathrm{PolyMeas}(m,q,d)\) be a measurement with the following properties:

(Consistency with \(A\)): On average over \(u \sim \mathbb {F}_q^{m}\),

\[ A^{u}_a \otimes I \simeq _{\nu } I \otimes G_{[g(u)=a]}. \]

Let

\[ \zeta = 3000m\cdot \Big(\varepsilon ^{1/32} + \delta ^{1/32} + (d/q)^{1/32}\Big). \]

Then there exists a projective submeasurement \(H \in \mathrm{PolySub}(m,q,d)\) with the following properties:

(Completeness): If \(H = \sum _h H_h\), then

\[ \langle \psi \rvert H \otimes I \lvert \psi \rangle \geq (1-\nu )-\zeta . \]
(Consistency with \(A\)): On average over \(u \sim \mathbb {F}_q^m\),

\[ A^u_a \otimes I \simeq _{\zeta } I \otimes H_{[h(u) = a]}. \]
(Strong self-consistency):

\[ H_h \otimes I \approx _{\zeta } I \otimes H_h. \]
(Boundedness): There exists a positive-semidefinite matrix \(Z\) such that

\[ \langle \psi \rvert Z \otimes (I - H) \lvert \psi \rangle \leq \zeta \]

and for each \(h \in \mathcal{P}(m,q,d)\),

\[ Z \geq \left(\mathbb {E}_{u} A^{u}_{h(u)}\right). \]

Proof ▶

The bound is trivial if one of \(\varepsilon \), \(\delta \), or \(d/q\) is at least \(1\), so assume all three are at most \(1\). In Lean, the third assumption is recorded as \(d \le q\), which is equivalent to \(d/q \le 1\) since \(q{\gt}0\). Apply Lemma 7.1 to \(G\) and let \(\widehat H \in \mathrm{PolySub}(m,q,d)\) be the output, with

\[ \widehat{\zeta } = 100m \cdot \Big(\varepsilon ^{1/2} + \delta ^{1/2} + (d/q)^{1/2}\Big). \]

By 3 of Lemma 7.1,

\[ \sum _{h} \langle \psi \rvert \widehat{H}_h \otimes \widehat{H}_h \lvert \psi \rangle \geq \langle \psi \rvert \widehat{H} \otimes I \lvert \psi \rangle - \widehat{\zeta }. \]

Therefore Theorem 4.4 supplies a projective submeasurement \(H \in \mathrm{PolySub}(m,q,d)\) such that

\begin{equation} \label{eq:approx-between-H-with-and-without-hat} \widehat{H}_h \otimes I \approx _{\widehat{\zeta }_{\mathrm{ortho}}} H_{h} \otimes I, \end{equation}

where

\[ \widehat{\zeta }_{\mathrm{ortho}} = 100 \widehat{\zeta }^{1/4}. \]

In addition, Lemma 3.39 implies that

\begin{equation} \label{eq:approx-data-processed} \widehat{H}_{[h(u)=a]} \otimes I \approx _{\widehat{\zeta }_{\mathrm{dataprocess}}} H_{[h(u)=a]} \otimes I, \end{equation}

where

\[ \widehat{\zeta }_{\mathrm{dataprocess}} = 8 \widehat{\zeta } + 8 \sqrt{\widehat{\zeta }_{\mathrm{ortho}}}. \]

The four conclusions are transferred one by one.

Proof of 1. Lemma 3.38 implies

\[ \langle \psi \rvert H \otimes I \lvert \psi \rangle \geq \langle \psi \rvert \widehat{H} \otimes I \lvert \psi \rangle - \widehat{\zeta } - 2\sqrt{\widehat{\zeta }_{\mathrm{ortho}}} \geq (1-\nu ) - 2\widehat{\zeta } - 2\sqrt{\widehat{\zeta }_{\mathrm{ortho}}}, \]

where the second inequality is 1 of Lemma 7.1.

Proof of 2. Lemma 3.20 applied to 2 of Lemma 7.1 and the post-processed comparison 46 gives

\[ A^u_a \otimes I \simeq _{\widehat{\zeta } + \sqrt{\widehat{\zeta }_{\mathrm{dataprocess}}}} I \otimes H_{[h(u) = a]}. \]

In Lean the corresponding transport is stated for submeasurements with the total-overlap displacement recorded explicitly; this is the term which vanishes in the measurement-valued form of Lemma 3.20. The monotone-total route records a sufficient structural replacement: if the orthonormalization repair preserves the completed residual outcome, then the projective total is bounded by the helper total as an operator, hence also has no larger right-register expectation in the strategy state. Under this structural hypothesis the alphabet-size displacement term is not introduced. The QXP-layer interface used by the formalization records both the total domination of the canonical projective family and the sharper residual comparison for the fresh option-completion outcome. At present the formal QXP algebra only isolates the construction-level statement \(Q_{\mathrm{none}} \leq P_{\mathrm{none}}\), obtained when the repair preserves the fresh row block \(\widehat X_{\mathrm{none}}=X_{\mathrm{none}}\). The former generic “RestrictSome” monotone-total route would have required one to turn this into the source-facing inequality \(\widehat A_{\bot } \leq \widehat P_{\bot }\), by adding a comparison between the completed source residual and the “Q”-layer fresh outcome. The present formal development no longer uses that generic route, and the comparison is false without additional hypotheses; see docs/reports/issue-1642-restrictsome-residual-domination-obstruction.md. Since \(A^u_{\mathrm{tot}}=I\) and postprocessing does not change the total operator, Lean also records the equivalent form in which this displacement is the single scalar difference

\[ \left| \langle \psi , I \otimes H_{\mathrm{tot}} \psi \rangle - \langle \psi , I \otimes \widehat H_{\mathrm{tot}} \psi \rangle \right| \]

between the right-register totals of \(H\) and \(\widehat H\). The outcomewise data-processing bound controls this scalar by applying the vector triangle inequality to the sum over \(a\in \mathbb {F}_q\); the formal estimate gives the additional term

\[ \sqrt{q\, \widehat{\zeta }_{\mathrm{dataprocess}}}. \]

Thus the total-overlap term is no longer an independent hypothesis, although the numerical absorption of this alphabet-size loss is recorded separately. There is also a sharper formal route: if the right-register total of the projective family has no larger expectation than that of \(\widehat H\), then the total-overlap term can only improve the consistency defect. Under this monotonicity hypothesis the transported error is again \(\widehat{\zeta }+\sqrt{\widehat{\zeta }_{\mathrm{dataprocess}}}\), and the standard final-stage numerical estimate absorbs it into \(\zeta \).

Proof of 3. Lemma 3.36 implies

\[ \widehat{H}_h \otimes I \approx _{2\widehat{\zeta }} I \otimes \widehat{H}_h. \]

Combining this with 45 on both sides and summing the three transports with Lemma 3.27 yields

\[ H_h \otimes I \approx _{6 \widehat{\zeta } + 6\widehat{\zeta }_{\mathrm{ortho}}} I \otimes H_h. \]

Proof of 4. The boundedness quantity is

\begin{align} & \langle \psi \rvert Z \otimes (I - H) \lvert \psi \rangle \notag \\ ={}& \langle \psi \rvert Z \otimes I \lvert \psi \rangle - \sum _h \langle \psi \rvert Z \otimes H_h \lvert \psi \rangle \notag \\ \leq {}& \langle \psi \rvert Z \otimes I \lvert \psi \rangle - \sum _h \langle \psi \rvert \mathbb {E}_{u} A^{u}_{h(u)} \otimes H_h \lvert \psi \rangle \notag \\ ={}& \langle \psi \rvert Z \otimes I \lvert \psi \rangle -\mathbb {E}_{u} \sum _h \langle \psi \rvert A^{u}_{h(u)} \otimes H_h \lvert \psi \rangle \notag \\ ={}& \langle \psi \rvert Z \otimes I \lvert \psi \rangle -\mathbb {E}_{u} \sum _a \langle \psi \rvert A^{u}_{a} \otimes H_{[h(u)=a]} \lvert \psi \rangle . \label{eq:projective-boundedness-expanded} \end{align}

Proposition 3.24 upgrades 46 to the scalar estimate

\[ \eqref{eq:projective-boundedness-expanded} \le \langle \psi \rvert Z \otimes I \lvert \psi \rangle -\mathbb {E}_{u} \sum _a \langle \psi \rvert A^{u}_{a} \otimes \widehat H_{[h(u)=a]} \lvert \psi \rangle + \sqrt{\widehat{\zeta }_{\mathrm{dataprocess}}}, \]

and now 4 of Lemma 7.1 bounds this by \(\widehat{\zeta } + \sqrt{\widehat{\zeta }_{\mathrm{dataprocess}}}\). The formal boundedness field is the corresponding operator-monotonicity step: once the SDP dual witness satisfies \(I\le Z\), the total mass of any left-placed submeasurement, and in particular of the final projective submeasurement, is bounded by \(Z\otimes I\) with zero boundedness error.

Thus the four conclusions hold with errors

\[ 2\widehat{\zeta } + 2\sqrt{\widehat{\zeta }_{\mathrm{ortho}}}, \qquad \widehat{\zeta } + \sqrt{\widehat{\zeta }_{\mathrm{dataprocess}}}, \qquad 6 \widehat{\zeta } + 6\widehat{\zeta }_{\mathrm{ortho}}, \qquad \widehat{\zeta } + \sqrt{\widehat{\zeta }_{\mathrm{dataprocess}}}, \]

respectively. The paper’s exponent bookkeeping then shows the following bounds. The formal bookkeeping uses the three-term power sum \(\varepsilon ^p + \delta ^p + (d/q)^p\), its monotonicity on the unit interval, and the corresponding square-root estimate. The displayed Lean theorems record these arithmetic identities together with the completeness, self-closeness, and projective-residual absorptions \(2 \widehat{\zeta } + 2\sqrt{\widehat{\zeta }_{\mathrm{ortho}}} \le \zeta \), \(6 \widehat{\zeta } + 6\widehat{\zeta }_{\mathrm{ortho}} \le \zeta \) and \(\widehat{\zeta } + \sqrt{\widehat{\zeta }_{\mathrm{dataprocess}}} \le \zeta \). The two threshold lemmas involving \(|\mathbb F_q|\) record the scalar part of the alphabet-size obstruction in the current final-fields point-consistency transport: the data-processing threshold contains \(8\widehat{\zeta }\), but the transported estimate still carries the factor \(\sqrt{|\mathbb F_q|}\).

\[ \widehat{\zeta }_{\mathrm{ortho}} \leq 400 m \cdot \Big(\varepsilon ^{1/8} + \delta ^{1/8} + (d/q)^{1/8}\Big), \]

\[ \widehat{\zeta }_{\mathrm{dataprocess}} \leq 960m \cdot \Big(\varepsilon ^{1/16} + \delta ^{1/16} + (d/q)^{1/16}\Big), \]

and hence

\[ 6 \widehat{\zeta } + 6\widehat{\zeta }_{\mathrm{ortho}} \le \zeta , \qquad \widehat{\zeta } + \sqrt{\widehat{\zeta }_{\mathrm{dataprocess}}} \le \zeta . \]

Since \(2\widehat{\zeta } + 2\sqrt{\widehat{\zeta }_{\mathrm{ortho}}} \le \widehat{\zeta }_{\mathrm{dataprocess}} \le \zeta \), all four bounds are at most \(\zeta \).