Section 12 pasting: degree-zero branch

Auxiliary constructions for the d = 0 complementary branch of thm:ld-pasting.

References

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

theorem MIPStarRE.LDT.Pasting.degreeZeroPastedPointConsistency {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma kappa zeta : Error) (hgood : strategy.IsGood eps delta gamma) (family : IdxPolyFamily params ι) (hcomplete : family.Complete strategy.state kappa) (hcons : family.ConsistentWithPoints strategy zeta) (hd_zero : params.d = 0) (k : ℕ) : ∃ (H : Measurement (Polynomial params.next) ι), H = Preliminaries.completeAtOutcome (averagedSliceAppendedSubMeas params family) (pastedFallbackOutcome params) ∧ ConsRel strategy.state (uniformDistribution (Point params.next)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params.next H.toSubMeas) (MainInductionStep.ldPastingInInductionError params k eps delta gamma kappa zeta)

Degree-zero point-consistency construction for thm:ld-pasting.

Paper origin: references/ldt-paper/ld-pasting.tex:12-55. In the degree-zero branch the slice polynomials and the last-coordinate line answers are constant on their respective domains. The measurement is the completion of averagedSliceAppendedSubMeas, the averaged slice family viewed as a global polynomial family by ignoring the appended variable.

theorem MIPStarRE.LDT.Pasting.degreeZeroPastedPointConsistency_of_axis_self {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma kappa zeta : Error) (haxis : strategy.axisParallelFailureProbability ≤ eps) (hselfBound : strategy.selfConsistencyFailureProbability ≤ delta) (heps_nonneg : 0 ≤ eps) (hdelta_nonneg : 0 ≤ delta) (hgamma_nonneg : 0 ≤ gamma) (family : IdxPolyFamily params ι) (hcomplete : family.Complete strategy.state kappa) (hcons : family.ConsistentWithPoints strategy zeta) (hd_zero : params.d = 0) (k : ℕ) : ∃ (H : Measurement (Polynomial params.next) ι), H = Preliminaries.completeAtOutcome (averagedSliceAppendedSubMeas params family) (pastedFallbackOutcome params) ∧ ConsRel strategy.state (uniformDistribution (Point params.next)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params.next H.toSubMeas) (MainInductionStep.ldPastingInInductionError params k eps delta gamma kappa zeta)

Axis/self-consistency form of the degree-zero point-consistency construction.

This is the same construction as degreeZeroPastedPointConsistency, with the ordinary good-strategy hypotheses replaced by the two estimates actually used in the proof.