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

Eligible-mass bounds and mass identities that feed the final lem:over-all-outcomes comparison: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/ComparisonLemmas/OverAllOutcomes/ErrorAndMass.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 𝔓; the masses are strategy.state.subMeasMass of left-placed submeasurements, (A.liftLeft strategy.state). The bound of an eligible mass by 1 (vendored through strategy.isNormalized) uses S.ev_one_of_isNormalized, which takes no hypothesis. The two mass identities are S.ev_leftTensor_averageOperatorOverDistribution up to definitional unfolding, and the vanishing masses below d + 1 coordinates and the monotonicity of the restricted mass are S.ev_zero and S.leftTensor_mono, where the vendored proofs unfold leftTensor and ev.

The error arithmetic (oneThirtySecondErrorSum_nonneg and the two comparisons with overAllOutcomesError) and the interpolation-uniqueness step are classical: this file imports the vendored file and names them through an explicit open MIPStarRE.LDT.Pasting (…) list.

Not ported

• dnoteq_term_le_overAllOutcomesError: classical, imported.
• hBConsistencyError_add_mdq_add_dnoteq_le_overAllOutcomesError: classical, imported.
• tupleInterpolatedVerticalLine_eq_of_no_supported_mismatch: classical, imported.

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.oneThirtySecondErrorSum_nonneg (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (eps delta gamma zeta : ℝ) (heps_nonneg : 0 ≤ eps) (hdelta_nonneg : 0 ≤ delta) (hgamma_nonneg : 0 ≤ gamma) (hzeta_nonneg : 0 ≤ zeta) : 0 ≤ eps.rpow (1 / 32) + delta.rpow (1 / 32) + gamma.rpow (1 / 32) + zeta.rpow (1 / 32) + (↑params.d / ↑params.q).rpow (1 / 32)

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

The common nonnegative error-sum with exponent 1/32 used by the Section 12 displayed error terms.

theorem MIPRE.LIDT.Co.Pasting.interpolationEligibleSandwich_total_eq_zero_of_not_d_add_one_le {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) {k : ℕ} (hnot : ¬params.d + 1 ≤ k) (xs : MIPStarRE.LDT.PointTuple params k) : (interpolationEligibleSandwichFamily params family k xs).total = 0

If k < d+1, the interpolation-eligible sandwich total vanishes.

theorem MIPRE.LIDT.Co.Pasting.eligibleMass_nonneg {𝔓 : 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) : 0 ≤ strategy.state.subMeasMass (SubMeas.liftLeft strategy.state (interpolationEligibleSandwichFamily params family k xs))

Eligible interpolation mass is nonnegative for every point tuple.

theorem MIPRE.LIDT.Co.Pasting.eligibleMass_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.next 𝔓 K) (family : IdxPolyFamily params 𝔓) {k : ℕ} (xs : MIPStarRE.LDT.PointTuple params k) : strategy.state.subMeasMass (SubMeas.liftLeft strategy.state (interpolationEligibleSandwichFamily params family k xs)) ≤ 1

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

theorem MIPRE.LIDT.Co.Pasting.avgOver_distinct_eligibleMass_le_uniform_add_dnoteq {𝔓 : 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 : ℕ) : (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.Pasting.distinctTupleDistribution params k) fun (xs : MIPStarRE.LDT.PointTuple params k) => strategy.state.subMeasMass (SubMeas.liftLeft strategy.state (interpolationEligibleSandwichFamily params family k xs))) ≤ (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.PointTuple params k)) fun (xs : MIPStarRE.LDT.PointTuple params k) => strategy.state.subMeasMass (SubMeas.liftLeft strategy.state (interpolationEligibleSandwichFamily params family k xs))) + ↑k ^ 2 / ↑params.q

Distinct tuple averaging is bounded by uniform averaging plus ldDnoteq.

theorem MIPRE.LIDT.Co.Pasting.avgOver_uniform_eligibleMass_le_distinct_add_dnoteq {𝔓 : 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 : ℕ) : (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.PointTuple params k)) fun (xs : MIPStarRE.LDT.PointTuple params k) => strategy.state.subMeasMass (SubMeas.liftLeft strategy.state (interpolationEligibleSandwichFamily params family k xs))) ≤ (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.Pasting.distinctTupleDistribution params k) fun (xs : MIPStarRE.LDT.PointTuple params k) => strategy.state.subMeasMass (SubMeas.liftLeft strategy.state (interpolationEligibleSandwichFamily params family k xs))) + ↑k ^ 2 / ↑params.q

Uniform tuple averaging is bounded by distinct averaging plus ldDnoteq.

theorem MIPRE.LIDT.Co.Pasting.overAllOutcomesPastedMass_eq_avg_distinct_global {𝔓 : 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 : ℕ) : overAllOutcomesPastedMass params strategy family k = MIPStarRE.LDT.avgOver (MIPStarRE.LDT.Pasting.distinctTupleDistribution params k) fun (xs : MIPStarRE.LDT.PointTuple params k) => strategy.state.subMeasMass (SubMeas.liftLeft strategy.state (restrictSubMeas (interpolationEligibleSandwichFamily params family k xs) (MIPStarRE.LDT.Pasting.IsGloballyConsistent params xs)))

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

theorem MIPRE.LIDT.Co.Pasting.overAllOutcomesExpansionMass_eq_avg_uniform_eligible {𝔓 : 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 : ℕ) : overAllOutcomesExpansionMass params strategy family k = MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.PointTuple params k)) fun (xs : MIPStarRE.LDT.PointTuple params k) => strategy.state.subMeasMass (SubMeas.liftLeft strategy.state (interpolationEligibleSandwichFamily params family k xs))

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

theorem MIPRE.LIDT.Co.Pasting.overAllOutcomes_reverse_mass_bound_of_not_d_add_one_le {𝔓 : 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 : ℕ) (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 ≤ MIPStarRE.LDT.Pasting.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 MIPRE.LIDT.Co.Pasting.overAllOutcomes_pasted_sub_expansion_le_dnoteq {𝔓 : 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 : ℕ) : 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.