Section 12 pasting: vertical-line consistency transfer

The ldGbcon transfer compares the slice family G^x with the vertical-line answers B^u. It combines the conditioned axis-parallel consistency estimate with the point-to-vertical-line state-dependent-distance bound.

noncomputable def MIPStarRE.LDT.Pasting.ldGbconVerticalLineMeasurement {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) : IdxMeas (Point params.next) (Fq params) ι

Equations

• One or more equations did not get rendered due to their size.

theorem MIPStarRE.LDT.Pasting.pointVerticalLineSdd_of_axis_self {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta : Error) (haxis : strategy.axisParallelFailureProbability ≤ eps) (hself : strategy.selfConsistencyFailureProbability ≤ delta) : SDDRel strategy.state (uniformDistribution (Point params.next)) strategy.pointMeasurement.toIdxSubMeas.liftRight (ldGbconVerticalLineMeasurement params strategy).toIdxSubMeas.liftRight (8 * ↑params.m * eps + 4 * delta)

Axis/self-consistency form of lem:point-vertical-line-sdd.

The proof of the point-to-vertical-line transfer uses only the axis-parallel test and point self-consistency. The diagonal-line test is not part of this calculation.

theorem MIPStarRE.LDT.Pasting.pointVerticalLineSdd_liftedVerticalLine_of_axis_self {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta : Error) (haxis : strategy.axisParallelFailureProbability ≤ eps) (hself : strategy.selfConsistencyFailureProbability ≤ delta) : SDDRel strategy.state (uniformDistribution (Point params.next)) strategy.pointMeasurement.toIdxSubMeas.liftRight (liftedVerticalLineAnswerFamily params strategy).liftRight (8 * ↑params.m * eps + 4 * delta)

Named submeasurement-family form of pointVerticalLineSdd_of_axis_self.

The proof above constructs the vertical-line measurement as a complete measurement-valued family. The degree-zero estimates use only its underlying submeasurement family, namely liftedVerticalLineAnswerFamily.

theorem MIPStarRE.LDT.Pasting.pointVerticalLineSdd {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma : Error) (hgood : strategy.IsGood eps delta gamma) : SDDRel strategy.state (uniformDistribution (Point params.next)) strategy.pointMeasurement.toIdxSubMeas.liftRight (ldGbconVerticalLineMeasurement params strategy).toIdxSubMeas.liftRight (8 * ↑params.m * eps + 4 * delta)

lem:point-vertical-line-sdd. A good strategy induces a state-dependent distance bound between the point measurements and the vertical-line (axis-parallel rebased) measurements.

theorem MIPStarRE.LDT.Pasting.ldGbcon_of_axis_self {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta zeta : Error) (haxis : strategy.axisParallelFailureProbability ≤ eps) (hself : strategy.selfConsistencyFailureProbability ≤ delta) (family : IdxPolyFamily params ι) (hcons : family.ConsistentWithPoints strategy zeta) : ConsRel strategy.state (uniformDistribution (Point params.next)) (evaluateFiberFamilyAtNextPoint params family.meas.toIdxSubMeas) (fun (u : Point params.next) => postprocess (verticalLineMeasurementFamily params strategy (truncatePoint params u)) fun (f : AxisLinePolynomial params.next) => f.toFun (pointHeight params u)) (zeta + √(8 * ↑params.m * eps + 4 * delta))

lem:ld-gbcon.

This is the direct consistency transfer from the slice family G^x to the vertical line answers B^u, obtained by composing the hypothesis item:ld-pasting-consistency with the conditioned axis-parallel test relation.

theorem MIPStarRE.LDT.Pasting.ldGbcon {ι : 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) (family : IdxPolyFamily params ι) (hcons : family.ConsistentWithPoints strategy zeta) : ConsRel strategy.state (uniformDistribution (Point params.next)) (evaluateFiberFamilyAtNextPoint params family.meas.toIdxSubMeas) (fun (u : Point params.next) => postprocess (verticalLineMeasurementFamily params strategy (truncatePoint params u)) fun (f : AxisLinePolynomial params.next) => f.toFun (pointHeight params u)) (zeta + √(8 * ↑params.m * eps + 4 * delta))

lem:ld-gbcon.

This is the direct consistency transfer from the slice family G^x to the vertical line answers B^u, obtained by composing the hypothesis item:ld-pasting-consistency with the conditioned axis-parallel test relation.

theorem MIPStarRE.LDT.Pasting.ldGbcon_liftedVerticalLine_of_axis_self {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta zeta : Error) (haxis : strategy.axisParallelFailureProbability ≤ eps) (hself : strategy.selfConsistencyFailureProbability ≤ delta) (family : IdxPolyFamily params ι) (hcons : family.ConsistentWithPoints strategy zeta) : ConsRel strategy.state (uniformDistribution (Point params.next)) family.evaluatedAtNextPoint (liftedVerticalLineAnswerFamily params strategy) (zeta + √(8 * ↑params.m * eps + 4 * delta))

Named-family form of lem:ld-gbcon.

This is the same consistency transfer as ldGbcon, restated with the two families used in the degree-zero branch of thm:ld-pasting: the evaluated slice family family.evaluatedAtNextPoint and the lifted vertical-line family liftedVerticalLineAnswerFamily. In the degree-zero branch, these are the two families whose pointwise invariance properties must be combined to control height dependence.

theorem MIPStarRE.LDT.Pasting.ldGbcon_liftedVerticalLine {ι : 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) (family : IdxPolyFamily params ι) (hcons : family.ConsistentWithPoints strategy zeta) : ConsRel strategy.state (uniformDistribution (Point params.next)) family.evaluatedAtNextPoint (liftedVerticalLineAnswerFamily params strategy) (zeta + √(8 * ↑params.m * eps + 4 * delta))

Named-family form of lem:ld-gbcon.