10 The main induction step

10.1 Restricting to one slice

Definition 10.1 Appending a line at height \(x\)

✓

For \(x \in \mathbb {F}_q\), let \(\operatorname {append}_x(\ell )\) be the line in \(\mathbb {F}_q^{m+1}\) obtained by appending the coordinate \(x\) to every point of a line \(\ell \subseteq \mathbb {F}_q^m\). If \(f \colon \ell \to \mathbb {F}_q\), let \(\operatorname {append}_x(f)\) be the polynomial on \(\operatorname {append}_x(\ell )\) defined by \(\operatorname {append}_x(f)(u,x)=f(u)\).

Definition 10.2 \(x\)-restricted strategy

✓

Let \((\psi ,A,B,L)\) be a symmetric strategy for the \((m+1,q,d)\) low individual degree test. For each \(x \in \mathbb {F}_q\), the \(x\)-restricted strategy \((\psi ,A^x,B^x,L^x)\) for the \((m,q,d)\) test is defined by

\[ (A^x)_a^u = A_a^{u,x}, \qquad (B^x)_f^\ell = B_{\operatorname {append}_x(f)}^{\operatorname {append}_x(\ell )}, \qquad (L^x)_f^\ell = L_{\operatorname {append}_x(f)}^{\operatorname {append}_x(\ell )}. \]

Lemma 10.3 Restricted success probabilities

✓

Let \((\psi ,A,B,L)\) be an \((\varepsilon ,\delta ,\gamma )\)-good symmetric strategy for the \((m+1,q,d)\) test. For each \(x \in \mathbb {F}_q\), let \((\psi ,A^x,B^x,L^x)\) be the restricted strategy and let \(\varepsilon _x,\delta _x,\gamma _x\) be its three failure probabilities. Then

\[ \mathbb {E}_x \varepsilon _x \le \frac{m+1}{m}\varepsilon , \qquad \mathbb {E}_x \delta _x \le \delta , \qquad \mathbb {E}_x \gamma _x \le \frac{m+1}{m}\gamma . \]

Proof ▶

The self-consistency test restricts exactly to the slice at height \(x\). For the axis-parallel and diagonal-line tests, conditioning on the sampled line not being parallel to the last coordinate identifies the test with the corresponding restricted game.

Definition 10.4 Average restricted errors

✓

The average restricted errors are the expectations over \(x \in \mathbb {F}_q\) of the axis-parallel, self-consistency, and restricted diagonal-line failure probabilities of the \(x\)-restricted strategies.

Lemma 10.5 Weighted restricted-probability bounds

✓

The weighted bounds from Lemma 10.3 imply the restricted-probability data used in the successor step.

Proof ▶

The weighted axis-parallel and diagonal-line estimates are divided by the transverse-direction weight, while the self-consistency estimate is exactly the average restricted self-consistency probability. These three estimates form the restricted-probability record used in the successor step.

10.2 The inductive construction

Theorem 10.6 Self-improvement

✓

Let \((\psi ,A,B,L)\) be an \((\varepsilon ,\delta ,\gamma )\)-good symmetric strategy for the \((m,q,d)\) low individual degree test. 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_a^u \otimes I \simeq _\nu I \otimes G_{[g(u)=a]}. \]

Let

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

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 \ge (1-\nu )-\zeta . \]
(Consistency with \(A\)): On average over \(u \sim \mathbb {F}_q^m\),

