Section 12 pasting: H-A consistency

The vertical-line to point-consistency transport and the completed-measurement statement of cor:h-a-consistency: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/ComparisonLemmas/HAConsistency.lean in the port of planning/c6b-plan.md (milestone M11, section "Port conventions").

A strategy is a SymStrat params.next 𝔓 K, a slice family an IdxPolyFamily params 𝔓 and a candidate polynomial submeasurement H : SubMeas (Polynomial params.next) 𝔓; the consistency statements are ConsRels on strategy.state, and the completeness hypothesis is strategy.state.CompletenessAtLeast (H.liftLeft strategy.state) …. Three uses of the vendored strategy fields become theorems of the model:

• the bounds of the two failure probabilities by 1 (vendored through strategy.isNormalized) are S.bipartiteConsError_uniform_le_one and Pasting.bipartiteSSCError_uniform_le_one;
• the swap of the consistency relation (vendored through strategy.densityFixed) is S.consRel_symm_of_density_fixed, and the triangle step Preliminaries.triangleSub_right takes no normalization argument;
• the residual mass ev(R(1 − H.total)) = 1 − ev(L H.total) (vendored through strategy.permInvState.swap_ev, an entrywise Kronecker identity and ev_one_of_isNormalized) is S.ev_L_eq_ev_R, S.leftTensor_sub and S.ev_one_of_isNormalized. 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.hAConsistency_submeas_from_lineConsistency_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) (H : SubMeas (MIPStarRE.LDT.Polynomial params.next) 𝔓) (eps delta gamma zeta : ℝ) (haxis : strategy.axisParallelFailureProbability ≤ eps) (hself_good : strategy.selfConsistencyFailureProbability ≤ delta) (hgamma_nonneg : 0 ≤ gamma) (hzeta_nonneg : 0 ≤ zeta) (k : ℕ) (hk_pos : 1 ≤ k) (hline : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) (hRestrictionToVerticalLine params H) (verticalLineMeasurementFamily params strategy) (MIPStarRE.LDT.Pasting.hBConsistencyError params eps delta gamma zeta k)) : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params.next)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params.next H) (MIPStarRE.LDT.MainInductionStep.ldPastingInInductionNu params k eps delta gamma zeta)

Convert source-style vertical-line consistency to point consistency using only the axis-parallel and self-consistency estimates.

This is the main estimate in cor:h-a-consistency, stated without the intermediate HBConsistencyStatement type. It takes only the line-consistency estimate for a candidate polynomial submeasurement H, restricts that estimate to the point on each vertical line, and then applies the good-strategy point-to-vertical-line comparison. The diagonal-line estimate in strategy.IsGood is not used in this transport step; it enters earlier in the construction of the line-consistency estimate.

Paper reference: cor:h-a-consistency proof in ld-pasting.tex lines 1098–1117.

Steps:

1. Restrict the line-consistency hypothesis to a single point on the line
2. Apply triangleSub with the A-B consistency bound from hgood
3. Error bound: ν₆ + √(8mε + 4δ) ≤ 47k²m(...) ≤ 100k²m(...).

The completion and large-k hypotheses are carried by the downstream completed-measurement theorem; this submeasurement argument only uses the positive k regime and the displayed line-consistency estimate.

theorem MIPRE.LIDT.Co.Pasting.hAConsistency_submeas_from_lineConsistency {𝔓 : 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) (H : SubMeas (MIPStarRE.LDT.Polynomial params.next) 𝔓) (eps delta gamma zeta : ℝ) (hgood : strategy.IsGood eps delta gamma) (hgamma_nonneg : 0 ≤ gamma) (hzeta_nonneg : 0 ≤ zeta) (k : ℕ) (hk_pos : 1 ≤ k) (hline : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) (hRestrictionToVerticalLine params H) (verticalLineMeasurementFamily params strategy) (MIPStarRE.LDT.Pasting.hBConsistencyError params eps delta gamma zeta k)) : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params.next)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params.next H) (MIPStarRE.LDT.MainInductionStep.ldPastingInInductionNu params k eps delta gamma zeta)

Convert source-style vertical-line consistency to point consistency.

This source-style restatement specializes hAConsistency_submeas_from_lineConsistency_of_axis_self to the two estimates contained in strategy.IsGood.

theorem MIPRE.LIDT.Co.Pasting.hAConsistency_submeas_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) (family : IdxPolyFamily params 𝔓) (eps delta gamma zeta : ℝ) (haxis : strategy.axisParallelFailureProbability ≤ eps) (hself_good : strategy.selfConsistencyFailureProbability ≤ delta) (hgamma_nonneg : 0 ≤ gamma) (hzeta_nonneg : 0 ≤ zeta) (k : ℕ) (hk_pos : 1 ≤ k) (hHB : HBConsistencyStatement params strategy family eps delta gamma zeta k) : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params.next)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params.next (constructedPastedSubMeas params family k)) (MIPStarRE.LDT.MainInductionStep.ldPastingInInductionNu params k eps delta gamma zeta)

Specialization of hAConsistency_submeas_from_lineConsistency to the constructed pasted submeasurement.

