Section 12 pasting: line one-point transport — core theorems

The assembly of lem:ld-sandwich-line-one-point: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/ComparisonLemmas/LdSandwichLineOnePoint/Core.lean in the port of planning/c6b-plan.md (milestone M11, section "Port conventions").

A strategy is a SymStrat params.next 𝔓 K and the slice family an IdxPolyFamily params 𝔓; the consistency statements are ConsRels on strategy.state. The linear-defect bound of Co/.../LdSandwichLineOnePoint/CauchySchwarz.lean reinstates the max 0 of the bipartite consistency error (ldSandwichLineOnePoint_prefix_cauchySchwarz_transport), the moved endpoint of PrefixMoved.lean closes the nonzero-coordinate branch, and the endpoint of Endpoint.lean the zero-coordinate branch. The vendored proofs bound the two failure probabilities by 1 through strategy.isNormalized; here S.bipartiteConsError_uniform_le_one and Pasting.bipartiteSSCError_uniform_le_one take no normalization argument. No statement carries a swap or normalization hypothesis, the vendored statements having none.

Not ported

Nothing: every vendored declaration has a counterpart of the same name.

References

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

• references/ldt-paper/ld-pasting.tex
• blueprint/src/chapter/ch09_pasting.tex

theorem MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePoint_prefix_cauchySchwarz_transport {𝔓 : 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.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (gamma zeta : ℝ) {k i : ℕ} (hi : i < k) (hi0 : i ≠ 0) (facts : LdSandwichLineOnePointAdjointRawCoreBound params strategy family gamma zeta hi) : strategy.state.bipartiteConsError (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k)) (ldSandwichLineOnePointPrefixOriginalFamily params family hi) (ldSandwichLineOnePointRightFamily params strategy family k i) ≤ strategy.state.bipartiteConsError (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k)) (ldSandwichLineOnePointPrefixMovedFamily params family hi) (ldSandwichLineOnePointRightFamily params strategy family k i) + 2 * √(MIPStarRE.LDT.Pasting.commuteGHalfSandwichError params gamma zeta (i + 1))

The post-deletion analytic transport in lem:ld-sandwich-line-one-point.

The substantive paper gap is now the averaged linear defect bound ldSandwichLineOnePoint_prefix_linearDefect_average_cauchySchwarz_bound; this lemma is only the proved reduction that reinstates the max 0 bipartite consistency error using the measurement-valued right family.

theorem MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePoint_matchMass_lower_bound {𝔓 : 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.next 𝔓 K) (eps delta gamma zeta : ℝ) (heps_nonneg : 0 ≤ eps) (hdelta_nonneg : 0 ≤ delta) (hgamma_nonneg : 0 ≤ gamma) (hzeta_nonneg : 0 ≤ zeta) (hzeta_le : zeta ≤ 1) (family : IdxPolyFamily params 𝔓) {k i : ℕ} (hi : i < k) (hi0 : i ≠ 0) (facts : LdSandwichLineOnePointAdjointRawCoreBound params strategy family gamma zeta hi) (hmovedEndpoint : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k)) (ldSandwichLineOnePointPrefixMovedFamily params family hi) (ldSandwichLineOnePointRightFamily params strategy family k i) (zeta + √(8 * ↑params.m * min eps 1 + 4 * min delta 1))) : strategy.state.bipartiteConsError (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k)) (ldSandwichLineOnePointPrefixOriginalFamily params family hi) (ldSandwichLineOnePointRightFamily params strategy family k i) ≤ MIPStarRE.LDT.Pasting.ldSandwichLineOnePointError params eps delta gamma zeta k

Scalar residual for the nonzero-coordinate branch of lem:ld-sandwich-line-one-point.

This is the match-mass lower-bound step after unfolding ConsRel: it bounds the averaged off-diagonal defect for the prefix-marginalized one-point family. The helper consumes only the adjoint raw-core bound; endpoint identifications, raw-family reindexing, exact tail deletion, and match-mass expansion are proved directly in the local lemmas that use them.

theorem MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePoint_nonzero_prefix_transport {𝔓 : 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.next 𝔓 K) (eps delta gamma zeta : ℝ) (heps_nonneg : 0 ≤ eps) (hdelta_nonneg : 0 ≤ delta) (hgamma_nonneg : 0 ≤ gamma) (hzeta_nonneg : 0 ≤ zeta) (hzeta_le : zeta ≤ 1) (family : IdxPolyFamily params 𝔓) {k i : ℕ} (hi : i < k) (hi0 : i ≠ 0) (hcomm : ∀ (j : ℕ), 2 ≤ j → CommuteGHalfSandwichStatement params strategy.state family gamma zeta j) (hmovedEndpoint : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k)) (ldSandwichLineOnePointPrefixMovedFamily params family hi) (ldSandwichLineOnePointRightFamily params strategy family k i) (zeta + √(8 * ↑params.m * min eps 1 + 4 * min delta 1))) : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k)) (ldSandwichLineOnePointLeftFamily params strategy family k i) (ldSandwichLineOnePointRightFamily params strategy family k i) (MIPStarRE.LDT.Pasting.ldSandwichLineOnePointError params eps delta gamma zeta k)

