Section 12 pasting: H-A consistency

Vertical-line to point-consistency transport and completed-measurement statement for cor:h-a-consistency.

References

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

theorem MIPStarRE.LDT.Pasting.hAConsistency_submeas_from_lineConsistency_of_axis_self {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (H : SubMeas (Polynomial params.next) ι) (eps delta gamma zeta : Error) (haxis : strategy.axisParallelFailureProbability ≤ eps) (hself_good : strategy.selfConsistencyFailureProbability ≤ delta) (hgamma_nonneg : 0 ≤ gamma) (hzeta_nonneg : 0 ≤ zeta) (k : ℕ) (hk_pos : 1 ≤ k) (hline : ConsRel strategy.state (uniformDistribution (Point params)) (hRestrictionToVerticalLine params H) (verticalLineMeasurementFamily params strategy) (hBConsistencyError params eps delta gamma zeta k)) : ConsRel strategy.state (uniformDistribution (Point params.next)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params.next H) (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 MIPStarRE.LDT.Pasting.hAConsistency_submeas_from_lineConsistency {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (H : SubMeas (Polynomial params.next) ι) (eps delta gamma zeta : Error) (hgood : strategy.IsGood eps delta gamma) (hgamma_nonneg : 0 ≤ gamma) (hzeta_nonneg : 0 ≤ zeta) (k : ℕ) (hk_pos : 1 ≤ k) (hline : ConsRel strategy.state (uniformDistribution (Point params)) (hRestrictionToVerticalLine params H) (verticalLineMeasurementFamily params strategy) (hBConsistencyError params eps delta gamma zeta k)) : ConsRel strategy.state (uniformDistribution (Point params.next)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params.next H) (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 MIPStarRE.LDT.Pasting.hAConsistency_submeas_ofLinePointBounds_of_axis_self {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma zeta : Error) (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) : ConsRel strategy.state (uniformDistribution (Point params.next)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params.next (constructedPastedSubMeas params family k)) (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 MIPStarRE.LDT.Pasting.hAConsistency_submeas_ofGHatFacts_of_axis_self {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma zeta : Error) (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) : ConsRel strategy.state (uniformDistribution (Point params.next)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params.next (constructedPastedSubMeas params family k)) (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 MIPStarRE.LDT.Pasting.hAConsistency_submeas_ofComMain_of_axis_self {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma zeta : Error) (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) : ConsRel strategy.state (uniformDistribution (Point params.next)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params.next (constructedPastedSubMeas params family k)) (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 MIPStarRE.LDT.Pasting.hAConsistency_submeas {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (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) (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) : ConsRel strategy.state (uniformDistribution (Point params.next)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params.next (constructedPastedSubMeas params family k)) (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 MIPStarRE.LDT.Pasting.hAConsistency_completed_from_submeas {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma kappa zeta : Error) (H : SubMeas (Polynomial params.next) ι) (k : ℕ) (hsubmeas : ConsRel strategy.state (uniformDistribution (Point params.next)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params.next H) (MainInductionStep.ldPastingInInductionNu params k eps delta gamma zeta)) (hcomplete : CompletenessAtLeast strategy.state H.liftLeft (ldPastingCompletenessLowerBound params kappa (MainInductionStep.ldPastingInInductionNu params k eps delta gamma zeta) k)) : ConsRel strategy.state (uniformDistribution (Point params.next)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params.next (Preliminaries.completeAtOutcome H (pastedFallbackOutcome params)).toSubMeas) (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 MIPStarRE.LDT.Pasting.hAConsistency_completed {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma kappa zeta : Error) (family : IdxPolyFamily params ι) (k : ℕ) (hsubmeas : ConsRel strategy.state (uniformDistribution (Point params.next)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params.next (constructedPastedSubMeas params family k)) (MainInductionStep.ldPastingInInductionNu params k eps delta gamma zeta)) (hcomplete : CompletenessAtLeast strategy.state (constructedPastedSubMeas params family k).liftLeft (ldPastingCompletenessLowerBound params kappa (MainInductionStep.ldPastingInInductionNu params k eps delta gamma zeta) k)) : ConsRel strategy.state (uniformDistribution (Point params.next)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params.next (constructedPastedMeasurement params family k).toSubMeas) (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.