theorem MIPRE.LIDT.Co.Pasting.hAConsistency_submeas_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) (hzeta_nonneg : 0 ≤ zeta) (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 : ℕ) (hk_pos : 1 ≤ k) (hline : ∀ i < k, LdSandwichLineOnePointStatement params strategy family eps delta gamma zeta k i) : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params.next)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params.next (constructedPastedSubMeas params family k)) (MIPStarRE.LDT.MainInductionStep.ldPastingInInductionNu params k eps delta gamma zeta)

Internal form of cor:h-a-consistency from the one-point sandwich estimates.

This theorem separates the genuinely earlier pasting input from the diagonal test. Once the estimates of lem:ld-sandwich-line-one-point are known for all positions, the passage from H-B consistency to H-A consistency uses only the axis-parallel and self-consistency estimates of the ambient strategy.

theorem MIPRE.LIDT.Co.Pasting.hAConsistency_submeas_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) (hd : 0 < params.d) (family : IdxPolyFamily params 𝔓) (hcons : family.ConsistentWithPoints strategy zeta) (hself : family.StronglySelfConsistent strategy.state zeta) (hbound : IdxPolyFamily.SliceBoundednessInput strategy family zeta) (hfacts : GHatFactsStatement params strategy.state family gamma zeta) (k : ℕ) (hk_pos : 1 ≤ k) : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params.next)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params.next (constructedPastedSubMeas params family k)) (MIPStarRE.LDT.MainInductionStep.ldPastingInInductionNu params k eps delta gamma zeta)

Internal form of cor:h-a-consistency from cor:G-hat-facts.

This is the same proof as hAConsistency_submeas_ofLinePointBounds_of_axis_self, with the one-point sandwich estimates constructed from GHatFactsStatement.

theorem MIPRE.LIDT.Co.Pasting.hAConsistency_submeas_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) (hbound : IdxPolyFamily.SliceBoundednessInput strategy family zeta) (hcom : Commutativity.ComMainConclusion params strategy family gamma zeta) (k : ℕ) (hk_pos : 1 ≤ k) : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params.next)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params.next (constructedPastedSubMeas params family k)) (MIPStarRE.LDT.MainInductionStep.ldPastingInInductionNu params k eps delta gamma zeta)

Internal form of cor:h-a-consistency from the Section 11 commutativity conclusion.

This exposes the precise upstream mathematical input needed for the G-hat construction. The diagonal-line estimate is not used in the H-B to H-A transport; it is used only insofar as it is needed to prove the commutativity conclusion supplied here.

theorem MIPRE.LIDT.Co.Pasting.hAConsistency_submeas {𝔓 : 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 : ℕ) (hk_pos : 1 ≤ k) : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params.next)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params.next (constructedPastedSubMeas params family k)) (MIPStarRE.LDT.MainInductionStep.ldPastingInInductionNu params k eps delta gamma zeta)

cor:h-a-consistency.

This is the point-consistency part of the pasted-submeasurement chain. The completed-measurement consistency is deliberately separated as hAConsistency_completed, since the paper proves it only after cor:ld-pasting-N-completeness.

theorem MIPRE.LIDT.Co.Pasting.hAConsistency_completed_from_submeas {𝔓 : 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 kappa zeta : ℝ) (H : SubMeas (MIPStarRE.LDT.Polynomial params.next) 𝔓) (k : ℕ) (hsubmeas : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params.next)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params.next H) (MIPStarRE.LDT.MainInductionStep.ldPastingInInductionNu params k eps delta gamma zeta)) (hcomplete : strategy.state.CompletenessAtLeast (SubMeas.liftLeft strategy.state H) (MIPStarRE.LDT.Pasting.ldPastingCompletenessLowerBound params kappa (MIPStarRE.LDT.MainInductionStep.ldPastingInInductionNu params k eps delta gamma zeta) k)) : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params.next)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params.next (Preliminaries.completeAtOutcome H (MIPStarRE.LDT.Pasting.pastedFallbackOutcome params)).toSubMeas) (MIPStarRE.LDT.MainInductionStep.ldPastingInInductionError params k eps delta gamma kappa zeta)

Complete a polynomial submeasurement after its point consistency and mass lower bound have been proved.

This is the completion step in cor:h-a-consistency, stated for an arbitrary submeasurement H. The source argument first proves point consistency for a submeasurement and then completes it by adding the missing mass to a fixed fallback polynomial.

theorem MIPRE.LIDT.Co.Pasting.hAConsistency_completed {𝔓 : 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 kappa zeta : ℝ) (family : IdxPolyFamily params 𝔓) (k : ℕ) (hsubmeas : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params.next)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params.next (constructedPastedSubMeas params family k)) (MIPStarRE.LDT.MainInductionStep.ldPastingInInductionNu params k eps delta gamma zeta)) (hcomplete : strategy.state.CompletenessAtLeast (SubMeas.liftLeft strategy.state (constructedPastedSubMeas params family k)) (MIPStarRE.LDT.Pasting.ldPastingCompletenessLowerBound params kappa (MIPStarRE.LDT.MainInductionStep.ldPastingInInductionNu params k eps delta gamma zeta) k)) : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params.next)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params.next (constructedPastedMeasurement params family k).toSubMeas) (MIPStarRE.LDT.MainInductionStep.ldPastingInInductionError params k eps delta gamma kappa zeta)

Completed-measurement version of cor:h-a-consistency.

This theorem is intentionally downstream of cor:ld-pasting-N-completeness: it may use the submeasurement consistency together with the completeness bound for the constructed pasted submeasurement to control the added completion mass.