Diagonal add-in-u selection and point-sandwich endpoints

This module contains the diagonal selection used in the strong-self-consistency application of the add-in-u lemma, the endpoint identities for its left and right sides, the point-projector insertion identities, and the Schwartz--Zippel collision endpoints used by the helper strong-self-consistency argument.

References

• references/ldt-paper/self_improvement.tex lines 247--252, 455--468
• blueprint/src/chapter/ch07_self_improvement.tex

noncomputable def MIPStarRE.LDT.SelfImprovement.selfConsistencyAddInUSelection (params : Parameters) [FieldModel params.q] : AddInUSelection params (Polynomial params)

The diagonal selection used in the strong-self-consistency application of lem:add-in-u in the proof of lem:self-improvement-helper.

At every point u, this selects exactly the pairs (h, h) of polynomial outcomes, matching self_improvement.tex, lines 459--468.

Equations

• MIPStarRE.LDT.SelfImprovement.selfConsistencyAddInUSelection params x✝ = {hh : MIPStarRE.LDT.Polynomial params × MIPStarRE.LDT.Polynomial params | hh.1 = hh.2}

theorem MIPStarRE.LDT.SelfImprovement.addInULeftQuantity_selfConsistencySelection_eq_matchMass {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) : addInULeftQuantity params strategy (sandwichedPolynomialSubMeasAt params strategy T) (averagedSandwichedPolynomialSubMeas params strategy T) (selfConsistencyAddInUSelection params) = qBipartiteMatchMass strategy.state (averagedSandwichedPolynomialSubMeas params strategy T) (averagedSandwichedPolynomialSubMeas params strategy T)

The left side of the diagonal add-in-u application in the helper strong-self-consistency proof is exactly the diagonal bipartite match mass of Hhat = E_u H^u.

This formalizes the paper's identity ∑_h ⟪H_h, H_h⟫ = E_u ∑_h ⟪H^u_h, H_h⟫ used at self_improvement.tex, lines 455--468.

theorem MIPStarRE.LDT.SelfImprovement.addInURightQuantity_selfConsistencySelection_eq_release {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) : addInURightQuantity params strategy (sandwichedPolynomialSubMeasAt params strategy T) T (selfConsistencyAddInUSelection params) = avgOver (uniformDistribution (Point params)) fun (u : Point params) => ∑ h : Polynomial params, have Au := GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy h u; ev strategy.state (opTensor (Au * (sandwichedPolynomialSubMeasAt params strategy T u).outcome h * Au) (T.outcome h))

The right side of the diagonal add-in-u application is the paper's "release-the-kraken" expression, with the two copies of A^u_{h(u)} placed around the pointwise helper submeasurement H^u_h.

theorem MIPStarRE.LDT.SelfImprovement.selfConsistencyDiagonalAddInU_of_transfer {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta : Error) (T : SubMeas (Polynomial params) ι) (htransfer : |addInULeftQuantity params strategy (sandwichedPolynomialSubMeasAt params strategy T) (averagedSandwichedPolynomialSubMeas params strategy T) (selfConsistencyAddInUSelection params) - addInURightQuantity params strategy (sandwichedPolynomialSubMeasAt params strategy T) T (selfConsistencyAddInUSelection params)| ≤ addInUError params eps delta) : |qBipartiteMatchMass strategy.state (averagedSandwichedPolynomialSubMeas params strategy T) (averagedSandwichedPolynomialSubMeas params strategy T) - avgOver (uniformDistribution (Point params)) fun (u : Point params) => ∑ h : Polynomial params, have Au := GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy h u; ev strategy.state (opTensor (Au * (sandwichedPolynomialSubMeasAt params strategy T u).outcome h * Au) (T.outcome h))| ≤ addInUError params eps delta

Specialization of the missing full add-in-u transfer to the diagonal selection needed for helper strong self-consistency.

