Diagonal add-in-u selection and point-sandwich endpoints #
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:
the counterpart of the vendored
SelfImprovement/Theorems/Results/AddInUDiagonalAndDefs/Selection.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 helper submeasurements live in 𝔓 and the add-in-u
operators are joint operators K →L[ℂ] K, built with strategy.state.opTensor. The selection
selfConsistencyAddInUSelection is classical and imported from the vendored file. The vendored
collision bound passed hnorm := strategy.isNormalized to
Preliminaries.polynomialCollision_sandwichTensor_le_mdq, whose ported form takes no
normalization hypothesis, and leftTensor_mul_rightTensor_eq_opTensor holds by rfl. The
state-free proj_outer_sandwich_eq holds in any semigroup.
Not ported #
selfConsistencyAddInUSelection: classical, imported.
References #
In LionSR/MIPStarRE at commit 507e8122, not in this repository:
references/ldt-paper/self_improvement.texlines 247--252, 455--468blueprint/src/chapter/ch07_self_improvement.tex
The diagonal selection at a point: the selected pairs (h, h) re-indexed by h.
The right add-in-u operator at a point for the diagonal selection, re-indexed by h.
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.
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.
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.
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. It is state-free, and holds in any semigroup (the vendored statement is on
MIPStarRE.Quantum.Op ι).
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.
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.
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)}.
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.
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.
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 (its vendored hypothesis hnorm is a theorem of the model).
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.
Projective simplification of the diagonal add-in-u right operator at a point.
Combining addInURightOperatorAtPoint_selfConsistencySelection with the
projectivity of strategy.pointMeasurement (each A^u_a * A^u_a = A^u_a),
the at-point operator collapses to the simpler tensor sum
Σ_h H^u_h ⊗ T_h where H^u_h = sandwichedPolynomialSubMeasAt T u 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.