Add-in-u scalar transfer and off-diagonal expansion #
Assembly of the four add-in-u scalar moves, the arithmetic absorption of the paper, and the
residual off-diagonal expansion used by the helper strong self-consistency argument: the
counterpart of the vendored SelfImprovement/Theorems/Results/AddInUStep34AndTransfer/Transfer.lean
(under MIPRE/Background/LIDT/MIPStarRE/LDT/) in the port of planning/c6b-plan.md (milestone
M10, section "Port conventions").
Contents #
add_in_u_simplified_transfer_of_cs_chain,add_in_u_selected_transfer_of_cs_chain: the triangle inequality alongQ₀ → Q₁ → Q₂ → Q₃ → Q₄, for the diagonal and the selected chains.add_in_u_simplified_transfer_of_cs_chain_sqrt_formand its_local_variance_formand_selfConsistency_local_variance_formclosings, which discharge the four step bounds in turn.selfConsistencyDiagonalAddInU_of_simplifiedTransfer: the projection-simplified transfer gives the released one.helper_mass_sub_release_eq_polynomial_off_diagonal: the helper mass minus the released right side is the off-diagonal sumE_u ∑_h ∑_{h' ≠ h} ⟨ψ, H^u_{h'} ⊗ T_h ψ⟩.
Every scalar is strategy.state.ev of a joint operator; opTensor A B is
strategy.state.opTensor A B, leftTensor (ι₂ := ι) A is strategy.state.L A,
qBipartiteMatchMass strategy.state and subMeasMass strategy.state are the SymModel/VecState
declarations reached by dot notation, and A.liftLeft is A.liftLeft strategy.state. The vendored
try rfl step ev (leftTensor X) = ev (opTensor X 1) is the keystone's rightTensor_one under
mul_one. No
statement of the vendored file carries a swap, density or normalization hypothesis, so no statement
changed; the file sets no option, the vendored file-wide respectTransparency false not being
needed.
The vendored module is imported for its three classical declarations; its imports, the vendored
AddInUStep34AndTransfer/{Selected,Variance}, are already imported by Co Selected and Variance.
Not ported #
two_sqrt_two_mul_add_two_sqrt_le_four_sqrt: classical, imported.two_mul_delta_le_selfImprovementVarianceError: classical, imported.two_sqrt_two_delta_add_two_sqrt_selfImprovementVarianceError_le_addInUError: classical, imported.
References #
In LionSR/MIPStarRE at commit 507e8122, not in this repository:
references/ldt-paper/self_improvement.texlines 341--343blueprint/src/chapter/ch07_self_improvement.tex
Assemble the projection-simplified scalar transfer from the four scalar
chain moves. The analytic work remains exactly the four bounds
Q₀ ≈ Q₁, Q₁ ≈ Q₂, Q₂ ≈ Q₃, and Q₃ ≈ Q₄, plus the final arithmetic
absorption into addInUError.
Assemble the selected add-in-u scalar transfer from the four selected
scalar chain moves.
This is the selection-parametrized counterpart of
add_in_u_simplified_transfer_of_cs_chain. The endpoints are the theorem-side
generic add-in-u quantities rather than the diagonal match-mass and simplified
release quantities.
Wrapper composing add_in_u_simplified_transfer_of_cs_chain with the
arithmetic absorption: when the four chain step bounds have the paper-faithful
shapes √(2 δ), √(2 δ), √(ζ_variance), √(ζ_variance), the
projection-simplified transfer holds with the displayed
addInUError = 4 ζ_variance^{1/2}.
Projection-simplified add-in-u transfer with the Step 3/4 variance bounds
supplied by the local-variance sum hypothesis.
After the factor estimates of Co AddInUStep34AndTransfer/Variance, the remaining scalar
hypotheses are only the two self-consistency moves Q₀ → Q₁ and Q₁ → Q₂, together with the
local-variance sum bound from the GlobalVariance theorem.
Projection-simplified add-in-u transfer from point self-consistency and
the local-variance sum bound.
This closes all four scalar moves in the add-in-u chain: Step 1 and Step 2
come from point-measurement self-consistency, while Step 3 and Step 4 are
supplied by the local-variance form above.
Specialization of the diagonal add-in-u transfer to the projection-simplified scalar
transfer hypothesis.
The hypothesis is stated against the cleaner right-hand side E_u Σ_h ⟨ψ, H^u_h ⊗ T_h ψ⟩
obtained after collapsing the outer projection factors of eq:release-the-kraken via
proj_outer_sandwich_eq; the conclusion is the released form, with A^u_{h(u)} on both sides
of H^u_h. Both right-hand sides are addInURightQuantity of the self-consistency selection.
Exact residual-side expansion for the helper strong self-consistency proof.
For the averaged helper Hhat = E_u H^u produced from the primal measurement
T, the difference between the helper left mass and the released diagonal
add-in-u right-hand side is precisely the contribution of the off-diagonal
polynomial pairs (h',h) with h' ≠ h:
E_u \sum_h \sum_{h'≠h} ⟨ψ, H^u_{h'} ⊗ T_h ψ⟩.
This is the exact algebraic opening of the residual helper_left_mass - release-the-kraken;
the later Cauchy--Schwarz, Schwartz--Zippel, point-consistency, and self-consistency estimates
bound this off-diagonal expression in the proof of item:self-improvement-self. It differs from
the paper's intermediate "threw-in-h'" expression, where the off-diagonal helper operator is
still sandwiched by A^u_{h(u)}.