Boundedness transport decomposition identities #
This file contains the algebraic reindexing and off-diagonal decompositions used in the final-fields boundedness and point-consistency arguments. The identities come from the helper-stage agreement average in the proof of self-improvement.
References #
references/ldt-paper/self_improvement.texlines 435 and 612--613blueprint/src/chapter/ch07_self_improvement.tex
Scalar expansion of the averaged helper-agreement operator.
The expectation of the averaged agreement operator is the average, over the point question, of the scalar agreement between the point measurement and the postprocessed polynomial family.
Reindexing identity for the pointwise helper-agreement operator.
The fiberwise definition H_{[h(u)=a]} := ∑_{h : h(u)=a} H_h collapses the
a-summed expression ∑_a A^u_a ⊗ H_{[h(u)=a]} to the polynomial-indexed sum
∑_h A^u_{h(u)} ⊗ H_h, by expanding the tensor product fiberwise and applying
Finset.sum_fiberwise along h ↦ h u.
This is the first equality of the boundedness display in the proof of
\ref{item:self-improvement-boundedness}:
references/ldt-paper/self_improvement.tex line 612, mirrored at
blueprint/src/chapter/ch07_self_improvement.tex lines 274--282
("Reindexing the sum by~$h$"). It is a purely algebraic identity — no estimate,
no measurement structure used beyond the postprocess fiber decomposition built
into evaluateAt.
Reindexed expansion of the averaged helper-agreement operator.
Combining the pointwise reindexing identity
helperAgreementOperatorAtPoint_eq_sum_polynomial with
helper_agreement_average_ev_eq_avg, the scalar
⟨ψ| E_u Σ_a A^u_a ⊗ H_{[h(u)=a]} |ψ⟩ equals the polynomial-indexed expectation
E_u Σ_h ⟨ψ| A^u_{h(u)} ⊗ H_h |ψ⟩ from the second line of the boundedness
display in the proof of \ref{item:self-improvement-boundedness}
(references/ldt-paper/self_improvement.tex line 612;
blueprint/src/chapter/ch07_self_improvement.tex lines 274--282).
Off-diagonal decomposition of the pointwise helper boundedness slack.
For each point u, the difference between the right-placed total
I ⊗ H.total = ∑_h I ⊗ H_h and the pointwise helper-agreement operator
helperAgreementOperatorAtPoint params strategy H u = ∑_a A^u_a ⊗ H_{[h(u)=a]}
equals the off-diagonal sum
∑_h ∑_{a ≠ h(u)} A^u_a ⊗ H_h,
by combining the polynomial-indexed reindexing of helperAgreementOperatorAtPoint
from #1124 (helperAgreementOperatorAtPoint_eq_sum_polynomial) with
∑_a A^u_a = 1 (since pointMeasurement u is a measurement) and the bilinearity
of opTensor.
This is the operator-level form of the second algebraic identity in the
boundedness display in \ref{item:self-improvement-boundedness}
(references/ldt-paper/self_improvement.tex line 613, mirrored at
blueprint/src/chapter/ch07_self_improvement.tex lines 296--300, the step
"Combined with $\sum_a A_a^u = I$ and~\eqref{eq:explicit-bound-for-A-consistency}
this gives ..."). The averaged scalar form of the off-diagonal sum on the right
is the LHS of eq:explicit-bound-for-A-consistency (line 435), which the paper
bounds by 4 √ζ_variance.
Scalar form of the pointwise off-diagonal decomposition.
For each evaluation point u, the scalar slack
⟨ψ, I ⊗ H.total, ψ⟩ - ⟨ψ, helperAgreementOperatorAtPoint u, ψ⟩
is the sum of the off-diagonal masses
⟨ψ, A^u_a ⊗ H_h, ψ⟩ over the pairs with a ≠ h(u).
Averaged scalar form of the off-diagonal decomposition.
Composed from helperAgreementOperatorAtPoint_off_diagonal_decomposition by
applying the bilinearity of ev/avgOver over subtraction and averaging via
avgOver_uniform_const. The difference
⟨ψ, I ⊗ H.total, ψ⟩ - ⟨ψ, helperAgreementAverageOperator, ψ⟩ equals the
averaged off-diagonal scalar sum
E_u ∑_h ∑_{a ≠ h(u)} ⟨ψ, A^u_a ⊗ H_h, ψ⟩,
which is the LHS of eq:explicit-bound-for-A-consistency
(references/ldt-paper/self_improvement.tex line 435; blueprint
ch07_self_improvement.tex lines 153--168).