Scalar chain for the diagonal add-in-u transfer

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: the counterpart of the vendored SelfImprovement/Theorems/Results/AddInUDiagonalAndDefs/ScalarChain.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 measurements M, T and the point projectors live in 𝔓, and every scalar of the chain is strategy.state.ev of a joint operator strategy.state.opTensor X Y. The statements are the vendored ones, translated:

• addInU_pointMeasurement_snd_selfConsistency places with IdxSubMeas.liftLeft strategy.state and IdxSubMeas.liftRight strategy.state. The vendored proof passes strategy.permInvState to Preliminaries.twoNotionsOfSelfConsistencyAfterEvaluation with the identity postprocessing; here the ported Preliminaries.twoNotionsOfSelfConsistency, which has no swap hypothesis, is applied directly.
• addInU_filtered_sandwiched_tensor_sum_le_one bounds a joint operator, ≤ (1 : K →L[ℂ] K), through SubMeas.opTensor_sum_filter_le_one strategy.state.

Not ported

Every declaration of the vendored file has a counterpart here.

References

In LionSR/MIPStarRE at commit 507e8122, not in this repository:

• 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 MIPRE.LIDT.Co.SelfImprovement.addInU_pointMeasurement_snd_selfConsistency {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (delta : ℝ) (hssc : strategy.state.BipartiteSSCRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurement.toIdxSubMeas delta) : strategy.state.SDDRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params × MIPStarRE.LDT.Point params)) (IdxSubMeas.liftLeft strategy.state fun (uv : MIPStarRE.LDT.Point params × MIPStarRE.LDT.Point params) => (strategy.pointMeasurement uv.2).toSubMeas) (IdxSubMeas.liftRight strategy.state fun (uv : MIPStarRE.LDT.Point params × MIPStarRE.LDT.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 MIPRE.LIDT.Co.SelfImprovement.addInU_filtered_sandwiched_tensor_sum_le_one {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (u v : MIPStarRE.LDT.Point params) (a : MIPStarRE.LDT.Fq params) : ∑ h : MIPStarRE.LDT.Polynomial params with h.toFun v = a, strategy.state.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 MIPRE.LIDT.Co.SelfImprovement.addInUSelectedCSChainQ0 {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (M : IdxSubMeas (MIPStarRE.LDT.Point params) Outcome 𝔓) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (S : MIPStarRE.LDT.SelfImprovement.AddInUSelection params Outcome) : ℝ

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 MIPRE.LIDT.Co.SelfImprovement.addInUSelectedCSChainQ1 {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (M : IdxSubMeas (MIPStarRE.LDT.Point params) Outcome 𝔓) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (S : MIPStarRE.LDT.SelfImprovement.AddInUSelection params Outcome) : ℝ

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 MIPRE.LIDT.Co.SelfImprovement.addInUSelectedCSChainQ2 {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (M : IdxSubMeas (MIPStarRE.LDT.Point params) Outcome 𝔓) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (S : MIPStarRE.LDT.SelfImprovement.AddInUSelection params Outcome) : ℝ

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 MIPRE.LIDT.Co.SelfImprovement.addInUSelectedCSChainQ3 {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (M : IdxSubMeas (MIPStarRE.LDT.Point params) Outcome 𝔓) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (S : MIPStarRE.LDT.SelfImprovement.AddInUSelection params Outcome) : ℝ

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 MIPRE.LIDT.Co.SelfImprovement.addInUSelectedCSChainQ4 {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (M : IdxSubMeas (MIPStarRE.LDT.Point params) Outcome 𝔓) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (S : MIPStarRE.LDT.SelfImprovement.AddInUSelection params Outcome) : ℝ

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 MIPRE.LIDT.Co.SelfImprovement.addInUSelectedCSChainQ0_eq_leftQuantity_averagedSandwiched {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (M : IdxSubMeas (MIPStarRE.LDT.Point params) Outcome 𝔓) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (S : MIPStarRE.LDT.SelfImprovement.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 MIPRE.LIDT.Co.SelfImprovement.addInUSelectedCSChainQ4_eq_rightQuantity {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (M : IdxSubMeas (MIPStarRE.LDT.Point params) Outcome 𝔓) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (S : MIPStarRE.LDT.SelfImprovement.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 MIPRE.LIDT.Co.SelfImprovement.addInUCSChainQ0 {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) : ℝ

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 MIPRE.LIDT.Co.SelfImprovement.addInUCSChainQ1 {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) : ℝ

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 MIPRE.LIDT.Co.SelfImprovement.addInUCSChainQ2 {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) : ℝ

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 MIPRE.LIDT.Co.SelfImprovement.addInUCSChainQ3 {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) : ℝ

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 MIPRE.LIDT.Co.SelfImprovement.addInUCSChainQ4 {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) : ℝ

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 MIPRE.LIDT.Co.SelfImprovement.add_in_u_cs_chain_q0_eq_match_mass {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) : strategy.state.qBipartiteMatchMass (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 MIPRE.LIDT.Co.SelfImprovement.add_in_u_cs_chain_q4_eq_simplified_rhs {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) : addInUCSChainQ4 params strategy T = MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) fun (u : MIPStarRE.LDT.Point params) => ∑ h : MIPStarRE.LDT.Polynomial params, strategy.state.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.