Section 12 pasting: H-B consistency

The aggregation theorem proving lem:h-b-consistency from the one-point line consistency statements: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/ComparisonLemmas/HBConsistency.lean in the port of planning/c6b-plan.md (milestone M11, section "Port conventions").

A strategy is a SymStrat params.next 𝔓 K and the slice family an IdxPolyFamily params 𝔓; the consistency statement is a ConsRel on strategy.state. The fixed-u defect, its comparison with the bad mass and the aggregation of the one-point line estimates are the lemmas of Co/.../LineInterpolation/HBError.lean; the nonnegativity of ε, δ and ζ is read off the hypotheses through S.bipartiteConsError_nonneg and S.bipartiteSSCError_nonneg, and that of γ, in hBConsistency_ofLinePointBounds, through gamma_nonneg_of_isGood. No statement carries a swap or normalization hypothesis, the vendored statements having none.

Not ported

Nothing: every vendored declaration has a counterpart of the same name.

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.hBConsistency_core_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) (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 : ℕ) (hline : ∀ i < k, LdSandwichLineOnePointStatement params strategy family eps delta gamma zeta k i) : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.VerticalLineQuestion params)) (hRestrictionToVerticalLine params (constructedPastedSubMeas params family k)) (verticalLineMeasurementFamily params strategy) (MIPStarRE.LDT.Pasting.hBConsistencyError params eps delta gamma zeta k)

Aggregate one-point consistency bounds over all slice indices, plus the distinct-tuple approximation error.

Paper reference: lem:h-b-consistency proof in ld-pasting.tex lines 1050–1091.

Steps:

1. Expand using degree constraints to find eligible index i
2. Switch from independent to distinct samples (prop:ld-dnoteq, cost k²/q)
3. Union bound over k indices, each contributing ν₅
4. Total: k·ν₅ + k²/q ≤ 44k²m(...)

theorem MIPRE.LIDT.Co.Pasting.hBConsistency_ofLinePointBounds_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) (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 : ℕ) (hline : ∀ i < k, LdSandwichLineOnePointStatement params strategy family eps delta gamma zeta k i) : HBConsistencyStatement params strategy family eps delta gamma zeta k

Internal form of lem:h-b-consistency after applying lem:ld-sandwich-line-one-point at each coordinate.

Source: The proof in references/ldt-paper/ld-pasting.tex:1075-1109 uses the one-point line estimates and then performs the averaging and distinct-tuple comparison. The paper-facing theorem hBConsistency below derives the one-point estimates from the source hypotheses.

theorem MIPRE.LIDT.Co.Pasting.hBConsistency_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 : ℝ) (hgood : strategy.IsGood eps delta gamma) (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 : ℕ) (hline : ∀ i < k, LdSandwichLineOnePointStatement params strategy family eps delta gamma zeta k i) : HBConsistencyStatement params strategy family eps delta gamma zeta k

lem:h-b-consistency for a good strategy, from the one-point line estimates.

theorem MIPRE.LIDT.Co.Pasting.hBConsistency {𝔓 : 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 : ℕ) : HBConsistencyStatement params strategy family eps delta gamma zeta k

lem:h-b-consistency, source-facing form.