Scalar chain for the diagonal add-in-u transfer

This module contains the selected and diagonal Q₀--Q₄ scalar chains used for the projection-simplified diagonal add-in-u transfer, together with the endpoint identifications needed by the helper strong-self-consistency proof.

References

• references/ldt-paper/self_improvement.tex lines 247--252
• blueprint/src/chapter/ch07_self_improvement.tex

Scalar chain for the projection-simplified diagonal add-in-u transfer

theorem MIPStarRE.LDT.SelfImprovement.addInU_pointMeasurement_snd_selfConsistency {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (delta : Error) (hssc : BipartiteSSCRel strategy.state (uniformDistribution (Point params)) strategy.pointMeasurement.toIdxSubMeas delta) : SDDRel strategy.state (uniformDistribution (Point params × Point params)) (IdxSubMeas.liftLeft fun (uv : Point params × Point params) => (strategy.pointMeasurement uv.2).toSubMeas) (IdxSubMeas.liftRight fun (uv : Point params × Point params) => (strategy.pointMeasurement uv.2).toSubMeas) (2 * delta)

Strong self-consistency for the point measurement, pulled back to the second coordinate of the independent (u, v) average used by the add-in-u scalar chain.

This is the distributional self-consistency input for the A^v_{h(v)} moves in self_improvement.tex, lines 255--297: the point measurement sampled at v has the same 2δ left/right state-dependent distance after the product average over (u, v).

theorem MIPStarRE.LDT.SelfImprovement.addInU_filtered_sandwiched_tensor_sum_le_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) (u v : Point params) (a : Fq params) : ∑ h : Polynomial params with h.toFun v = a, opTensor ((sandwichedPolynomialSubMeasAt params strategy T u).outcome h) (T.outcome h) ≤ 1

The grouped tensor mass over a fiber h(v)=a is a contraction.

This is the submeasurement bound used inside the first Cauchy--Schwarz square root in self_improvement.tex, lines 267--272: after grouping by the value a = h(v), the selected operators H^u_h ⊗ T_h are dominated by the total mass of the sandwiched polynomial submeasurement at u, hence by I.

Selection-parametrized add-in-u scalar chain

The paper proves lem:add-in-u for an arbitrary outcome family M and selection S_u ⊆ 𝒪 × polyfunc. The diagonal helper strong-self-consistency application below is one specialization of this statement. The following definitions record the same five scalar quantities before specializing to the diagonal case, so that the off-diagonal point-consistency selection can reuse the Cauchy--Schwarz chain rather than restating the transfer hypothesis.