\[ A_a^u \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 operator \(Z\) such that

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

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

\[ Z \ge \mathbb {E}_u A_{h(u)}^u. \]

Proof ▶

This is Theorem 7.11, with the conclusions reformulated in the notation used by the induction step. Since the output is projective, Lemma 3.36 converts the strong self-consistency statement to the usual bipartite formulation.

Remark 10.7 Lean realization of induction self-improvement

The Lean declaration for Theorem 10.6 has the paper hypotheses, in particular that \(G\) is a complete polynomial measurement. The labelled theorem in references/ldt-paper/inductive_step.tex:249–286 states the input as a submeasurement, while the proved form in references/ldt-paper/self_improvement.tex:635–671 states it as a measurement. The blueprint and Lean follow the proved measurement-valued form, which is also the form used at the point where the theorem is applied in references/ldt-paper/inductive_step.tex:461–485. The proof applies SelfImprovement.selfImprovement to \(G\), then uses selfImprovementInInductionSectionConclusion_ofSelfImprovementConclusion to transport the fields. The Section 7 SDP slackness input is supplied by the formalized theorem sdp_statement_with_slackness; it is not an additional hypothesis of the induction-section theorem.

Theorem 10.8 Pasting

✓

Let \((\psi ,A,B,L)\) be an \((\varepsilon ,\delta ,\gamma )\)-good symmetric strategy for the \((m+1,q,d)\) low individual degree test. Let \(\{ G^x\} _{x \in \mathbb {F}_q}\) be projective submeasurements in \(\mathrm{PolySub}(m,q,d)\) with the following properties:

(Completeness): If \(G=\mathbb {E}_x \sum _g G_g^x\), then

\[ \langle \psi \rvert G \otimes I \lvert \psi \rangle \ge 1-\kappa . \]
(Consistency with \(A\)): On average over \((u,x) \sim \mathbb {F}_q^{m+1}\),

\[ A_a^{u,x} \otimes I \simeq _\zeta I \otimes G_{[g(u)=a]}^x. \]
(Strong self-consistency): On average over \(x \sim \mathbb {F}_q\),

\[ G_g^x \otimes I \approx _\zeta I \otimes G_g^x. \]
(Boundedness): There are positive semidefinite operators \(Z^x\) such that

\[ \mathbb {E}_x \langle \psi \rvert (I-G^x) \otimes Z^x \lvert \psi \rangle \le \zeta \]

and for each \(x \in \mathbb {F}_q\) and \(g \in \mathcal{P}(m,q,d)\),

\[ Z^x \ge \mathbb {E}_u A_{g(u)}^{u,x}. \]

Let \(k \ge 400md\) and set

\[ \nu = 100k^2m\left(\varepsilon ^{1/32}+\delta ^{1/32}+\gamma ^{1/32}+\zeta ^{1/32}+(d/q)^{1/32}\right) \]

and

\[ \sigma = \kappa \left(1+\frac{1}{100m}\right) + 2\nu + e^{-k/(80000m^2)}. \]

Then there exists a measurement \(H \in \mathrm{PolyMeas}(m+1,q,d)\) with the following property:

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

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

Proof ▶

This is exactly Theorem 9.1, restated in the induction chapter because it is the pasting input used in the proof of Theorem 10.14. The Lean declaration linked above applies the unrestricted formal pasting theorem and transports its point-consistency field to the induction-section conclusion record.

Remark 10.9 Unrestricted Lean form of induction-section pasting

The Lean declaration linked to Theorem 10.8 is now the unrestricted source-facing restatement. It calls the formal Section 9 theorem Pasting.ldPasting and therefore carries exactly the source hypotheses displayed above, together with the faithful formal boundary hypotheses needed to interpret the objects in Lean.

The nontrivial-regime proof reduction remains represented in the Chapter 9 declaration Pasting.ldPastingNontrivial. That helper assumes

\[ \gamma \le 1,\qquad \zeta \le 1,\qquad d \le q,\qquad 0{\lt}d,\qquad 1\le k. \]

These inequalities are not hypotheses of the paper theorem: in references/ldt-paper/ld-pasting.tex, lines 12–50 state the unrestricted result, while lines 52–55 use the inequalities only to reduce the proof to the nontrivial regime. The formal theorem linked from the blueprint has already incorporated the complementary cases through Pasting.ldPasting.

Remark 10.10 Lean self-improvement slice transport for the successor step

The successor step records the slice-wise self-improvement output in SelfImprovementData, and the answer-valued route records the analogous output in AnswerSelfImprovementData. Their constructors call selfImprovementInInductionSection; they no longer carry a separate bundle of Section 7 proof-stage data as an input. The SliceStrategyTransport structures are narrow formal interfaces: they assume concrete per-slice symmetric strategies and measurement-transport data, while averaged point-operator compatibility is derived structurally from point-measurement transport. They then convert the remaining data into the ordinary or answer-valued self-improvement output.

Definition 10.11 Pasting data for the successor step

✓

The successor step forms the pasting input by combining the restricted probability estimates with the slice-wise self-improvement data. The Lean construction applies the unrestricted induction-section pasting theorem directly, and the small-error constructor supplies the scalar side conditions \(\gamma \le 1\), \(\zeta \le 1\), and \(d\le q\) internally. Thus the successor proof can call the small-error pasting constructor without carrying \(0{\lt}d\), \(1\le k\), \(\gamma \le 1\), \(\zeta \le 1\), or \(d\le q\) as separate proof inputs. The answer-valued small-error assembly then converts the answer-valued slice data to this pasting interface and applies the checked stage-data theorem.

Lemma 10.12 Base case of main induction

✓

Under the hypotheses of Theorem 10.14 with \(m=1\), there exists a measurement \(G \in \mathrm{PolyMeas}(1,q,d)\) such that, on average over \(u \sim \mathbb {F}_q\),

\[ A_a^u \otimes I \simeq _\varepsilon I \otimes G_{[g(u)=a]}, \]

which is stronger than the bound required by Theorem 10.14 for \(m=1\). Lean also proves the same one-dimensional construction for the answer-valued strategy interface used by the recursive-slice route.

Proof ▶

For \(m=1\), there is only one axis-parallel line \(\ell \) in \(\mathbb {F}_q\), so the line measurement \(B^\ell \) is already an element of \(\mathrm{PolyMeas}(1,q,d)\). Because the strategy fails the axis-parallel lines test with probability at most \(\varepsilon \), the consistency bound follows directly from the axis-parallel consistency hypothesis.

Lemma 10.13 Large-error branch of main induction

✓

If the target error parameter in Theorem 10.14 is at least \(1\), then the conclusion follows from a distinguished trivial polynomial measurement. Lean also proves the same large-error branch for the answer-valued strategy interface used by the recursive-slice route.

Proof ▶

The normalized bipartite consistency defect of two submeasurements is at most \(1\). Hence any polynomial measurement, in particular the measurement concentrated on one polynomial, satisfies the claimed consistency relation when the allowed error is at least \(1\).

Theorem 10.14 Main induction

✓

This is the corrected numerical form of the theorem; the paper-gap note [ con26b ] records the replacement of the printed bound \(k \ge md\) by \(k \ge 400md\). Let \((\psi ,A,B,L)\) be an \((\varepsilon ,\delta ,\gamma )\)-good symmetric strategy for the \((m,q,d)\) low individual degree test. Let \(k \ge 400md\) and set

\[ \nu = 1000k^2m^2\left(\varepsilon ^{1/1024}+\delta ^{1/1024}+\gamma ^{1/1024}+(d/q)^{1/1024}\right) \]

and

\[ \sigma = m^2\left(\nu + e^{-k/(80000m^2)}\right). \]

Then there exists a measurement \(G \in \mathrm{PolyMeas}(m,q,d)\) such that, on average over \(u \sim \mathbb {F}_q^m\),

\[ A_a^u \otimes I \simeq _\sigma I \otimes G_{[g(u)=a]}. \]

Proof ▶

The base case, the large-error branch, and the small-error successor construction are all formalized for the corrected large-\(k\) interface. The paper prints the weaker bound \(k\ge md\); the implication needed to apply the pasting theorem is false in the interval \(md\le k{\lt}400md\). Thus the factor \(400\) is recorded as a confirmed statement correction, as documented in [ con26b ] .

Proposition 10.15 Small-error successor construction for the induction theorem

✓

This is the nontrivial successor branch in the corrected large-\(k\) induction interface. The ordinary successor theorem now reduces to the internal answer-valued induction theorem. That theorem supplies the predecessor induction argument for the restricted slices by a genuine strong induction on the dimension. The answer-valued pasting invocation is recorded in Proposition 10.18, and the answer-valued self-improvement construction is checked by Proposition 10.17. This is a construction internal to the proof, not an assumption of Theorem 10.14. The recursive slice route applies also when \(d=0\); the successor reduction no longer needs a separate degree-zero family construction.

Proof ▶

The checked assembly theorem mainInductionSuccessorNext_ofSmallErrorConstruction reduces the ordinary branch to the answer-valued induction theorem through the answer-carrier construction. The answer-valued induction theorem supplies the predecessor argument internally; the answer-valued slice self-improvement construction and the averaged family-field assembly are checked, and the answer-valued pasting construction below supplies the final pasting input.

Proposition 10.16 Predecessor induction argument for successor slices

✓

In the small-error successor branch, the proof must apply the induction hypothesis in dimension \(m\) to the restricted strategies indexed by \(x\in \mathbb F_q\), with the same integer \(k\). The successor large-\(k\) hypothesis implies the predecessor large-\(k\) side condition in the corrected formal interface, and the nontrivial small-error branch supplies \(k\ge 1\). This is the genuine recursive use of the theorem; it is not an additional hypothesis on the successor strategy. The answer-valued restriction map for an answer-valued successor strategy is now explicit in Lean; it preserves the full function-valued diagonal answer on the slice, so it does not use the ordinary low-degree realization that is unavailable for arbitrary answer-valued diagonal measurements. The corresponding restricted-probability theorem for answer-valued successor strategies is also checked: the axis-parallel and diagonal slice averages are derived from the ambient answer-valued goodness assumptions, and the diagonal calculation uses the full function-valued answer rather than an ordinary polynomial-valued realization. Lean now also checks the recursive application itself: after these restricted probabilities are constructed, the predecessor answer-valued induction hypothesis gives the main-induction conclusion for every answer-valued restricted slice. The theorem answerMainInduction now supplies this predecessor hypothesis by strong induction on the dimension. Thus the predecessor induction argument is a checked internal construction, not an additional theorem hypothesis.

Proof ▶

The Lean proof is contained in the simultaneous answer-valued induction theorem and its restricted-slice constructors.

Proposition 10.17 Answer-valued slice self-improvement

✓

The restricted slice strategy is represented in Lean by an answer-valued strategy. The slice self-improvement data are constructed directly: replace only the diagonal part by an inert ordinary covariant measurement and apply the induction-section self-improvement theorem in the form whose hypotheses are the axis-parallel and point self-consistency estimates. Since the Section 9 conclusion is independent of the diagonal-line error parameter, no low-degree support theorem for the answer-valued diagonal outcomes is needed for this step. Such a support theorem would still be necessary for the stronger route which realizes the answer-valued diagonal measurement as an ordinary polynomial-valued covariant measurement, but that realization is not used here.

Proof ▶

The Lean proof is the carrier construction described in the statement. The diagonal component of the carrier is a fixed covariant projective measurement; the hypotheses consumed by self-improvement are the axis-parallel and point self-consistency estimates of the answer-valued restricted slice.

Proposition 10.18 Answer-valued pasting construction for the successor step

✓

After the recursive answer-valued slice measurements and the slice-wise self-improvement outputs have been averaged, Lean has a polynomial family which is complete, point-consistent with the actual answer-valued point measurement, strongly self-consistent, and bounded by the witnesses obtained from self-improvement. The boundedness input is presently typed through the point-equivalent ordinary carrier, because the existing boundedness interface for pasting is an ordinary-strategy interface.

The final induction-section pasting invocation is proved by first deriving the answer-valued Section 10 point-commutativity estimate from the answer-valued diagonal-line verifier relation, then invoking the Section 11 scalar chain in the form which assumes this point-commutativity estimate. The proof does not replace the answer-valued strategy by the ordinary carrier for the diagonal-line test; the carrier is used only for the ordinary boundedness interface. This construction is therefore a Lean-only internal construction for the simultaneous successor proof, not a new hypothesis of Theorem 10.14 and not a replacement for Theorem 10.8.

Proof ▶

The checked reduction answerMainInductionSuccessorNext_ofRecursiveHypothesisAndAnswerPasting shows that, with the predecessor answer-valued induction hypothesis in the successor context, the successor branch reduces to the answer-valued pasting theorem answerLdPastingInInductionSectionOfSmallError. That theorem is now proved from the answer-valued commutativity route, the degree-zero branch, and the scalar absorption estimate.

Checked status of the corrected induction interface.

In Lean, the base case is formalized through . The answer-valued analogue needed by the simultaneous recursive route uses the same one-dimensional axis-parallel-line construction and does not involve the diagonal answer interface. The printed source range \(md\le k{\lt}400md\) is excluded from the corrected theorem statement: the missing implication to the pasting size hypothesis is a confirmed statement gap, and Theorem 10.14 is stated with the corrected large-\(k\) hypothesis. The successor step of is isolated in its native \(m\to m+1\) form as the corrected large-\(k\) theorem . Its nontrivial branch is named as the small-error construction . The non-base branch only decomposes an arbitrary parameter bundle with \(m\ne 1\) into this successor form. Neither declaration takes restricted-probability, recursive-slice, self-improvement, or pasting records as hypotheses. The nearby formalization still names the stage data that mirror the four paper stages \(\text{restrict} \to \text{induct} \to \text{self-improve} \to \text{paste}\), but no theorem with these data as additional source-level hypotheses is advertised as Theorem 10.14. For the answer-valued restriction route used in the successor branch of the main formal theorem, Lean now also exposes , , which record the predecessor induction hypothesis for the restricted strategies, transport induction data in both directions between the answer-valued and ordinary slice interfaces, and then forget only the answer-valued diagonal alphabet before the existing pasting assembly. The weighted restricted-probability estimates are now public via , The Lean proof now closes the large-error branch by . The answer-valued large-error branch is checked by . The internal answer-valued induction theorem is ; it is now a genuine strong induction on the dimension. The surrounding development also contains the internal reductions , , which derive the successor conclusion from the answer-valued predecessor induction hypothesis. The answer-carrier forms construct the answer-valued self-improvement data directly from the restricted slices. The successor-bound form also derives the predecessor large-\(k\) and \(k\ge 1\) side conditions from the successor large-\(k\) hypothesis together with the small-error assumption, so these elementary arithmetic conditions are no longer additional hypotheses in the successor proof. The answer-carrier route shows that the separate degree-zero family route is not needed for the successor reduction: the predecessor induction hypothesis is used for the restricted slices also when \(d=0\), while \(k\ge 1\) comes from the nontrivial error branch. The obsolete slice-transport and degree-split family routes have therefore been removed from the checked interface. Thus the ordinary small-error construction theorem is now proved from the internal answer-valued induction theorem, and the answer-valued pasting theorem is also proved by the answer-valued commutativity route, the degree-zero branch, and the scalar absorption estimate. None of these constructions is a separate source hypothesis. The former answer-valued self-improvement interface mismatch is resolved for the induction step by the checked carrier construction. The older ordinary-realization constructors remain available and show that, under the stronger ordinary-realization route, the Section 9 theorem can also be applied slice by slice through the checked transport interface. Such a route still requires a low-degree support theorem for the answer-valued diagonal outcomes; otherwise the ordinary polynomial diagonal measurement cannot satisfy the required covariance after rebasing. The answer-valued ambient point-consistency averaging step is now checked by and . These lemmas prove the last-coordinate reindexing identity and the averaged consistency estimate for an ambient answer-valued strategy. The answer-valued successor scalar averaging estimates are checked by , and ; these are the \(\zeta _x\), \(\nu _x\), and \(\sigma _x\) Jensen and conditioning bounds for the actual AnswerSymStrat restricted successor profiles. The theorem now extracts the recursive slice measurements from the predecessor answer-valued induction hypothesis and proves the averaged \(\sigma _x\)-bound. The theorem then applies the axis-parallel/self-consistency form of self-improvement slice by slice, producing the projective \(\widehat G^x\)’s and witnesses \(Z^x\) together with the averaged \(\zeta _x\) and \(\sigma _x\) bounds. These slice outputs are assembled at the ambient answer-valued level by , which proves averaged completeness, point consistency with the actual answer-valued point measurement, strong self-consistency, the carrier-typed slice boundedness input, and the \(\kappa \)- and \(\zeta \)-bounds. This is not a final pasting theorem: the boundedness field uses the point-equivalent ordinary carrier only because the current boundedness interface is typed for ordinary strategies, and no claim is made that the carrier’s dummy diagonal measurement satisfies the answer-valued diagonal test. The answer-valued pasting invocation is proved as . The checked reduction shows that, with the predecessor answer-valued induction hypothesis available in the successor context, the successor branch reduces to this answer-valued pasting theorem. The conditional reduction is an internal lemma used inside the strong-induction proof, not a proof-level formalization link for a source theorem. The remaining ordinary family-level averaging components are also now isolated as checked lemmas: and . For answer-valued self-improvement data attached to an ordinary ambient strategy, the corresponding pasting fields are checked directly by and . The direct ordinary-ambient answer-valued assembly now invokes the induction-section pasting theorem from these fields and the answer-valued averaged scalar estimates; the exported theorem calls this direct proof. The remaining ambient answer-valued assembly is therefore the AnswerSymStrat analogue needed inside the simultaneous successor proof, together with the final pasting interface, not the ordinary answer-valued slice averaging calculation. The answer-valued pasting invocation and predecessor induction argument are now supplied internally in the proof of Theorem 10.14; they are not additional hypotheses about the successor strategy. We may assume \(\varepsilon ,\delta ,\gamma ,d/q \le 1\), since otherwise \(\nu \ge 1\) and the bound is trivial.

The proof is by induction on \(m\). The base case \(m=1\) is Lemma 10.12.

For the step from \(m\) to \(m+1\), let \((\psi ,A,B,L)\) be an \((\varepsilon ,\delta ,\gamma )\)-good symmetric strategy for the \((m+1,q,d)\) test, and let \(k \ge 400(m+1)d\). For each \(x \in \mathbb {F}_q\), let \((\psi ,A^x,B^x,L^x)\) be the \(x\)-restricted strategy, with failure parameters \(\varepsilon _x,\delta _x,\gamma _x\). Apply the induction hypothesis to each restricted strategy with the same integer \(k\) and define

\[ \nu _x = 1000k^2m^2\left(\varepsilon _x^{1/1024}+\delta _x^{1/1024}+\gamma _x^{1/1024}+(d/q)^{1/1024}\right), \qquad \sigma _x = m^2\left(\nu _x + e^{-k/(80000m^2)}\right). \]

This yields a measurement \(G^x \in \mathrm{PolyMeas}(m,q,d)\) such that

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

Next define

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

Theorem 10.6 produces a projective submeasurement \(\widehat G^x \in \mathrm{PolySub}(m,q,d)\) such that, for each \(x\):

if \(\widehat G^x=\sum _g \widehat G_g^x\), then

\[ \langle \psi \rvert \widehat G^x \otimes I \lvert \psi \rangle \ge (1-\sigma _x)-\zeta _x; \]
on average over \(u \sim \mathbb {F}_q^m\),

\[ (A^x)_a^u \otimes I \simeq _{\zeta _x} I \otimes \widehat G_{[g(u)=a]}^x; \]
\[ \widehat G_g^x \otimes I \approx _{\zeta _x} I \otimes \widehat G_g^x; \]
there exists a positive semidefinite operator \(Z^x\) such that

\[ \langle \psi \rvert Z^x \otimes (I-\widehat G^x) \lvert \psi \rangle \le \zeta _x \]

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

\[ Z^x \ge \mathbb {E}_u (A^x)_{g(u)}^u. \]

We now average the slice-dependent parameters. By concavity of \(\alpha \mapsto \alpha ^c\) for \(c \le 1\) and Lemma 10.3,

\begin{align*} \mathbb {E}_x \nu _x & \le 1000k^2m^2\left((\mathbb {E}_x \varepsilon _x)^{1/1024}+(\mathbb {E}_x \delta _x)^{1/1024}+(\mathbb {E}_x \gamma _x)^{1/1024}+(d/q)^{1/1024}\right) \\ & \le 1000k^2m^2\left(\left(\frac{m+1}{m}\varepsilon \right)^{1/1024}+\delta ^{1/1024}+\left(\frac{m+1}{m}\gamma \right)^{1/1024}+(d/q)^{1/1024}\right) \\ & \le 1000k^2(m+1)^2\left(\varepsilon ^{1/1024}+\delta ^{1/1024}+\gamma ^{1/1024}+(d/q)^{1/1024}\right). \end{align*}

Call this final quantity \(\nu \). Then, defining

\[ \sigma = m^2\left(\nu + e^{-k/(80000m^2)}\right), \]

we have

\[ \sigma \ge \mathbb {E}_x \sigma _x. \]

Similarly,

\begin{align*} \mathbb {E}_x \zeta _x & \le 3000m\left((\mathbb {E}_x \varepsilon _x)^{1/32}+(\mathbb {E}_x \delta _x)^{1/32}+(d/q)^{1/32}\right) \\ & \le 3000m\left(\left(\frac{m+1}{m}\varepsilon \right)^{1/32}+\delta ^{1/32}+(d/q)^{1/32}\right) \\ & \le 3000(m+1)\left(\varepsilon ^{1/32}+\delta ^{1/32}+(d/q)^{1/32}\right). \end{align*}

Call this last quantity \(\zeta \). For later use,

\begin{align} \zeta & = 3000(m+1)\left(\varepsilon ^{1/32}+\delta ^{1/32}+(d/q)^{1/32}\right) \notag \\ & \le 1000k^2(m+1)^2\left(\varepsilon ^{1/32}+\delta ^{1/32}+(d/q)^{1/32}\right) \notag \\ & \le 1000k^2(m+1)^2\left(\varepsilon ^{1/1024}+\delta ^{1/1024}+\gamma ^{1/1024}+(d/q)^{1/1024}\right) \notag \\ & = \nu . \label{eq:zeta-smaller-than-nu} \end{align}

The averaged slice family \(\{ \widehat G^x\} _{x \in \mathbb {F}_q}\) therefore satisfies the four hypotheses of Theorem 10.8 with completeness parameter \(\kappa =\sigma +\zeta \). To verify the new \(\nu \) bound in that theorem, observe that \((3000)^{1/32} \le 2\), so

\[ \zeta ^{1/32} \le 2(m+1)\left(\varepsilon ^{1/1024}+\delta ^{1/1024}+(d/q)^{1/1024}\right), \]

and hence

\begin{align*} & 100k^2m\left(\varepsilon ^{1/32}+\delta ^{1/32}+\gamma ^{1/32}+\zeta ^{1/32}+(d/q)^{1/32}\right) \\ & \le 1000k^2(m+1)^2\left(\varepsilon ^{1/1024}+\delta ^{1/1024}+\gamma ^{1/1024}+(d/q)^{1/1024}\right) \\ & = \nu . \end{align*}

Therefore Theorem 10.8 gives a pasted measurement \(H \in \mathrm{PolyMeas}(m+1,q,d)\) such that, on average over \(u \sim \mathbb {F}_q^{m+1}\),

\[ A_a^u \otimes I \simeq _{\sigma ^*} I \otimes H_{[h(u)=a]}, \]

where

\[ \sigma ^* = (\sigma +\zeta )\left(1+\frac{1}{100m}\right) + 2\nu + e^{-k/(80000m^2)}. \]

It remains to compare \(\sigma ^*\) with the next-stage target. The pasting parameter in Theorem 10.8 is bounded by \(\nu /5\) in this regime. Using this sharper estimate and 1, we get

\begin{align*} \sigma ^* & \le \left(m^2\left(\nu +e^{-k/(80000m^2)}\right)+\nu \right) \left(1+\frac{1}{100m}\right) + \frac{2}{5}\nu + e^{-k/(80000m^2)} \\ & = \left((m^2+1)\left(1+\frac{1}{100m}\right)+\frac{2}{5}\right)\nu + \left(m^2\left(1+\frac{1}{100m}\right)+1\right)e^{-k/(80000m^2)}. \end{align*}

For every \(m\ge 1\),

\[ (m^2+1)\left(1+\frac{1}{100m}\right)+\frac{2}{5}\le (m+1)^2, \qquad m^2\left(1+\frac{1}{100m}\right)+1\le (m+1)^2. \]

Therefore

\[ \sigma ^* \le (m+1)^2\left(\nu +e^{-k/(80000m^2)}\right) \le (m+1)^2\left(\nu +e^{-k/(80000(m+1)^2)}\right), \]

which is exactly the bound required for dimension \(m+1\).

Remark 10.19 Lean status of the successor-step assembly

The Lean declaration for Theorem 10.14 has the corrected large-\(k\) theorem hypotheses and no additional stage-data hypotheses. Its native successor step mainInductionSuccessorNext is now proved. The weighted slice bounds feeding Lemma 10.3 remain exposed through the public restriction-package constructor above, but the recursive slice witnesses, the slice-wise self-improvement outputs, and the answer-valued pasting comparison are derived inside the successor proof. They are not represented by a separate theorem whose assumptions are added to the paper statement.

10.3 Proof of the main formal theorem

Lemma 10.20 Heterogeneous role-register symmetrization

✓

Let \((\psi ,A^{\mathrm A},B^{\mathrm A},L^{\mathrm A},A^{\mathrm B},B^{\mathrm B},L^{\mathrm B})\) be a projective strategy on two local spaces passing the \((m,q,d)\) low individual degree test with probability at least \(1-\varepsilon \). Adding a role register and placing the two local spaces in the direct sum \(H_{\mathrm A}\oplus H_{\mathrm B}\) yields a symmetric projective strategy that is \((3\varepsilon ,3\varepsilon ,3\varepsilon )\)-good.

Proof ▶

Each of the three subtests (axis-parallel, self-consistency, diagonal) occurs with probability \(1/3\), so the total failure probability at most \(\varepsilon \) implies each branch is at most \(3\varepsilon \). Block-diagonalizing the measurements over the role register preserves the axis-parallel and diagonal branch averages exactly, and the cross-register self-consistency branch of the symmetrized strategy equals the original point-agreement defect, which is itself bounded by \(3\varepsilon \).

Remark 10.21 Lean auxiliary data for role-register symmetrization

The formal proof of Theorem 2.14 uses the heterogeneous role-register strategy and its goodness proof. This construction supports the final assembly and is not an additional hypothesis in Lemma 10.20.

Proposition 10.22 Lean role-register main-induction handoff for the Section 3 proof

✓

For a two-space projective strategy passing the low individual degree test with error \(\varepsilon \), the role-register symmetrization is \((3\varepsilon ,3\varepsilon ,3\varepsilon )\)-good. Under the corrected hypothesis \(k\ge 400md\), Theorem 10.14 therefore supplies the Section 6 polynomial measurement used in the final theorem route.

Proof ▶

This is a Lean-only handoff theorem: combine Lemma 10.20 with the corrected large-\(k\) theorem .

Removed successor restricted-recursion targets.

The former Section 3 Lean-only answer-valued restricted-recursion records have been removed along with the same-space final-theorem assembly. The successor work belongs to the proof of Theorem 10.14, not to additional hypotheses or auxiliary inputs in Theorem 2.14.

Remark 10.23 Lean Step 6 constructions for the Section 3 proof

The old same-space base-case and completion-witness records have been removed. The current route starts with the heterogeneous role-register application of Theorem 10.14, extracts the two occupied role blocks, proves the Step 5 full-polynomial self-consistency relation, and then invokes the theorems for making measurements projective and for completion inside the two-space source route. These constructions are proof steps in Theorem 2.14, not hypotheses of its statement.

Lean successor-dependent Step 6 targets.

The role-register Section 6 measurement is obtained by applying the corrected large-\(k\) theorem MainInductionStep.mainInduction to the role-register symmetrization. The final source-route theorem then carries this measurement through the two unsymmetrized point-consistency relations, the Step 5 self-consistency calculation, the step making measurements projective, completion, and the final point-evaluation transport. These targets are proof-complete for the corrected large-\(k\) interface and are not added hypotheses of Theorem 2.14.

Remark 10.24 Projective-completion construction

The projective-completion construction is now internal to the two-space source route. It is not a separate assumption in the statement of Theorem 2.14. The corrected source theorem is proof-complete: the general two-space role-register passage has been assembled, and the theorem statement records the documented \(k\ge 400md\) and \(k{\gt}0\) boundary corrections.

Remark 10.25 Lean measurement-unsymmetrization consistency

Lean now isolates the Step 3 extraction from inductive_step.tex lines 84–108. In the same-space route, the principal-block map extractRoleBlock turns a role-register POVM \(G\) into the two POVMs \(G^{\mathrm A}\) and \(G^{\mathrm B}\) on the original prover space and proves that point-evaluation postprocessing commutes with this extraction. In the heterogeneous two-space route, the corresponding principal-block maps extractRoleRegisterAlice and extractRoleRegisterBob extract the occupied \((\mathrm A,\mathrm{inl})\) and \((\mathrm B,\mathrm{inr})\) blocks of a measurement on \(\{ \mathrm A,\mathrm B\} \times (\mathcal H_{\mathrm A}\oplus \mathcal H_{\mathrm B})\). Lean proves the trace-level factor-two identities for arbitrary role-register measurements in qBipartiteConsDefect_roleRegisterProjMeas_arbitrary_eq_average and its two factor-two consequences. No projectivity of arbitrary principal blocks is claimed, matching the paper’s later step making measurements projective.

Definition 10.26 Final error envelope

✓

Set

\[ E = \varepsilon ^{1/40000} + (d/q)^{1/40000} + e^{-k/(2560000m^2)}. \]

The remaining entries in this scalar-cascade subsection are Lean bookkeeping lemmas for the final proof of Theorem 2.14. They record explicit inequalities between the named error parameters; they are not independent source theorems from the paper.

Theorem 10.27 Basic facts about the final error envelope

✓

If \(0 \le \varepsilon \), then

\[ \nu _{\mathrm{main}}= 100000k^2m^4\left(\varepsilon ^{1/40000} + (d/q)^{1/40000} + e^{-k/(2560000m^2)}\right) = 100000k^2m^4 E, \]

and \(E \ge 0\).

Proof ▶

Both identities are by definition: the first unfolds \(\nu _{\mathrm{main}}\) and the second unfolds \(E\). Nonnegativity of \(E\) follows summand-wise from Real.rpow_nonneg (using \(0 \le \varepsilon \)) and Real.exp_nonneg.

Definition 10.28 Cascade parameters and standing hypotheses

✓

Assume \(q {\gt} 0\), \(k \ge 1\), \(m \ge 1\), \(0 \le \varepsilon \le 1\), and \(d \le q\). Fix an incoming error parameter \(\nu \). Define

\[ \sigma = m^2\left(\nu + e^{-k/(80000m^2)}\right), \qquad \zeta _1 = 2\sigma + 2\sqrt{3\varepsilon +2\sigma } + md/q, \]

\[ \zeta _2 = 200\zeta _1^{1/4} + 42\zeta _1^{1/8}, \qquad \zeta _3 = 6\zeta _1 + 6\zeta _2, \qquad \zeta _4 = 2\sigma + 2\sqrt{\zeta _1+\zeta _3/2}. \]

The coefficient \(42\) is the Lean cascade scalar; it widens the paper’s printed coefficient \(40\) so that the completion theorem’s extra \(2\zeta _1\) term is absorbed while preserving the final error envelope.

Theorem 10.29 Bound for the first cascade term

✓

Under the standing hypotheses, if

\[ \nu \le 10000k^2m^2\left(\varepsilon ^{1/1024} + (d/q)^{1/1024}\right), \]

then

\[ \sigma \le 10000k^2m^4 E. \]

Proof ▶

Multiply the assumed bound by \(m^2\), replace \(m^2\) by \(m^4\), coarsen the exponents from \(1/1024\) to \(1/40000\), and enlarge the exponential denominator from \(80000m^2\) to \(2560000m^2\).

Theorem 10.30 Cascade bounds for the later cascade terms

✓

Under the standing hypotheses, assume

\[ 0 \le \nu \le 10000k^2m^2\left(\varepsilon ^{1/1024} + (d/q)^{1/1024}\right). \]

Define

\[ \sigma = m^2\left(\nu + e^{-k/(80000m^2)}\right), \]

\[ \zeta _1 = 2\sigma + 2\sqrt{3\varepsilon + 2\sigma } + md/q, \qquad \zeta _2 = 200\zeta _1^{1/4} + 42\zeta _1^{1/8}, \]

\[ \zeta _3 = 6\zeta _1 + 6\zeta _2, \qquad \zeta _4 = 2\sigma + 2\sqrt{\zeta _1 + \zeta _3/2}. \]

Then

\[ \zeta _1, \zeta _2, \zeta _4 \le 100000k^2m^4 E, \qquad \zeta _3 \le 2 \cdot 100000k^2m^4 E. \]

Proof ▶

The Lean declarations first derive the native bounds for \(\zeta _1,\dots ,\zeta _4\) from the cascade definitions using square-root and \(rpow\) monotonicity, with \(\zeta _2\) using the widened coefficient \(42\), and then coarsen those bounds to the common envelope \(E\). The \(\zeta _2\) proof additionally uses \(k \le k^2\), \(m \le m^4\), and the nonnegativity of the earlier cascade variables.

Theorem 10.31 Consolidated error cascade

✓

Assume the standing hypotheses and

\[ 0 \le \nu \le 10000k^2m^2\left(\varepsilon ^{1/1024} + (d/q)^{1/1024}\right). \]

Let \(\sigma ,\zeta _1,\zeta _2,\zeta _3\) be the cascade quantities defined above. Then

\[ \sigma \le 100000k^2m^4 E, \qquad \zeta _1,\zeta _2 \le 100000k^2m^4 E, \qquad \zeta _3 \le 2 \cdot 100000k^2m^4 E, \]

and the concrete quantity

\[ \zeta _4 = 2\sigma + 2\sqrt{\zeta _1 + \zeta _3/2} \]

also satisfies

\[ \zeta _4 \le 100000k^2m^4 E. \]

Proof ▶

This is the direct combination of Theorem 10.29 and Theorem 10.30. The Lean declaration uses the explicit equalities naming \(\sigma ,\zeta _1,\zeta _2,\zeta _3\) as the corresponding cascade expressions.

Remark 10.32 Lean Step 5 expansion theorem

For the Step 5 passage below, Lean now names the weighted polynomial-collision mass, proves its \(md/q\) bound by specializing the existing tensor Schwartz–Zippel helper, and proves the algebraic expansion/reindexing statement comparing the evaluated consistency defect with the full-polynomial defect plus that collision mass. The theorem for Step 5 therefore no longer takes the expansion statement as an external hypothesis.

Remark 10.33 Lean witness structures for the main-formal assembly

The following Lean declarations are bookkeeping infrastructure for the final assembly witness: They split off the vacuous branch where the theorem error is at least \(1\), derive the Step 8 scalar hypotheses in the non-vacuous branch, and isolate the role-register Section 6 measurement behind a concrete role-witness record. The role-register measurement is now obtained directly from the mainInduction theorem by roleRegisterSymmStrategy_sourceMainInduction; the successor case is handled by the checked Section 6 theorem, so it is not a separate boundary hypothesis in Section 3. Lean also records that every non-base parameter choice has a predecessor via Parameters.successorDecompositionOfNeOne, and it retains the explicit transport helpers for the strategy and passing proof across that predecessor equality. The older branch-witness records, which assembled ordinary or answer-valued successor data from recursive slice witnesses and supplied self-improvement inputs, have been removed. The current completion witness carries the concrete role witness obtained from the Section 6 theorem rather than a separate decorative branch witness. Once the role-measurement record is obtained, Lean proves the two factor-two unsymmetrization links from its symmetrized consistency estimate. The subsequent proved lemmas use the proved Section 5 Schwartz–Zippel theorem to convert evaluated pre-projective consistency to full-polynomial consistency at \(\zeta _1\), prove the paper line-116 triangle step, and reconstruct the line-156 \(\approx _{\zeta _3}\) relation obtained while making measurements projective from pre-projective consistency plus left/right completion closeness at \(\zeta _2\). Lean also derives the evaluated line-164 projective consistency. The error-parametric lemmas pointAConsistency_ofLine169Consistency and pointBConsistency_ofLine169Consistency show that a polynomial line-169 estimate with error \(\eta \) yields the final point error

\[ 2\sigma + 2\sqrt{\eta +\zeta _3/2}. \]

The active formal route specializes this with the repaired value \(\eta =\zeta _1+10\zeta _1^{1/8}\). The existing pointAConsistency and pointBConsistency declarations are the corresponding repaired specializations. After the #869 right-register completion transport, the remaining active post-role witness asks only for Alice’s line-146 completion closeness, Bob’s right-register completion closeness, and the two repaired polynomial line-169 links. Lean reconstructs pre-projective full-polynomial consistency from the concrete role witness, uses those repaired line-169 links together with the evaluated line-164 projective consistency, and converts directly to the projective completion witness used by the final assembly. It no longer asks for an arbitrary role-measurement record or an arbitrary Section 6 witness as an independent field. It also no longer asks for stored factor-two role-block estimates, a stored Section 6 consistency input, or a duplicated pre-projective consistency field; those are rebuilt from the concrete role-register measurement and hpass. Lean then applies the projective converse of simeq-to-approx inside the two-space source route.

As stated in preliminaries.tex, prop:triangle-sub gives a \(\delta +\sqrt{\epsilon }\) loss, so applying it directly to \(G^{\mathrm A}\simeq _{\zeta _1}G^{\mathrm B}\) and \(G^{\mathrm A}\approx _{\zeta _2}Q^{\mathrm A}\) yields \(Q^{\mathrm A}\simeq _{\zeta _1+\sqrt{\zeta _2}}G^{\mathrm B}\), not the printed \(\zeta _1\) estimate. The generic corrected route would degrade the final point error to scale \(t^{1/65536}\), outside the current mainFormalError envelope. The sharper local pre-completion repair from Remark 4.6 avoids that widening. Its completion step uses only the formal monotonicity helper ProjectivizationMatchMassMonotonicity.completeAtOutcomeProj_left_matchMass_ge, not a separate exact match-mass witness route. For the corrected boundary assumptions \(k \ge 400md\) and \(k{\gt}0\), the source theorem now has a checked proof-level route.

Proof ▶

Let

\[ (\psi ,A^{\mathrm A},B^{\mathrm A},L^{\mathrm A},A^{\mathrm B},B^{\mathrm B},L^{\mathrm B}) \]

be a projective strategy passing the \((m,q,d)\) low individual degree test with probability at least \(1-\varepsilon \). Since the three subtests occur with probability \(1/3\), this strategy is \((3\varepsilon ,3\varepsilon ,3\varepsilon )\)-good.

Introduce a two-dimensional role register on each side and define the symmetrized state

\[ \lvert \psi _{\mathrm{sym}} \rangle = \frac{1}{\sqrt{2}} \left( \lvert 0 \rangle _{\mathrm{A}'}\lvert 1 \rangle _{\mathrm{B}'}\lvert \psi \rangle _{\mathrm{AB}} + \lvert 1 \rangle _{\mathrm{A}'}\lvert 0 \rangle _{\mathrm{B}'}\lvert \psi _{\mathrm{swap}} \rangle _{\mathrm{AB}} \right). \]

Define the symmetrized point measurement by

\[ (A_{\mathrm{sym}})_a^u = \lvert 0 \rangle \langle 0 \rvert \otimes A_a^{\mathrm A,u} + \lvert 1 \rangle \langle 1 \rvert \otimes A_a^{\mathrm B,u}, \]

and similarly for \(B_{\mathrm{sym}}\) and \(L_{\mathrm{sym}}\). This yields a symmetric \((3\varepsilon ,3\varepsilon ,3\varepsilon )\)-good strategy. Set

\[ \nu = 10000k^2m^2\left(\varepsilon ^{1/1024}+(d/q)^{1/1024}\right), \qquad \sigma = m^2\left(\nu +e^{-k/(80000m^2)}\right). \]

Theorem 10.14 applied to the symmetrized strategy produces a measurement \(G=\{ G_g\} \in \mathrm{PolyMeas}(m,q,d)\) such that

\begin{equation} \label{eq:symmetrized-induction-point-consistency} (A_{\mathrm{sym}})_a^u \otimes I \simeq _\sigma I \otimes G_{[g(u)=a]}, \qquad G_{[g(u)=a]} \otimes I \simeq _\sigma I \otimes (A_{\mathrm{sym}})_a^u. \end{equation}

Now unsymmetrize by defining

\[ G_g^{\mathrm A} = (\langle 0 \rvert \otimes I)\, G_g\, (\lvert 0 \rangle \otimes I), \qquad G_g^{\mathrm B} = (\langle 1 \rvert \otimes I)\, G_g\, (\lvert 1 \rangle \otimes I). \]

These are POVMs on the original prover space. Since \(A_{\mathrm{sym}}\) is a convex combination of \((\lvert 0 \rangle \langle 0 \rvert \otimes I)\) and \((\lvert 1 \rangle \langle 1 \rvert \otimes I)\) weighted by the test probabilities, the cross-terms \(\langle 0 \rvert \cdot A_{\mathrm{sym}} \cdot \lvert 1 \rangle \) vanish. Expanding the consistency of \(G\) gives

\begin{gather} G_{[g(u)=a]}^{\mathrm A} \otimes I \simeq _{2\sigma } I \otimes A_a^{\mathrm B,u}, \label{eq:cons-a}\\ I \otimes G_{[g(u)=a]}^{\mathrm B} \simeq _{2\sigma } A_a^{\mathrm A,u} \otimes I. \label{eq:cons-b} \end{gather}

Since the original strategy is \((3\varepsilon ,3\varepsilon ,3\varepsilon )\)-good,

\[ A_a^{\mathrm A,u} \otimes I \simeq _{3\varepsilon } I \otimes A_a^{\mathrm B,u}. \]

Therefore Lemma 3.29 yields

\[ G_{[g(u)=a]}^{\mathrm A} \otimes I \simeq _{2\sigma + 2\sqrt{3\varepsilon +2\sigma }} I \otimes G_{[g(u)=a]}^{\mathrm B}. \]

Expanding this consistency relation and applying Lemma 3.7 to replace point evaluations by polynomial evaluations (at cost \(md/q\)) gives

\begin{equation} \label{eq:G-self-consistency} G_g^{\mathrm A} \otimes I \simeq _{\zeta _1} I \otimes G_g^{\mathrm B}, \end{equation}

where

\[ \zeta _1 = 2\sigma + 2\sqrt{3\varepsilon +2\sigma } + \frac{md}{q}. \]

The Lean Step 5 theorem formalizes this expansion/reindexing step and combines it with the proved Schwartz–Zippel tensor bound . The Lean statement is now formulated for a bipartite state on \(H_A\otimes H_B\), so this particular Schwartz–Zippel loss is no longer a same-space restriction in the source-theorem route.

Apply Lemma 4.9 to 5. This gives projective submeasurements \(P^{\mathrm A},P^{\mathrm B} \in \mathrm{PolySub}(m,q,d)\) with

\[ G_g^{\mathrm A} \otimes I \approx _{100\zeta _1^{1/4}} P_g^{\mathrm A} \otimes I, \qquad I \otimes G_g^{\mathrm B} \approx _{100\zeta _1^{1/4}} I \otimes P_g^{\mathrm B}. \]

Completing them by Lemma 3.42 yields projective measurements \(Q^{\mathrm A},Q^{\mathrm B} \in \mathrm{PolyMeas}(m,q,d)\) such that

\begin{align} G_g^{\mathrm A} \otimes I & \approx _{\zeta _2} Q_g^{\mathrm A} \otimes I, \label{eq:G-with-Q-A} \\ I \otimes G_g^{\mathrm B} & \approx _{\zeta _2} I \otimes Q_g^{\mathrm B}, \notag \end{align}

where

\[ \zeta _2 = 200\zeta _1^{1/4} + 42\zeta _1^{1/8}. \]

The paper prints the coefficient \(40\) in this display. The formal Lean cascade uses the widened coefficient \(42\) to absorb the literal completion error \(2\cdot (100\zeta _1^{1/4})+4\sqrt{100\zeta _1^{1/4}}+2\zeta _1\): under the non-vacuous scalar regime \(0 \le \zeta _1 \le 1\), the extra term \(2\zeta _1\) is bounded by \(2\zeta _1^{1/8}\).

By 5 and Lemma 3.21,

\[ G_g^{\mathrm A} \otimes I \approx _{2\zeta _1} I \otimes G_g^{\mathrm B}. \]

Hence Lemma 3.27 gives

\[ Q_g^{\mathrm A} \otimes I \approx _{\zeta _3} I \otimes Q_g^{\mathrm B}, \]

where

\[ \zeta _3 = 6\zeta _1 + 6\zeta _2. \]

Because both measurements are projective, Lemma 3.21 converts this to

\begin{equation} \label{eq:completed-polynomial-consistency} Q_g^{\mathrm A} \otimes I \simeq _{\zeta _3/2} I \otimes Q_g^{\mathrm B}. \end{equation}

By data processing,

\begin{equation} \label{eq:point-evaluation-data-processing} Q_{[g(u)=a]}^{\mathrm A} \otimes I \simeq _{\zeta _3/2} I \otimes Q_{[g(u)=a]}^{\mathrm B}. \end{equation}

Next, Lemma 3.20, applied to 5 and 6, implies

\[ Q_g^{\mathrm A} \otimes I \simeq _{\zeta _1} I \otimes G_g^{\mathrm B}. \]

Data processing then gives

\begin{equation} \label{eq:left-completed-point-with-original-polynomial} Q_{[g(u)=a]}^{\mathrm A} \otimes I \simeq _{\zeta _1} I \otimes G_{[g(u)=a]}^{\mathrm B}. \end{equation}

Applying Lemma 3.29 to 4, 9, and 8 yields

\begin{equation} \label{eq:final-left-point-consistency} A_a^{\mathrm A,u} \otimes I \simeq _{\zeta _4} I \otimes Q_{[g(u)=a]}^{\mathrm B}, \end{equation}

where

\[ \zeta _4 = 2\sigma + 2\sqrt{\zeta _1+\zeta _3/2}. \]

The same argument with the roles reversed gives

\begin{equation} \label{eq:final-right-point-consistency} I \otimes A_a^{\mathrm B,u} \simeq _{\zeta _4} Q_{[g(u)=a]}^{\mathrm A} \otimes I. \end{equation}

Remark 10.33 records the Lean witness structures that separate the scalar cascade and the Step 5 Schwartz–Zippel handoff from the remaining projective-stage transport work. The scalar side discharges the paper’s line 71–73 coarsening and the Step 8 hypotheses in the non-vacuous branch; the Step 5 theorem now turns the evaluated estimate at line 116 into full-polynomial consistency at \(\zeta _1\). The remaining Lean witness is the completion-and-line-169 construction: supply the actual role-register measurement, Alice’s line-146 completion estimate, Bob’s left-register completion estimate, and the two exact polynomial-level \(\zeta _1\) links. Lean transports the Bob-side completion estimate to the line-147 right-register form, reconstructs the duplicated Step 6 pre-projective consistency field from these inputs and hpass, then data-processes the line-169 links to line 172 and derives the two \(\zeta _4\) point goals and the \(\zeta _3/2\) self-consistency target.

With \(E\) as in Definition 10.26, the quantities \(\sigma ,\zeta _1,\zeta _2,\zeta _3,\zeta _4\) form the cascade of Definition 10.28. Theorem 10.29 and Theorem 10.30 give the final inflation to the scale \(100000k^2m^4 E\). The underlying estimates, with the formal widened \(\zeta _2\), are:

\[ \sigma \le 10000k^2m^4\left(\varepsilon ^{1/1024}+(d/q)^{1/1024}+e^{-k/(80000m^2)}\right). \]

Then

\[ \zeta _1 \le 20204k^2m^4\left(\varepsilon ^{1/2048}+(d/q)^{1/2048}+e^{-k/(160000m^2)}\right), \]

and

\[ \zeta _2 \le 2568km\left(\varepsilon ^{1/16384}+(d/q)^{1/16384}+e^{-k/(1280000m^2)}\right). \]

Consequently,

\[ \zeta _3 \le 150000k^2m^4\left(\varepsilon ^{1/16384}+(d/q)^{1/16384}+e^{-k/(1280000m^2)}\right), \]

and

\[ \zeta _4 \le 40000k^2m^4\left(\varepsilon ^{1/32768}+(d/q)^{1/32768}+e^{-k/(2560000m^2)}\right). \]

Both \(\zeta _3/2\) and \(\zeta _4\) are therefore bounded by

\[ 100000k^2m^4\left(\varepsilon ^{1/40000}+(d/q)^{1/40000}+e^{-k/(2560000m^2)}\right). \]

Hence 10, 11, and 7 give the three claimed conclusions, with \(Q^{\mathrm A}\) and \(Q^{\mathrm B}\) renamed as the theorem’s \(G^{\mathrm A}\) and \(G^{\mathrm B}\).