Section 12 pasting: over all outcomes — error terms and eligible mass

Error-arithmetic lemmas, eligible-mass bounds, and mass identities that feed the final lem:over-all-outcomes comparison.

References

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

theorem MIPStarRE.LDT.Pasting.eligibleMass_le_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) {k : ℕ} (xs : PointTuple params k) : subMeasMass strategy.state (interpolationEligibleSandwichFamily params family k xs).liftLeft ≤ 1

Eligible interpolation mass is at most one for every point tuple.

theorem MIPStarRE.LDT.Pasting.avgOver_uniform_eligibleMass_le_distinct_add_dnoteq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (k : ℕ) : (avgOver (uniformDistribution (PointTuple params k)) fun (xs : PointTuple params k) => subMeasMass strategy.state (interpolationEligibleSandwichFamily params family k xs).liftLeft) ≤ (avgOver (distinctTupleDistribution params k) fun (xs : PointTuple params k) => subMeasMass strategy.state (interpolationEligibleSandwichFamily params family k xs).liftLeft) + ↑k ^ 2 / ↑params.q

Uniform tuple averaging is bounded by distinct averaging plus ldDnoteq.

theorem MIPStarRE.LDT.Pasting.overAllOutcomesPastedMass_eq_avg_distinct_global {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (k : ℕ) : overAllOutcomesPastedMass params strategy family k = avgOver (distinctTupleDistribution params k) fun (xs : PointTuple params k) => subMeasMass strategy.state (restrictSubMeas (interpolationEligibleSandwichFamily params family k xs) (IsGloballyConsistent params xs)).liftLeft

The pasted mass is the distinct average of globally consistent eligible mass.

theorem MIPStarRE.LDT.Pasting.overAllOutcomesExpansionMass_eq_avg_uniform_eligible {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (k : ℕ) : overAllOutcomesExpansionMass params strategy family k = avgOver (uniformDistribution (PointTuple params k)) fun (xs : PointTuple params k) => subMeasMass strategy.state (interpolationEligibleSandwichFamily params family k xs).liftLeft

The expansion mass is the uniform average of eligible interpolation mass.

theorem MIPStarRE.LDT.Pasting.overAllOutcomes_reverse_mass_bound_of_not_d_add_one_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (eps delta gamma zeta : Error) (k : ℕ) (hnot : ¬params.d + 1 ≤ k) (heps_nonneg : 0 ≤ eps) (hdelta_nonneg : 0 ≤ delta) (hgamma_nonneg : 0 ≤ gamma) (hzeta_nonneg : 0 ≤ zeta) : overAllOutcomesExpansionMass params strategy family k - overAllOutcomesPastedMass params strategy family k ≤ overAllOutcomesError params eps delta gamma zeta k

If there are not enough coordinates to interpolate, both sides of the reverse mass comparison are zero.

theorem MIPStarRE.LDT.Pasting.overAllOutcomes_pasted_sub_expansion_le_dnoteq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (k : ℕ) : overAllOutcomesPastedMass params strategy family k - overAllOutcomesExpansionMass params strategy family k ≤ ↑k ^ 2 / ↑params.q

The pasted-minus-expansion mass loss is bounded by the distinctness error.

theorem MIPStarRE.LDT.Pasting.dnoteq_term_le_overAllOutcomesError (params : Parameters) [FieldModel params.q] (eps delta gamma zeta : Error) (k : ℕ) (hd : 0 < params.d) (heps_nonneg : 0 ≤ eps) (hdelta_nonneg : 0 ≤ delta) (hgamma_nonneg : 0 ≤ gamma) (hzeta_nonneg : 0 ≤ zeta) : ↑k ^ 2 / ↑params.q ≤ overAllOutcomesError params eps delta gamma zeta k

The distinctness loss is already absorbed by the displayed lem:over-all-outcomes error term.

theorem MIPStarRE.LDT.Pasting.hBConsistencyError_add_mdq_add_dnoteq_le_overAllOutcomesError (params : Parameters) [FieldModel params.q] (eps delta gamma zeta : Error) (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) : hBConsistencyError params eps delta gamma zeta k + ↑(params.m * params.d) / ↑params.q + ↑k ^ 2 / ↑params.q ≤ overAllOutcomesError params eps delta gamma zeta k

The paper's md/q Schwartz–Zippel term and the final distinctness swap fit inside the two-coefficient slack between ν₆ and ν₇.

This is the arithmetic at ld-pasting.tex lines 1280--1286, isolated from the operator/probability part of the reverse mass comparison.

theorem MIPStarRE.LDT.Pasting.tupleInterpolatedVerticalLine_eq_of_no_supported_mismatch (params : Parameters) [FieldModel params.q] {k : ℕ} (u : Point params) (xs : PointTuple params k) (hxs : Function.Injective xs) (gs : GHatTupleOutcome params k) (hEligible : InterpolationEligible params gs) (f : AxisLinePolynomial params.next) (hNoMismatch : ¬∃ (i : Fin k) (hiSome : Option.isSome (gs i) = true), (Option.get (gs i) hiSome).toFun u ≠ f.toFun (xs i)) : tupleInterpolatedVerticalLine params u xs gs = f

A line answer matching every supported completed slice agrees with the vertical line induced by the interpolant chosen from the interpolation support.

This is the uniqueness step in ld-pasting.tex lines 1245--1255: once the d+1 support slices determine h*, any degree-d vertical-line answer matching all supported slices at u must be the restriction of h* to that line.