Section 12 pasting: over all outcomes — Schwartz–Zippel bounds and final assembly

Schwartz–Zippel aggregation, the line-consistent indicator bound, and the final chained assembly of lem:over-all-outcomes: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/ComparisonLemmas/OverAllOutcomes/Final.lean in the port of planning/c6b-plan.md (milestone M11, section "Port conventions").

A strategy is a SymStrat params.next 𝔓 K and a slice family an IdxPolyFamily params 𝔓. avgOver_subMeasMass_restrict_liftLeft_eq_sum_coeff, a lemma on a placement, takes the model S as an explicit first argument and a local A : SubMeas Outcome 𝔓; its proof is S.ev_leftTensor_total_eq_sum_outcome on the restricted submeasurement, where the vendored proof unfolds mkLeftPlacedSubMeas. The vanishing of ineligible outcomes is map_zero and S.ev_zero, where the vendored proof unfolds leftTensor and ev. No statement carries a swap or normalization hypothesis: heps_nonneg and hdelta_nonneg of overAllOutcomes_ofGHatFacts_of_axis_self come from strategy.state.bipartiteConsError_nonneg and strategy.state.bipartiteSSCError_nonneg.

The pointwise Schwartz–Zippel bound lineConsistentIndicator_probability_le_mdq is classical: this file imports the vendored file and names it, with the error arithmetic of ErrorAndMass, through an explicit open MIPStarRE.LDT.Pasting (…) list.

Not ported

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.lineConsistentIndicator_probability_le_mdq (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] {k : ℕ} (xs : MIPStarRE.LDT.PointTuple params k) (hxs : Function.Injective xs) (gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params k) (hEligible : MIPStarRE.LDT.Pasting.InterpolationEligible params gs) : (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) fun (u : MIPStarRE.LDT.Point params) => if ¬MIPStarRE.LDT.Pasting.IsGloballyConsistent params xs gs ∧ ∃ (f : MIPStarRE.LDT.AxisLinePolynomial params.next), ¬∃ (i : Fin k) (hiSome : Option.isSome (gs i) = true), (Option.get (gs i) hiSome).toFun u ≠ f.toFun (xs i) then 1 else 0) ≤ ↑(params.m * params.d) / ↑params.q

Upstream keeps this helper private since its Lean-module port (LionSR/MIPStarRE at 5fc363b); the port carries its own copy, with upstream's proof.

For a fixed distinct tuple and interpolation-eligible nonglobal outcome, the probability (over the vertical-line base point u) of the line-consistency indicator is bounded by the paper's md/q Schwartz--Zippel term.

This formalizes ld-pasting.tex lines 1256--1265: nonglobality gives a supported slice where gᵢ differs from the interpolant h*; line consistency forces agreement at the sampled u, and MIPStarRE.LDT.Preliminaries.polynomialAgreement_avg_le_mdq bounds that agreement probability.

theorem MIPRE.LIDT.Co.Pasting.avgOver_subMeasMass_restrict_liftLeft_eq_sum_coeff {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {Outcome : Type u_4} [Fintype Outcome] (S : SymModel 𝔓 K) (𝒟 : MIPStarRE.LDT.Distribution Question) (A : SubMeas Outcome 𝔓) (P : Question → Outcome → Prop) [(q : Question) → DecidablePred (P q)] : (MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => S.subMeasMass (SubMeas.liftLeft S (restrictSubMeas A (P q)))) = ∑ a : Outcome, (MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => if P q a then 1 else 0) * S.ev (S.L (A.outcome a))

Expand an averaged restricted lifted submeasurement into per-outcome masses weighted by the probability of the restricting predicate.

theorem MIPRE.LIDT.Co.Pasting.lineConsistentIndicatorLocal_avg_le_mdq {𝔓 : 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 𝔓) {k : ℕ} (xs : MIPStarRE.LDT.PointTuple params k) (hxs : Function.Injective xs) : (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) fun (u : MIPStarRE.LDT.Point params) => overAllOutcomesLineConsistentIndicatorLocal params strategy family u xs) ≤ ↑(params.m * params.d) / ↑params.q