noncomputable def MIPStarRE.LDT.SelfImprovement.addInUSelectedCSChainQ0 {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (M : IdxSubMeas (Point params) Outcome ι) (T : SubMeas (Polynomial params) ι) (S : AddInUSelection params Outcome) : Error

The selected-chain left endpoint Q₀.

For a selected pair (o, h) ∈ S_u, this is the expectation of M^u_o ⊗ H^v_h, where H^v_h = A^v_{h(v)} T_h A^v_{h(v)}.

Equations

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

noncomputable def MIPStarRE.LDT.SelfImprovement.addInUSelectedCSChainQ1 {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (M : IdxSubMeas (Point params) Outcome ι) (T : SubMeas (Polynomial params) ι) (S : AddInUSelection params Outcome) : Error

The selected-chain scalar Q₁, after moving the right point projector A^v_{h(v)} to the left tensor factor once.

Equations

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

noncomputable def MIPStarRE.LDT.SelfImprovement.addInUSelectedCSChainQ2 {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (M : IdxSubMeas (Point params) Outcome ι) (T : SubMeas (Polynomial params) ι) (S : AddInUSelection params Outcome) : Error

The selected-chain scalar Q₂, after moving both right point projectors to the left tensor factor.

Equations

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

noncomputable def MIPStarRE.LDT.SelfImprovement.addInUSelectedCSChainQ3 {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (M : IdxSubMeas (Point params) Outcome ι) (T : SubMeas (Polynomial params) ι) (S : AddInUSelection params Outcome) : Error

The selected-chain scalar Q₃, after replacing the first point projector at v by the corresponding point projector at u.

Equations

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

noncomputable def MIPStarRE.LDT.SelfImprovement.addInUSelectedCSChainQ4 {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (M : IdxSubMeas (Point params) Outcome ι) (T : SubMeas (Polynomial params) ι) (S : AddInUSelection params Outcome) : Error

The selected-chain scalar Q₄, after replacing both point projectors at v by the corresponding point projectors at u.

Equations

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

theorem MIPStarRE.LDT.SelfImprovement.addInUSelectedCSChainQ0_eq_leftQuantity_averagedSandwiched {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (M : IdxSubMeas (Point params) Outcome ι) (T : SubMeas (Polynomial params) ι) (S : AddInUSelection params Outcome) : addInULeftQuantity params strategy M (averagedSandwichedPolynomialSubMeas params strategy T) S = addInUSelectedCSChainQ0 params strategy M T S

The selected-chain endpoint Q₀ is the generic add-in-u left quantity when the second measurement is the averaged sandwiched polynomial submeasurement.

theorem MIPStarRE.LDT.SelfImprovement.addInUSelectedCSChainQ4_eq_rightQuantity {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (M : IdxSubMeas (Point params) Outcome ι) (T : SubMeas (Polynomial params) ι) (S : AddInUSelection params Outcome) : addInURightQuantity params strategy M T S = addInUSelectedCSChainQ4 params strategy M T S

The selected-chain endpoint Q₄ is the generic add-in-u right quantity.

noncomputable def MIPStarRE.LDT.SelfImprovement.addInUCSChainQ0 {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) : Error

The expanded left endpoint Q₀ of the four-step scalar chain in self_improvement.tex, lines 247--252, after setting M^u = H^u and averaging the second tensor factor H = E_v H^v.

Equations

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

noncomputable def MIPStarRE.LDT.SelfImprovement.addInUCSChainQ1 {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) : Error

The scalar Q₁ obtained from Q₀ by moving the right point projection A^v_{h(v)} to the left tensor factor; this is the target of eq:move-one.

Equations

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

noncomputable def MIPStarRE.LDT.SelfImprovement.addInUCSChainQ2 {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) : Error

The scalar Q₂ obtained from Q₁ by moving the second right point projection to the left tensor factor; this is the target of eq:move-another.

Equations

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

noncomputable def MIPStarRE.LDT.SelfImprovement.addInUCSChainQ3 {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) : Error

The scalar Q₃ obtained from Q₂ by replacing the first point projection A^v_{h(v)} by A^u_{h(u)}; this is the target of eq:change-one.

Equations

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

noncomputable def MIPStarRE.LDT.SelfImprovement.addInUCSChainQ4 {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) : Error

The scalar Q₄ obtained from Q₃ by replacing the second point projection A^v_{h(v)} by A^u_{h(u)}; after the projection collapse, this is the projection-simplified right endpoint of the diagonal add-in-u transfer.

Equations

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

theorem MIPStarRE.LDT.SelfImprovement.add_in_u_cs_chain_q0_eq_match_mass {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) : qBipartiteMatchMass strategy.state (averagedSandwichedPolynomialSubMeas params strategy T) (averagedSandwichedPolynomialSubMeas params strategy T) = addInUCSChainQ0 params strategy T

The expanded chain endpoint Q₀ is the existing diagonal match-mass left side used by selfConsistencyDiagonalAddInU_of_simplifiedTransfer.

theorem MIPStarRE.LDT.SelfImprovement.add_in_u_cs_chain_q4_eq_simplified_rhs {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) : addInUCSChainQ4 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))

The raw chain endpoint Q₄ collapses to the projection-simplified scalar right side used by selfConsistencyDiagonalAddInU_of_simplifiedTransfer.