Line interpolation: H-B consistency error aggregation

Fixed-u defect, hBConsistencyError, degree-ratio error bounds, and the final bad-mass aggregation lemma that drives lem:h-b-consistency.

References

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

theorem MIPStarRE.LDT.Pasting.hBConsistency_fixed_u_defect_le_avgOver_distinct {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (k : ℕ) (u : Point params) : qBipartiteConsDefect strategy.state (hRestrictionToVerticalLine params (constructedPastedSubMeas params family k) u) (verticalLineMeasurementFamily params strategy u) ≤ avgOver (distinctTupleDistribution params k) fun (xs : PointTuple params k) => qBipartiteConsDefect strategy.state (hRestrictionToVerticalLine params (pastedInterpolationFamily params family k xs) u) (verticalLineMeasurementFamily params strategy u)

theorem MIPStarRE.LDT.Pasting.hBConsistencyError_eq_k_mul_ldSandwichLineOnePointError_add (params : Parameters) (eps delta gamma zeta : Error) (k : ℕ) : hBConsistencyError params eps delta gamma zeta k = ↑k * ldSandwichLineOnePointError params eps delta gamma zeta k + ↑k ^ 2 * ↑params.m * (Real.rpow eps (1 / 32) + Real.rpow delta (1 / 32) + Real.rpow gamma (1 / 32) + Real.rpow zeta (1 / 32) + Real.rpow (↑params.d / ↑params.q) (1 / 32))

theorem MIPStarRE.LDT.Pasting.avgOver_sum_fin {α : Type u_2} (𝒟 : Distribution α) (k : ℕ) (f : α → Fin k → Error) : (avgOver 𝒟 fun (a : α) => ∑ i : Fin k, f a i) = ∑ i : Fin k, avgOver 𝒟 fun (a : α) => f a i

theorem MIPStarRE.LDT.Pasting.one_div_q_le_rpow_degreeRatio (params : Parameters) [FieldModel params.q] (hd : 0 < params.d) : 1 / ↑params.q ≤ Real.rpow (↑params.d / ↑params.q) (1 / 32)

theorem MIPStarRE.LDT.Pasting.dnoteq_term_le_hBConsistency_extra (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 ≤ ↑k ^ 2 * ↑params.m * (Real.rpow eps (1 / 32) + Real.rpow delta (1 / 32) + Real.rpow gamma (1 / 32) + Real.rpow zeta (1 / 32) + Real.rpow (↑params.d / ↑params.q) (1 / 32))

theorem MIPStarRE.LDT.Pasting.hBConsistency_error_bound (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 * ldSandwichLineOnePointError params eps delta gamma zeta k + ↑k ^ 2 / ↑params.q ≤ hBConsistencyError params eps delta gamma zeta k

theorem MIPStarRE.LDT.Pasting.avgOver_distinct_pasted_defect_le_badMass {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) {k : ℕ} (u : Point params) : (avgOver (distinctTupleDistribution params k) fun (xs : PointTuple params k) => qBipartiteConsDefect strategy.state (hRestrictionToVerticalLine params (pastedInterpolationFamily params family k xs) u) (verticalLineMeasurementFamily params strategy u)) ≤ avgOver (distinctTupleDistribution params k) fun (xs : PointTuple params k) => hBConsistencyBadMass params strategy family u xs

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

theorem MIPStarRE.LDT.Pasting.avgOver_uniform_badMass_le_k_mul_ldSandwichLineOnePointError_ofLinePointBounds {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (eps delta gamma zeta : Error) (k : ℕ) (hline : ∀ i < k, LdSandwichLineOnePointStatement params strategy family eps delta gamma zeta k i) : (avgOver (uniformDistribution (Point params)) fun (u : Point params) => avgOver (uniformDistribution (PointTuple params k)) fun (xs : PointTuple params k) => hBConsistencyBadMass params strategy family u xs) ≤ ↑k * ldSandwichLineOnePointError params eps delta gamma zeta k

Internal aggregation form after the one-point line estimates have been supplied.

Source: In references/ldt-paper/ld-pasting.tex:1075-1109, the proof of lem:h-b-consistency applies lem:ld-sandwich-line-one-point for each coordinate and then sums the resulting bounds. The paper-facing theorem below derives these one-point estimates from the source hypotheses.

theorem MIPStarRE.LDT.Pasting.avgOver_uniform_badMass_le_k_mul_ldSandwichLineOnePointError {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (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) (hcons : family.ConsistentWithPoints strategy zeta) (hself : family.StronglySelfConsistent strategy.state zeta) (hbound : IdxPolyFamily.SliceBoundednessInput strategy family zeta) (k : ℕ) : (avgOver (uniformDistribution (Point params)) fun (u : Point params) => avgOver (uniformDistribution (PointTuple params k)) fun (xs : PointTuple params k) => hBConsistencyBadMass params strategy family u xs) ≤ ↑k * ldSandwichLineOnePointError params eps delta gamma zeta k

The independent-tuple bad mass is bounded by the sum of the one-point line errors, in the source-facing Section 12 context.

theorem MIPStarRE.LDT.Pasting.avgOver_distinct_badMass_le_hBConsistencyError_ofLinePointBounds {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (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) (hline : ∀ i < k, LdSandwichLineOnePointStatement params strategy family eps delta gamma zeta k i) : (avgOver (uniformDistribution (Point params)) fun (u : Point params) => avgOver (distinctTupleDistribution params k) fun (xs : PointTuple params k) => hBConsistencyBadMass params strategy family u xs) ≤ hBConsistencyError params eps delta gamma zeta k

Aggregate the one-point line comparison statements over all inserted vertical lines and absorb the distinct-tuple loss into the displayed hBConsistency error.

This is the reusable bad-mass aggregation from ld-pasting.tex lines 1186--1202 (also used in the proof of lem:h-b-consistency).

theorem MIPStarRE.LDT.Pasting.avgOver_distinct_badMass_le_hBConsistencyError {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (eps delta gamma zeta : Error) (k : ℕ) (hd : 0 < params.d) (hgood : strategy.IsGood eps delta gamma) (hgamma_le : gamma ≤ 1) (hzeta_le : zeta ≤ 1) (hdq_le : params.d ≤ params.q) (hcons : family.ConsistentWithPoints strategy zeta) (hself : family.StronglySelfConsistent strategy.state zeta) (hbound : IdxPolyFamily.SliceBoundednessInput strategy family zeta) : (avgOver (uniformDistribution (Point params)) fun (u : Point params) => avgOver (distinctTupleDistribution params k) fun (xs : PointTuple params k) => hBConsistencyBadMass params strategy family u xs) ≤ hBConsistencyError params eps delta gamma zeta k

Aggregate the one-point line comparison estimates and absorb the distinct-tuple loss into the displayed hBConsistency error, deriving the one-point estimates internally from lem:ld-sandwich-line-one-point.