Add-in-u scalar transfer and off-diagonal expansion

Assembly of the four add-in-u scalar moves, the elementary arithmetic absorption from the paper, and the residual off-diagonal expansion used by the helper strong self-consistency argument.

References

• references/ldt-paper/self_improvement.tex lines 341--343
• blueprint/src/chapter/ch07_self_improvement.tex

theorem MIPStarRE.LDT.SelfImprovement.add_in_u_simplified_transfer_of_cs_chain {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta : Error) (T : SubMeas (Polynomial params) ι) (η01 η12 η23 η34 : Error) (h01 : |addInUCSChainQ0 params strategy T - addInUCSChainQ1 params strategy T| ≤ η01) (h12 : |addInUCSChainQ1 params strategy T - addInUCSChainQ2 params strategy T| ≤ η12) (h23 : |addInUCSChainQ2 params strategy T - addInUCSChainQ3 params strategy T| ≤ η23) (h34 : |addInUCSChainQ3 params strategy T - addInUCSChainQ4 params strategy T| ≤ η34) (hsum : η01 + η12 + η23 + η34 ≤ 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, ev strategy.state (opTensor ((sandwichedPolynomialSubMeasAt params strategy T u).outcome h) (T.outcome h))| ≤ addInUError params eps delta

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.

theorem MIPStarRE.LDT.SelfImprovement.add_in_u_selected_transfer_of_cs_chain {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta : Error) (M : IdxSubMeas (Point params) Outcome ι) (T : SubMeas (Polynomial params) ι) (S : AddInUSelection params Outcome) (η01 η12 η23 η34 : Error) (h01 : |addInUSelectedCSChainQ0 params strategy M T S - addInUSelectedCSChainQ1 params strategy M T S| ≤ η01) (h12 : |addInUSelectedCSChainQ1 params strategy M T S - addInUSelectedCSChainQ2 params strategy M T S| ≤ η12) (h23 : |addInUSelectedCSChainQ2 params strategy M T S - addInUSelectedCSChainQ3 params strategy M T S| ≤ η23) (h34 : |addInUSelectedCSChainQ3 params strategy M T S - addInUSelectedCSChainQ4 params strategy M T S| ≤ η34) (hsum : η01 + η12 + η23 + η34 ≤ addInUError params eps delta) : |addInULeftQuantity params strategy M (averagedSandwichedPolynomialSubMeas params strategy T) S - addInURightQuantity params strategy M T S| ≤ addInUError params eps delta

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.

theorem MIPStarRE.LDT.SelfImprovement.two_sqrt_two_mul_add_two_sqrt_le_four_sqrt {a b : Error} (hab : 2 * a ≤ b) : 2 * √(2 * a) + 2 * √b ≤ 4 * √b

Reusable numerical absorption: whenever 2 a ≤ b, the four-term sum 2 √(2 a) + 2 √b collapses into 4 √b. This is the schematic shape of the paper's closing absorption step in the proof of lem:add-in-u (self_improvement.tex:341--342).

theorem MIPStarRE.LDT.SelfImprovement.two_mul_delta_le_selfImprovementVarianceError (params : Parameters) [FieldModel params.q] (eps delta : Error) (heps : 0 ≤ eps) (hdelta : 0 ≤ delta) : 2 * delta ≤ selfImprovementVarianceError params eps delta

Paper-side comparison 2 δ ≤ ζ_variance from the closing line of the proof of lem:add-in-u (self_improvement.tex:342, blueprint/src/chapter/ch07_self_improvement.tex:494). Since ζ_variance = 24 m (ε + δ + m d / q) and m ≥ 1, the term 24 m δ already exceeds 2 δ whenever eps, delta ≥ 0.

theorem MIPStarRE.LDT.SelfImprovement.two_sqrt_two_delta_add_two_sqrt_selfImprovementVarianceError_le_addInUError (params : Parameters) [FieldModel params.q] (eps delta : Error) (heps : 0 ≤ eps) (hdelta : 0 ≤ delta) : 2 * √(2 * delta) + 2 * √(selfImprovementVarianceError params eps delta) ≤ addInUError params eps delta

Arithmetic absorption used by add_in_u_simplified_transfer_of_cs_chain: the four step-bound sum 2 √(2 δ) + 2 √(ζ_variance) is dominated by addInUError = 4 ζ_variance^{1/2} (self_improvement.tex:341--342, blueprint/src/chapter/ch07_self_improvement.tex:492--494). This is the arithmetic side condition that lets the step bounds with the paper-faithful Real.sqrt shape (companion issues #1089 and #1090) discharge the hsum hypothesis of add_in_u_simplified_transfer_of_cs_chain.

theorem MIPStarRE.LDT.SelfImprovement.add_in_u_simplified_transfer_of_cs_chain_sqrt_form {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta : Error) (heps : 0 ≤ eps) (hdelta : 0 ≤ delta) (T : SubMeas (Polynomial params) ι) (h01 : |addInUCSChainQ0 params strategy T - addInUCSChainQ1 params strategy T| ≤ √(2 * delta)) (h12 : |addInUCSChainQ1 params strategy T - addInUCSChainQ2 params strategy T| ≤ √(2 * delta)) (h23 : |addInUCSChainQ2 params strategy T - addInUCSChainQ3 params strategy T| ≤ √(selfImprovementVarianceError params eps delta)) (h34 : |addInUCSChainQ3 params strategy T - addInUCSChainQ4 params strategy T| ≤ √(selfImprovementVarianceError 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, ev strategy.state (opTensor ((sandwichedPolynomialSubMeasAt params strategy T u).outcome h) (T.outcome h))| ≤ addInUError params eps delta

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}. The four hypotheses match the targets of companion issues #1089 (Step 1/2) and #1083/#1088/#1090 (Step 3/4).

theorem MIPStarRE.LDT.SelfImprovement.add_in_u_simplified_transfer_of_cs_chain_local_variance_form {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta : Error) (heps : 0 ≤ eps) (hdelta : 0 ≤ delta) (T : SubMeas (Polynomial params) ι) (hlocal : ∑ g : Polynomial params, GlobalVariance.localVarianceDeviationAtPolynomial params strategy strategy.state T g ≤ GlobalVariance.localVarianceOfPointsError params eps delta) (h01 : |addInUCSChainQ0 params strategy T - addInUCSChainQ1 params strategy T| ≤ √(2 * delta)) (h12 : |addInUCSChainQ1 params strategy T - addInUCSChainQ2 params strategy T| ≤ √(2 * delta)) : |qBipartiteMatchMass strategy.state (averagedSandwichedPolynomialSubMeas params strategy T) (averagedSandwichedPolynomialSubMeas params strategy T) - 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))| ≤ addInUError params eps delta

Projection-simplified add-in-u transfer with the Step 3/4 variance bounds supplied by the local-variance sum hypothesis.

After the factor estimates in this file, 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.

theorem MIPStarRE.LDT.SelfImprovement.add_in_u_simplified_transfer_of_cs_chain_selfConsistency_local_variance_form {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta : Error) (heps : 0 ≤ eps) (hdelta : 0 ≤ delta) (T : SubMeas (Polynomial params) ι) (hssc : BipartiteSSCRel strategy.state (uniformDistribution (Point params)) strategy.pointMeasurement.toIdxSubMeas delta) (hlocal : ∑ g : Polynomial params, GlobalVariance.localVarianceDeviationAtPolynomial params strategy strategy.state T g ≤ GlobalVariance.localVarianceOfPointsError 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, ev strategy.state (opTensor ((sandwichedPolynomialSubMeasAt params strategy T u).outcome h) (T.outcome h))| ≤ addInUError params eps delta

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.

theorem MIPStarRE.LDT.SelfImprovement.selfConsistencyDiagonalAddInU_of_simplifiedTransfer {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta : Error) (T : SubMeas (Polynomial params) ι) (htransfer : |qBipartiteMatchMass strategy.state (averagedSandwichedPolynomialSubMeas params strategy T) (averagedSandwichedPolynomialSubMeas params strategy T) - 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))| ≤ 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 selfConsistencyDiagonalAddInU_of_transfer to the projection-simplified scalar transfer hypothesis.

Compared to selfConsistencyDiagonalAddInU_of_transfer, 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 identical and can therefore feed the same diagonal helper-SSC application; the simplification reduces the Cauchy--Schwarz/global-variance comparison (self_improvement.tex:247--343) to a transfer in the simpler shape.

theorem MIPStarRE.LDT.SelfImprovement.helper_mass_sub_release_eq_polynomial_off_diagonal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : Measurement (Polynomial params) ι) : subMeasMass strategy.state (averagedSandwichedPolynomialSubMeas params strategy T.toSubMeas).liftLeft - addInURightQuantity params strategy (sandwichedPolynomialSubMeasAt params strategy T.toSubMeas) T.toSubMeas (selfConsistencyAddInUSelection params) = avgOver (uniformDistribution (Point params)) fun (u : Point params) => ∑ h : Polynomial params, ∑ h' ∈ Finset.univ.erase h, ev strategy.state (opTensor ((sandwichedPolynomialSubMeasAt params strategy T.toSubMeas u).outcome h') (T.outcome h))

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 Lean residual helper_left_mass - release-the-kraken; the later Cauchy--Schwarz, Schwartz--Zippel, point-consistency, and self-consistency estimates are the remaining inequalities that bound this off-diagonal expression in the proof of item:self-improvement-self.

This Lean identity expands the helper left mass minus the released diagonal right-hand side directly. It therefore differs from the paper's intermediate ``threw-in-h''' expression, where the off-diagonal helper operator is still sandwiched by A^u_{h(u)}.