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: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/Core/LdGbcon.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 𝔓, so the two vertical-line measurements are local families in 𝔓, and the distance bounds are SDDRels of their right placements on strategy.state. The vendored swap consRel_symm_of_density_fixed strategy.state strategy.densityFixed is the model's theorem SymModel.consRel_symm_of_density_fixed, and the normalization strategy.isNormalized that the vendored triangleSub_right takes is not a hypothesis of the ported one, so no swap or normalization hypothesis appears.

Two proofs are shorter than the vendored ones. pointVerticalLineSdd_of_axis_self drops the vendored point self-consistency ConsRel, which it computed and did not use. ldGbcon_of_axis_self is Preliminaries.triangleSub_right applied to the point consistency of the family and to pointVerticalLineSdd_of_axis_self directly, in place of a second copy of that bound's proof followed by a rewrite along ldGbconAxisLineMeasurement_eq_verticalLineMeasurement.

Not ported

Every declaration of the vendored file has a counterpart here.

References

In LionSR/MIPStarRE at commit 507e8122, not in this repository:

• references/ldt-paper/ld-pasting.tex

noncomputable def MIPRE.LIDT.Co.Pasting.ldGbconAxisLineMeasurement {𝔓 : 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) : IdxMeas (MIPStarRE.LDT.Point params.next) (MIPStarRE.LDT.Fq params) 𝔓

The axis-parallel line measurement in the last direction through u, read at its base point: the line answer B^u of the axis-parallel test conditioned on the last direction.

Equations

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

noncomputable def MIPRE.LIDT.Co.Pasting.ldGbconVerticalLineMeasurement {𝔓 : 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) : IdxMeas (MIPStarRE.LDT.Point params.next) (MIPStarRE.LDT.Fq params) 𝔓

The vertical line through u, based at height zero, read at the height of u: the vertical-line answer B^u as a measurement.

Equations

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

theorem MIPRE.LIDT.Co.Pasting.ldGbconAxisLineMeasurement_eq_verticalLineMeasurement {𝔓 : 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) : (ldGbconAxisLineMeasurement params strategy).toIdxSubMeas = (ldGbconVerticalLineMeasurement params strategy).toIdxSubMeas

The two readings of B^u agree, by the rebasing covariance of the axis-parallel measurement: rebasing the vertical line at the height of u gives the last-direction line through u.

theorem MIPRE.LIDT.Co.Pasting.ldGbcon_axis_last_direction_consistency {𝔓 : 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 : ℝ) (haxis : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.AxisParallelTestSample params.next)) (axisParallelPointAnswerFamily strategy) (axisParallelLineAnswerFamily strategy) eps) : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params.next)) strategy.pointMeasurement.toIdxSubMeas (ldGbconAxisLineMeasurement params strategy).toIdxSubMeas (↑params.next.m * eps)

The point measurements are m'·ε-consistent with the last-direction line answers, where m' = m + 1 is the number of directions and ε bounds the axis-parallel test averaged over all directions.

theorem MIPRE.LIDT.Co.Pasting.pointVerticalLineSdd_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 : ℝ) (haxis : strategy.axisParallelFailureProbability ≤ eps) (hself : strategy.selfConsistencyFailureProbability ≤ delta) : strategy.state.SDDRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params.next)) (IdxSubMeas.liftRight strategy.state strategy.pointMeasurement.toIdxSubMeas) (IdxSubMeas.liftRight strategy.state (ldGbconVerticalLineMeasurement params strategy).toIdxSubMeas) (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 MIPRE.LIDT.Co.Pasting.pointVerticalLineSdd_liftedVerticalLine_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 : ℝ) (haxis : strategy.axisParallelFailureProbability ≤ eps) (hself : strategy.selfConsistencyFailureProbability ≤ delta) : strategy.state.SDDRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params.next)) (IdxSubMeas.liftRight strategy.state strategy.pointMeasurement.toIdxSubMeas) (IdxSubMeas.liftRight strategy.state (liftedVerticalLineAnswerFamily params strategy)) (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 MIPRE.LIDT.Co.Pasting.pointVerticalLineSdd {𝔓 : 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 : ℝ) (hgood : strategy.IsGood eps delta gamma) : strategy.state.SDDRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params.next)) (IdxSubMeas.liftRight strategy.state strategy.pointMeasurement.toIdxSubMeas) (IdxSubMeas.liftRight strategy.state (ldGbconVerticalLineMeasurement params strategy).toIdxSubMeas) (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 MIPRE.LIDT.Co.Pasting.ldGbcon_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 zeta : ℝ) (haxis : strategy.axisParallelFailureProbability ≤ eps) (hself : strategy.selfConsistencyFailureProbability ≤ delta) (family : IdxPolyFamily params 𝔓) (hcons : family.ConsistentWithPoints strategy zeta) : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params.next)) (evaluateFiberFamilyAtNextPoint params family.meas.toIdxSubMeas) (fun (u : MIPStarRE.LDT.Point params.next) => postprocess (verticalLineMeasurementFamily params strategy (MIPStarRE.LDT.truncatePoint params u)) fun (f : MIPStarRE.LDT.AxisLinePolynomial params.next) => f.toFun (MIPStarRE.LDT.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 MIPRE.LIDT.Co.Pasting.ldGbcon {𝔓 : 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) (family : IdxPolyFamily params 𝔓) (hcons : family.ConsistentWithPoints strategy zeta) : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params.next)) (evaluateFiberFamilyAtNextPoint params family.meas.toIdxSubMeas) (fun (u : MIPStarRE.LDT.Point params.next) => postprocess (verticalLineMeasurementFamily params strategy (MIPStarRE.LDT.truncatePoint params u)) fun (f : MIPStarRE.LDT.AxisLinePolynomial params.next) => f.toFun (MIPStarRE.LDT.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 MIPRE.LIDT.Co.Pasting.ldGbcon_liftedVerticalLine_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 zeta : ℝ) (haxis : strategy.axisParallelFailureProbability ≤ eps) (hself : strategy.selfConsistencyFailureProbability ≤ delta) (family : IdxPolyFamily params 𝔓) (hcons : family.ConsistentWithPoints strategy zeta) : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.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 MIPRE.LIDT.Co.Pasting.ldGbcon_liftedVerticalLine {𝔓 : 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) (family : IdxPolyFamily params 𝔓) (hcons : family.ConsistentWithPoints strategy zeta) : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params.next)) family.evaluatedAtNextPoint (liftedVerticalLineAnswerFamily params strategy) (zeta + √(8 * ↑params.m * eps + 4 * delta))

Named-family form of lem:ld-gbcon.