Fixed-distinct-tuple form of the line-consistent Schwartz--Zippel bound.

theorem MIPRE.LIDT.Co.Pasting.overAllOutcomes_distinct_lineConsistent_indicator_mass_le_mdq {𝔓 : 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 𝔓) (k : ℕ) : overAllOutcomesDistinctLineConsistentIndicatorMass params strategy family k ≤ ↑(params.m * params.d) / ↑params.q

The line-consistent Schwartz--Zippel aggregation after the insertion and bad-line finite-sum split.

Paper anchor: ld-pasting.tex lines 1235--1275. For every distinct tuple xs, interpolation-eligible nonglobal outcome gs, and line-consistent answer f, the paper chooses the interpolant h*; nonglobality gives a supported coordinate where gᵢ ≠ h*|_{xsᵢ}, and Schwartz--Zippel bounds the probability over u that this disagreement vanishes by md/q.

theorem MIPRE.LIDT.Co.Pasting.overAllOutcomes_distinct_nonglobal_mass_le_bad_line_mass_add_mdq {𝔓 : 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 𝔓) (k : ℕ) : overAllOutcomesDistinctNonglobalMass params strategy family k ≤ overAllOutcomesDistinctBadLineMass params strategy family k + ↑(params.m * params.d) / ↑params.q

The local finite-sum/SZ comparison after the one-point line-mismatch aggregation has been separated off.

The insertion and finite-sum split from ld-pasting.tex lines 1174--1228 are proved by overAllOutcomes_distinct_nonglobal_mass_le_bad_line_mass_add_lineConsistent. The line-consistent remainder is exactly the Schwartz--Zippel aggregation proved by overAllOutcomes_distinct_lineConsistent_indicator_mass_le_mdq, corresponding to lines 1235--1275.

theorem MIPRE.LIDT.Co.Pasting.overAllOutcomes_reverse_mass_bound_of_nonglobal_mass_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) (family : IdxPolyFamily params 𝔓) (eps delta gamma zeta : ℝ) (k : ℕ) (hd : 0 < params.d) (hdq_le : params.d ≤ params.q) (hkEligible : params.d + 1 ≤ k) (heps_nonneg : 0 ≤ eps) (hdelta_nonneg : 0 ≤ delta) (hgamma_nonneg : 0 ≤ gamma) (hzeta_nonneg : 0 ≤ zeta) (hnonglobal : overAllOutcomesDistinctNonglobalMass params strategy family k ≤ MIPStarRE.LDT.Pasting.hBConsistencyError params eps delta gamma zeta k + ↑(params.m * params.d) / ↑params.q) : overAllOutcomesExpansionMass params strategy family k - overAllOutcomesPastedMass params strategy family k ≤ MIPStarRE.LDT.Pasting.overAllOutcomesError params eps delta gamma zeta k

If the distinct nonglobal mass is bounded by the paper's local k·ν₅ + k²/q + md/q comparison, then the reverse half of lem:over-all-outcomes follows.

The remaining hypothesis is exactly the content of ld-pasting.tex lines 1174--1275: insert the line measurement, pay the one-point line consistency bound to add the consistency indicator, and use Schwartz--Zippel for the indicator term.

theorem MIPRE.LIDT.Co.Pasting.overAllOutcomes_distinct_nonglobal_mass_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) (family : IdxPolyFamily params 𝔓) (eps delta gamma zeta : ℝ) (k : ℕ) (hd : 0 < params.d) (heps_nonneg : 0 ≤ eps) (hdelta_nonneg : 0 ≤ delta) (hgamma_nonneg : 0 ≤ gamma) (hzeta_nonneg : 0 ≤ zeta) (hline : ∀ i < k, LdSandwichLineOnePointStatement params strategy family eps delta gamma zeta k i) : overAllOutcomesDistinctNonglobalMass params strategy family k ≤ MIPStarRE.LDT.Pasting.hBConsistencyError params eps delta gamma zeta k + ↑(params.m * params.d) / ↑params.q

The paper-local nonglobal mass comparison after the algebraic reductions.