The hypothesis is exactly the scalar transfer inequality supplied by the paper's lem:add-in-u after choosing M^u = H^u and S_u = {(h,h) : h ∈ \polyfunc{m}{q}{d}}. The conclusion rewrites that transfer into the paper's displayed step eq:release-the-kraken. The helper strong-self-consistency assembly now consumes this transfer internally; it is not a source-theorem hypothesis.

theorem MIPStarRE.LDT.SelfImprovement.proj_outer_sandwich_eq {ι : Type u_2} [Fintype ι] (A X : Quantum.Op ι) (hA : A * A = A) : A * (A * X * A) * A = A * X * A

Projective sandwich collapse: if A * A = A, then A * (A * X * A) * A = A * X * A.

This is the operator-algebra fact used to simplify the diagonal add-in-u right-hand side: the outer A^u_{h(u)} factors collapse into the inner sandwich A^u_{h(u)} T_h A^u_{h(u)} because (strategy.pointMeasurement u).proj makes every point-measurement outcome a projection.

theorem MIPStarRE.LDT.SelfImprovement.pointConditioned_sandwichedPolynomialOutcome_outer_eq_ite {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) (u : Point params) (h h' : Polynomial params) : have Ah := GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy h u; Ah * (sandwichedPolynomialSubMeasAt params strategy T u).outcome h' * Ah = if h.toFun u = h'.toFun u then (sandwichedPolynomialSubMeasAt params strategy T u).outcome h' else 0

Insert the point projector around a sandwiched helper outcome.

For fixed u, the operator H^u_{h'} = A^u_{h'(u)} T_{h'} A^u_{h'(u)} survives the outer sandwich by A^u_{h(u)} precisely when the two polynomials agree at u. This is the operator form of the paper identity labelled eq:h-blt.

theorem MIPStarRE.LDT.SelfImprovement.ev_opTensor_pointConditioned_sandwichedPolynomialOutcome_outer_eq_indicator {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) (u : Point params) (h h' : Polynomial params) : have Ah := GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy h u; ev strategy.state (opTensor (Ah * (sandwichedPolynomialSubMeasAt params strategy T u).outcome h' * Ah) (T.outcome h)) = (if h.toFun u = h'.toFun u then 1 else 0) * ev strategy.state (opTensor ((sandwichedPolynomialSubMeasAt params strategy T u).outcome h') (T.outcome h))

Expectation form of the point-projector insertion identity.

This is the scalar version of pointConditioned_sandwichedPolynomialOutcome_outer_eq_ite, with the agreement condition written as the real-valued indicator that appears in the paper's off-diagonal residual estimate.

