Off-diagonal residual estimates for the helper SSC argument

The off-diagonal scalar quantities appearing after the projector insertion in the helper strong-self-consistency proof, their exact decompositions, and the assembly of the two variance-transport comparisons with the Schwartz--Zippel endpoint: the counterpart of the vendored SelfImprovement/Theorems/Results/AddInUDiagonalAndDefs/Residual.lean (under MIPRE/Background/LIDT/MIPStarRE/LDT/) in the port of planning/c6b-plan.md (milestone M10, section "Port conventions").

A strategy is a SymStrat params 𝔓 K; the polynomial submeasurement T and the point projectors live in 𝔓, and every scalar quantity is strategy.state.ev of a joint operator strategy.state.opTensor X Y. The statements are the vendored ones, translated; none of them has a swap or normalization hypothesis. The error term selfImprovementVarianceError is classical and imported from the vendored SelfImprovement/Defs.lean.

Not ported

Every declaration of the vendored file has a counterpart here.

References

In LionSR/MIPStarRE at commit 507e8122, not in this repository:

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

Off-diagonal residual quantities for the helper SSC estimate

noncomputable def MIPRE.LIDT.Co.SelfImprovement.helperOffDiagonalOuterSandwichQuantity {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) : ℝ

The off-diagonal contribution after inserting the outer point projector A^u_{h(u)} around the pointwise helper outcome H^u_{h'}.

This is the non-diagonal term added when the diagonal released expression is enlarged to the full (h,h') sum in the proof of helper strong self-consistency.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.LIDT.Co.SelfImprovement.helperOffDiagonalIndicatorQuantity {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) : ℝ

The same off-diagonal contribution after using eq:h-blt: the outer projector has been removed from the operator and replaced by the polynomial agreement indicator 1_{h(u)=h'(u)}.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.LIDT.Co.SelfImprovement.helperOffDiagonalOneSidedSwappedIndicatorQuantity {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) : ℝ

The intermediate off-diagonal expression after the first variance swap.

The left copy of the point projector has been evaluated at an independent point v, while the right copy is still evaluated at the original point u. This is the Lean scalar form of the expression in the paper immediately after eq:swapped-u-for-v.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.LIDT.Co.SelfImprovement.helperOffDiagonalSwappedIndicatorQuantity {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) : ℝ

The post-variance-swap endpoint for the off-diagonal contribution.

Here both copies of the point projector have been evaluated at an independent point v, while the agreement indicator has already been averaged over the original point u. This is the scalar expression to which the Schwartz--Zippel estimate is applied.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.LIDT.Co.SelfImprovement.helperFullOuterSandwichQuantity {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) : ℝ

The full enlarged expression after inserting the outer point projector.

This includes both the diagonal and off-diagonal pairs (h,h'), and is the right-hand side of eq:threw-in-h-prime before applying eq:h-blt.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.LIDT.Co.SelfImprovement.helperFullOuterSandwichQuantity_eq_release_add_offDiagonalOuterSandwichQuantity {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) : helperFullOuterSandwichQuantity params strategy T = addInURightQuantity params strategy (sandwichedPolynomialSubMeasAt params strategy T) T (MIPStarRE.LDT.SelfImprovement.selfConsistencyAddInUSelection params) + helperOffDiagonalOuterSandwichQuantity params strategy T

The full inserted expression splits into its released diagonal part and its off-diagonal remainder.

This is the finite-sum identity underlying the passage from eq:release-the-kraken to eq:threw-in-h-prime: for each fixed polynomial h, the sum over all h' is the diagonal term h' = h plus the sum over h' ≠ h.

noncomputable def MIPRE.LIDT.Co.SelfImprovement.helperDeleteAQuantity {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) : ℝ

The full enlarged expression after deleting the left copy of the point projector.

This is the paper's eq:delete-an-A scalar quantity.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.LIDT.Co.SelfImprovement.helperFullOuterSandwichQuantity_eq_deleteAQuantity {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) : helperFullOuterSandwichQuantity params strategy T = helperDeleteAQuantity params strategy T

Formal version of the paper's eq:delete-an-A identity.

noncomputable def MIPRE.LIDT.Co.SelfImprovement.helperDeleteAClonedQuantity {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) : ℝ

The delete-an-A expression after replacing the remaining point projector by an independent point.

This is the scalar quantity on the right-hand side of the paper's eq:swap-u-for-v-attack-of-the-clones.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.LIDT.Co.SelfImprovement.helperMoveOverVQuantity {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) : ℝ

The expression obtained after moving the remaining point projector to the right tensor factor.

This is the scalar quantity on the right-hand side of the paper's eq:move-over-v.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.LIDT.Co.SelfImprovement.helperDeleteAQuantity_le_moveOverV_of_abs_transports {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (eps delta : ℝ) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (hclone : |helperDeleteAQuantity params strategy T - helperDeleteAClonedQuantity params strategy T| ≤ √(MIPStarRE.LDT.SelfImprovement.selfImprovementVarianceError params eps delta)) (hmove : |helperDeleteAClonedQuantity params strategy T - helperMoveOverVQuantity params strategy T| ≤ √(2 * delta)) : helperDeleteAQuantity params strategy T ≤ helperMoveOverVQuantity params strategy T + √(MIPStarRE.LDT.SelfImprovement.selfImprovementVarianceError params eps delta) + √(2 * delta)

Assemble the post-delete-an-A transport estimates.

The first hypothesis is the variance replacement A^u_{h(u)} → A^v_{h(v)} in eq:swap-u-for-v-attack-of-the-clones. The second hypothesis is the self-consistency move eq:move-over-v, which moves the remaining point projector from Alice's tensor factor to Bob's tensor factor. This lemma only performs the scalar triangle-inequality assembly; the analytic proofs of the two displayed hypotheses remain separate.

theorem MIPRE.LIDT.Co.SelfImprovement.helperMoveOverVQuantity_le_deleteA_of_abs_transports {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (eps delta : ℝ) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (hclone : |helperDeleteAQuantity params strategy T - helperDeleteAClonedQuantity params strategy T| ≤ √(MIPStarRE.LDT.SelfImprovement.selfImprovementVarianceError params eps delta)) (hmove : |helperDeleteAClonedQuantity params strategy T - helperMoveOverVQuantity params strategy T| ≤ √(2 * delta)) : helperMoveOverVQuantity params strategy T ≤ helperDeleteAQuantity params strategy T + √(MIPStarRE.LDT.SelfImprovement.selfImprovementVarianceError params eps delta) + √(2 * delta)

The reverse scalar direction of the post-delete-an-A transport estimates.

This is the direction used when the final move-over-v expression is known to be large and one transfers that lower bound back to the delete-an-A expression. It is again only the triangle-inequality assembly of the two analytic transport estimates.

theorem MIPRE.LIDT.Co.SelfImprovement.helperOffDiagonalOuterSandwichQuantity_eq_indicator {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) : helperOffDiagonalOuterSandwichQuantity params strategy T = helperOffDiagonalIndicatorQuantity params strategy T

Named form of the identity eq:h-blt for the off-diagonal helper SSC quantity.

theorem MIPRE.LIDT.Co.SelfImprovement.helperOffDiagonalSwappedIndicatorQuantity_le_mdq {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) : helperOffDiagonalSwappedIndicatorQuantity params strategy T ≤ ↑params.m * ↑params.d / ↑params.q

Named Schwartz--Zippel endpoint for the helper SSC off-diagonal term.

theorem MIPRE.LIDT.Co.SelfImprovement.helperOffDiagonalIndicatorQuantity_le_swapped_of_abs_transports {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (eps delta : ℝ) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (hleft : |helperOffDiagonalIndicatorQuantity params strategy T - helperOffDiagonalOneSidedSwappedIndicatorQuantity params strategy T| ≤ √(MIPStarRE.LDT.SelfImprovement.selfImprovementVarianceError params eps delta)) (hright : |helperOffDiagonalOneSidedSwappedIndicatorQuantity params strategy T - helperOffDiagonalSwappedIndicatorQuantity params strategy T| ≤ √(MIPStarRE.LDT.SelfImprovement.selfImprovementVarianceError params eps delta)) : helperOffDiagonalIndicatorQuantity params strategy T ≤ helperOffDiagonalSwappedIndicatorQuantity params strategy T + 2 * √(MIPStarRE.LDT.SelfImprovement.selfImprovementVarianceError params eps delta)

Assemble the two one-projector variance transports for the off-diagonal helper residual.

The first hypothesis is the estimate for replacing the left copy of A^u_{h(u)} by A^v_{h(v)}. The second hypothesis is the estimate for replacing the remaining right copy by the same independent point v. Together they give the transport inequality used before the Schwartz--Zippel endpoint in the proof of helper strong self-consistency.

theorem MIPRE.LIDT.Co.SelfImprovement.helperOffDiagonalOuterSandwichQuantity_le_of_swapped_transport {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (η : ℝ) (htransport : helperOffDiagonalIndicatorQuantity params strategy T ≤ helperOffDiagonalSwappedIndicatorQuantity params strategy T + η) : helperOffDiagonalOuterSandwichQuantity params strategy T ≤ η + ↑params.m * ↑params.d / ↑params.q

Assemble the off-diagonal projector-insertion bound from the two variance swaps and the Schwartz--Zippel endpoint.

The hypothesis htransport is precisely the analytic content of the two Cauchy--Schwarz variance moves in the proof of item:self-improvement-self: it transports the indicator form of the off-diagonal term to the endpoint with both point projectors evaluated at the independent point v. The conclusion is the corresponding paper estimate before substituting the concrete value of the transport error.

theorem MIPRE.LIDT.Co.SelfImprovement.helperOffDiagonalOuterSandwichQuantity_le_two_sqrt_variance_add_mdq {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (eps delta : ℝ) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (htransport : helperOffDiagonalIndicatorQuantity params strategy T ≤ helperOffDiagonalSwappedIndicatorQuantity params strategy T + 2 * √(MIPStarRE.LDT.SelfImprovement.selfImprovementVarianceError params eps delta)) : helperOffDiagonalOuterSandwichQuantity params strategy T ≤ 2 * √(MIPStarRE.LDT.SelfImprovement.selfImprovementVarianceError params eps delta) + ↑params.m * ↑params.d / ↑params.q

Paper-shaped form of the off-diagonal projector-insertion estimate.

Once the two variance swaps have supplied transport error 2√ζ_variance, the inserted off-diagonal contribution is bounded by 2√ζ_variance + md/q.

theorem MIPRE.LIDT.Co.SelfImprovement.helperOffDiagonalOuterSandwichQuantity_le_two_sqrt_variance_add_mdq_of_abs_transports {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (eps delta : ℝ) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (hleft : |helperOffDiagonalIndicatorQuantity params strategy T - helperOffDiagonalOneSidedSwappedIndicatorQuantity params strategy T| ≤ √(MIPStarRE.LDT.SelfImprovement.selfImprovementVarianceError params eps delta)) (hright : |helperOffDiagonalOneSidedSwappedIndicatorQuantity params strategy T - helperOffDiagonalSwappedIndicatorQuantity params strategy T| ≤ √(MIPStarRE.LDT.SelfImprovement.selfImprovementVarianceError params eps delta)) : helperOffDiagonalOuterSandwichQuantity params strategy T ≤ 2 * √(MIPStarRE.LDT.SelfImprovement.selfImprovementVarianceError params eps delta) + ↑params.m * ↑params.d / ↑params.q

Paper-shaped off-diagonal bound from the two explicit variance transports.

This version exposes the two Cauchy--Schwarz/global-variance moves separately: first from the indicator form to the one-sided swapped expression, and then from the one-sided swapped expression to the Schwartz--Zippel endpoint.