The one-point line-comparison aggregation from ld-pasting.tex lines 1186--1202 is proved by overAllOutcomes_distinct_bad_line_mass_le_hBConsistencyError, and the remaining insertion/Schwartz--Zippel estimate is overAllOutcomes_distinct_nonglobal_mass_le_bad_line_mass_add_mdq.

theorem MIPRE.LIDT.Co.Pasting.overAllOutcomes_of_reverse_mass_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) (family : IdxPolyFamily params 𝔓) (eps delta gamma zeta : ℝ) (k : ℕ) (hd : 0 < params.d) (heps_nonneg : 0 ≤ eps) (hdelta_nonneg : 0 ≤ delta) (hgamma_nonneg : 0 ≤ gamma) (hzeta_nonneg : 0 ≤ zeta) (hreverse : overAllOutcomesExpansionMass params strategy family k - overAllOutcomesPastedMass params strategy family k ≤ MIPStarRE.LDT.Pasting.overAllOutcomesError params eps delta gamma zeta k) : OverAllOutcomesStatement params strategy family eps delta gamma zeta k

Reduction of lem:over-all-outcomes to a reverse mass comparison.

The forward direction overAllOutcomesPastedMass - overAllOutcomesExpansionMass is now discharged by expanding the pasted mass over distinct tuples, forgetting global consistency, and paying only ldDnoteq. The reverse loss overAllOutcomesExpansionMass - overAllOutcomesPastedMass is the part of ld-pasting.tex supplied below by the completed ldSandwichLineOnePoint aggregation.

theorem MIPRE.LIDT.Co.Pasting.overAllOutcomes_ofLinePointBounds {𝔓 : 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) (hdq_le : params.d ≤ params.q) (hd : 0 < params.d) (family : IdxPolyFamily params 𝔓) (k : ℕ) (hline : ∀ i < k, LdSandwichLineOnePointStatement params strategy family eps delta gamma zeta k i) : OverAllOutcomesStatement params strategy family eps delta gamma zeta k

Internal form of lem:over-all-outcomes from the one-point sandwich estimates.

The proof of the mass comparison uses the estimates lem:ld-sandwich-line-one-point in the interpolation-eligible case. Once those estimates are supplied explicitly, the remaining argument only needs nonnegativity of the scalar error parameters and the usual degree and field-size side conditions.

theorem MIPRE.LIDT.Co.Pasting.overAllOutcomes_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_nonneg : 0 ≤ zeta) (hzeta_le : zeta ≤ 1) (hdq_le : params.d ≤ params.q) (hd : 0 < params.d) (family : IdxPolyFamily params 𝔓) (hcons : family.ConsistentWithPoints strategy zeta) (hfacts : GHatFactsStatement params strategy.state family gamma zeta) (k : ℕ) : OverAllOutcomesStatement params strategy family eps delta gamma zeta k

Internal form of lem:over-all-outcomes from cor:G-hat-facts.

theorem MIPRE.LIDT.Co.Pasting.overAllOutcomes_ofComMain_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) (hgamma_le : gamma ≤ 1) (hzeta_nonneg : 0 ≤ zeta) (hzeta_le : zeta ≤ 1) (hdq_le : params.d ≤ params.q) (hd : 0 < params.d) (family : IdxPolyFamily params 𝔓) (hcons : family.ConsistentWithPoints strategy zeta) (hself : family.StronglySelfConsistent strategy.state zeta) (hcom : Commutativity.ComMainConclusion params strategy family gamma zeta) (k : ℕ) : OverAllOutcomesStatement params strategy family eps delta gamma zeta k

Internal form of lem:over-all-outcomes from the Section 11 commutativity conclusion.

theorem MIPRE.LIDT.Co.Pasting.overAllOutcomes {𝔓 : 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) (hd : 0 < params.d) (family : IdxPolyFamily params 𝔓) (hcons : family.ConsistentWithPoints strategy zeta) (hself : family.StronglySelfConsistent strategy.state zeta) (hbound : IdxPolyFamily.SliceBoundednessInput strategy family zeta) (k : ℕ) : OverAllOutcomesStatement params strategy family eps delta gamma zeta k

lem:over-all-outcomes.