Turn the scalar match-mass lower bound into the ConsRel needed by the public line-one-point statement.

theorem MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePoint_core_of_axis_self {𝔓 : 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.next 𝔓 K) (eps delta gamma zeta : ℝ) (haxis : strategy.axisParallelFailureProbability ≤ eps) (hself : strategy.selfConsistencyFailureProbability ≤ delta) (hgamma_nonneg : 0 ≤ gamma) (hzeta_le : zeta ≤ 1) (family : IdxPolyFamily params 𝔓) (hcons : family.ConsistentWithPoints strategy zeta) (hcomm : ∀ (j : ℕ), 2 ≤ j → CommuteGHalfSandwichStatement params strategy.state family gamma zeta j) (k i : ℕ) (hi : i < k) : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k)) (ldSandwichLineOnePointLeftFamily params strategy family k i) (ldSandwichLineOnePointRightFamily params strategy family k i) (MIPStarRE.LDT.Pasting.ldSandwichLineOnePointError params eps delta gamma zeta k)

Cauchy-Schwarz sandwich elimination for one-point consistency.

Given the half-sandwich commutation bound from commuteGHalfSandwich, performs the Cauchy-Schwarz + measurement-completeness argument that converts the sandwiched operator distance into a one-point consistency bound.

Paper reference: lem:ld-sandwich-line-one-point proof in ld-pasting.tex lines 931-1036.

Steps:

1. Simplify by summing out indices > i using measurement completeness
2. Apply Cauchy-Schwarz with commuteGHalfSandwich to move Ghat_1 left
3. Apply Cauchy-Schwarz again to move Ghat_1 right
4. Eliminate Ghat_<i product using measurement completeness
5. Reduce to the single-slice bound eq:ld-gbcon

theorem MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePoint_ofGHatFacts_of_axis_self {𝔓 : 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.next 𝔓 K) (eps delta gamma zeta : ℝ) (haxis : strategy.axisParallelFailureProbability ≤ eps) (hself_good : strategy.selfConsistencyFailureProbability ≤ delta) (hgamma_nonneg : 0 ≤ gamma) (hzeta_le : zeta ≤ 1) (family : IdxPolyFamily params 𝔓) (hcons : family.ConsistentWithPoints strategy zeta) (hfacts : GHatFactsStatement params strategy.state family gamma zeta) (k i : ℕ) (hi : i < k) : LdSandwichLineOnePointStatement params strategy family eps delta gamma zeta k i

Internal form of lem:ld-sandwich-line-one-point after applying cor:G-hat-facts.

Source: The proof in references/ldt-paper/ld-pasting.tex:956-1074 uses the half-sandwich commutation estimates obtained from cor:G-hat-facts. The paper-facing theorem ldSandwichLineOnePoint below derives those estimates from the source hypotheses.

theorem MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePoint_ofGHatFacts {𝔓 : 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.next 𝔓 K) (eps delta gamma zeta : ℝ) (hgood : strategy.IsGood eps delta gamma) (_hgamma_le : gamma ≤ 1) (hzeta_le : zeta ≤ 1) (_hdq_le : params.d ≤ params.q) (family : IdxPolyFamily params 𝔓) (hcons : family.ConsistentWithPoints strategy zeta) (_hself : family.StronglySelfConsistent strategy.state zeta) (_hbound : IdxPolyFamily.SliceBoundednessInput strategy family zeta) (hfacts : GHatFactsStatement params strategy.state family gamma zeta) (k i : ℕ) (hi : i < k) : LdSandwichLineOnePointStatement params strategy family eps delta gamma zeta k i

Internal form of lem:ld-sandwich-line-one-point after applying cor:G-hat-facts.

This source-facing statement retains the usual good-strategy hypothesis.

theorem MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePoint {𝔓 : 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.next 𝔓 K) (eps delta gamma zeta : ℝ) (hgood : strategy.IsGood eps delta gamma) (hgamma_le : gamma ≤ 1) (hzeta_le : zeta ≤ 1) (hdq_le : params.d ≤ params.q) (family : IdxPolyFamily params 𝔓) (hcons : family.ConsistentWithPoints strategy zeta) (hself : family.StronglySelfConsistent strategy.state zeta) (hbound : IdxPolyFamily.SliceBoundednessInput strategy family zeta) (k i : ℕ) (hi : i < k) : LdSandwichLineOnePointStatement params strategy family eps delta gamma zeta k i

lem:ld-sandwich-line-one-point, source-facing form.