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

Internal helper module; part of the file-split for #1127.

References

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

theorem MIPStarRE.LDT.Pasting.ldSandwichLineOnePoint_prefix_cauchySchwarz_transport {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (gamma zeta : Error) {k i : ℕ} (hi : i < k) (hi0 : i ≠ 0) (facts : LdSandwichLineOnePointAdjointRawCoreBound params strategy family gamma zeta hi) : bipartiteConsError strategy.state (uniformDistribution (SandwichedLineQuestion params k)) (ldSandwichLineOnePointPrefixOriginalFamily params family hi) (ldSandwichLineOnePointRightFamily params strategy family k i) ≤ bipartiteConsError strategy.state (uniformDistribution (SandwichedLineQuestion params k)) (ldSandwichLineOnePointPrefixMovedFamily params family hi) (ldSandwichLineOnePointRightFamily params strategy family k i) + 2 * √(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 MIPStarRE.LDT.Pasting.ldSandwichLineOnePoint_matchMass_lower_bound {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma zeta : Error) (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 : ConsRel strategy.state (uniformDistribution (SandwichedLineQuestion params k)) (ldSandwichLineOnePointPrefixMovedFamily params family hi) (ldSandwichLineOnePointRightFamily params strategy family k i) (zeta + √(8 * ↑params.m * min eps 1 + 4 * min delta 1))) : bipartiteConsError strategy.state (uniformDistribution (SandwichedLineQuestion params k)) (ldSandwichLineOnePointPrefixOriginalFamily params family hi) (ldSandwichLineOnePointRightFamily params strategy family k i) ≤ 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 now proved directly in the local lemmas that use them.

theorem MIPStarRE.LDT.Pasting.ldSandwichLineOnePoint_nonzero_prefix_transport {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma zeta : Error) (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 : ConsRel strategy.state (uniformDistribution (SandwichedLineQuestion params k)) (ldSandwichLineOnePointPrefixMovedFamily params family hi) (ldSandwichLineOnePointRightFamily params strategy family k i) (zeta + √(8 * ↑params.m * min eps 1 + 4 * min delta 1))) : ConsRel strategy.state (uniformDistribution (SandwichedLineQuestion params k)) (ldSandwichLineOnePointLeftFamily params strategy family k i) (ldSandwichLineOnePointRightFamily params strategy family k i) (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 MIPStarRE.LDT.Pasting.ldSandwichLineOnePoint_core_of_axis_self {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma zeta : Error) (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) : ConsRel strategy.state (uniformDistribution (SandwichedLineQuestion params k)) (ldSandwichLineOnePointLeftFamily params strategy family k i) (ldSandwichLineOnePointRightFamily params strategy family k i) (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 MIPStarRE.LDT.Pasting.ldSandwichLineOnePoint_ofGHatFacts_of_axis_self {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma zeta : Error) (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 MIPStarRE.LDT.Pasting.ldSandwichLineOnePoint_ofGHatFacts {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma zeta : Error) (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 MIPStarRE.LDT.Pasting.ldSandwichLineOnePoint {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma zeta : Error) (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.