theorem MIPStarRE.LDT.SelfImprovement.polynomial_off_diagonal_outer_sandwich_eq_indicator_avg {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) : (avgOver (uniformDistribution (Point params)) fun (u : Point params) => ∑ h : Polynomial params, ∑ h' ∈ Finset.univ.erase h, have Ah := GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy h u; ev strategy.state (opTensor (Ah * (sandwichedPolynomialSubMeasAt params strategy T u).outcome h' * Ah) (T.outcome h))) = avgOver (uniformDistribution (Point params)) fun (u : Point params) => ∑ h : Polynomial params, ∑ h' ∈ Finset.univ.erase h, (if h.toFun u = h'.toFun u then 1 else 0) * ev strategy.state (opTensor ((sandwichedPolynomialSubMeasAt params strategy T u).outcome h') (T.outcome h))

Averaged off-diagonal form of the paper identity eq:h-blt.

The left-hand side is the off-diagonal contribution after inserting the outer point projector A^u_{h(u)}. The right-hand side removes that outer sandwich and records the surviving summands by the agreement indicator 1_{h(u)=h'(u)}.

theorem MIPStarRE.LDT.SelfImprovement.sandwichedPolynomialOutcome_mul_pointConditioned_eq_ite {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) (u : Point params) (h h' : Polynomial params) : have Ah := GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy h u; (sandwichedPolynomialSubMeasAt params strategy T u).outcome h' * Ah = if h.toFun u = h'.toFun u then (sandwichedPolynomialSubMeasAt params strategy T u).outcome h' else 0

Right multiplication form of the point-projector identity.

For a point u, multiplying the pointwise helper outcome H^u_{h'} on the right by A^u_{h(u)} retains exactly the summands with h(u)=h'(u). Together with pointConditioned_sandwichedPolynomialOutcome_outer_eq_ite, this is the operator identity used to pass from the enlarged outer-sandwich expression to the paper's eq:delete-an-A form.

theorem MIPStarRE.LDT.SelfImprovement.pointConditioned_sandwichedPolynomialOutcome_outer_eq_right {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) (u : Point params) (h h' : Polynomial params) : have Ah := GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy h u; Ah * (sandwichedPolynomialSubMeasAt params strategy T u).outcome h' * Ah = (sandwichedPolynomialSubMeasAt params strategy T u).outcome h' * Ah

The full outer point-sandwich equals the one-sided delete-an-A form.

This is the operator identity underlying the paper's passage from the enlarged sum in eq:threw-in-h-prime to eq:delete-an-A.

theorem MIPStarRE.LDT.SelfImprovement.polynomial_collision_pointMeasurement_sandwichTensor_avg_le_mdq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) : (avgOver (uniformDistribution (Point params)) fun (v : Point params) => ∑ gg : Polynomial params × Polynomial params, ∑ a : Fq params, (if gg.1 = gg.2 then 0 else avgOver (uniformDistribution (Point params)) fun (u : Point params) => if gg.1.toFun u = gg.2.toFun u then 1 else 0) * ev strategy.state (opTensor ((strategy.pointMeasurement v).outcome a * T.outcome gg.1 * (strategy.pointMeasurement v).outcome a) (T.outcome gg.2))) ≤ ↑params.m * ↑params.d / ↑params.q

Schwartz--Zippel bound for the point-measurement sandwich collision term.

After the two variance swaps in the helper strong self-consistency proof, the polynomial-agreement indicator is independent of the point v at which the outer point measurement is evaluated. Averaging over v, the tensor-form Schwartz--Zippel estimate from the preliminaries bounds the whole collision term by m d / q.

theorem MIPStarRE.LDT.SelfImprovement.polynomial_off_diagonal_swapped_indicator_sandwich_avg_le_mdq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) : (avgOver (uniformDistribution (Point params)) fun (v : Point params) => ∑ h : Polynomial params, ∑ h' ∈ Finset.univ.erase h, (avgOver (uniformDistribution (Point params)) fun (u : Point params) => if h.toFun u = h'.toFun u then 1 else 0) * ev strategy.state (opTensor (GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy h v * T.outcome h' * GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy h v) (T.outcome h))) ≤ ↑params.m * ↑params.d / ↑params.q

Schwartz--Zippel bound for the selected off-diagonal residual endpoint.

This is the endpoint used after the variance swaps in the helper strong-self-consistency residual estimate. The selected outer point-measurement outcome A^v_{h(v)} is bounded by the full sum over field outcomes in polynomial_collision_pointMeasurement_sandwichTensor_avg_le_mdq.

theorem MIPStarRE.LDT.SelfImprovement.addInURightQuantity_selfConsistencySelection_eq_simplified {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) : addInURightQuantity params strategy (sandwichedPolynomialSubMeasAt params strategy T) T (selfConsistencyAddInUSelection params) = avgOver (uniformDistribution (Point params)) fun (u : Point params) => ∑ h : Polynomial params, ev strategy.state (opTensor ((sandwichedPolynomialSubMeasAt params strategy T u).outcome h) (T.outcome h))

Projective simplification of the diagonal add-in-u right quantity.

This is the projection-collapsed paper expression: the two outer A^u_{h(u)} factors absorb into the inner sandwich H^u_h = A^u_{h(u)} T_h A^u_{h(u)}, leaving the cleaner form E_u Σ_h ⟨ψ, H^u_h ⊗ T_h ψ⟩ used in the simplified scalar transfer.