Section 12 pasting: degree-zero branch

Auxiliary constructions for the d = 0 complementary branch of thm:ld-pasting: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/Bernoulli/DegreeZero.lean in the port of planning/c6b-plan.md (milestone M11, section "Port conventions").

A strategy is a SymStrat params.next 𝔓 K and a slice family an IdxPolyFamily params 𝔓; the candidate is the averaged slice family viewed as a polynomial in one more variable, averagedSliceAppendedSubMeas, and the consistency statements are ConsRels on 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.

The proofs are shorter than the vendored ones. The good-strategy forms degreeZero_averagedSlice_liftedVerticalLineConsistency, degreeZero_averagedSlice_pointConsistency and degreeZeroPastedPointConsistency are their axis/self-consistency forms applied to hgood.axisParallelTest and hgood.selfConsistencyTest, so each is declared after its _of_axis_self form, the reverse of the vendored order. The height averaging of the lifted-line estimate decomposes both sides through avgOver_uniform_pointNext_decompose once each.

Not ported

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.degreeZero_submeas_error_le_two_nu (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (eps delta gamma zeta : ℝ) (k : ℕ) (hk_pos : 1 ≤ k) (heps_nonneg : 0 ≤ eps) (hdelta_nonneg : 0 ≤ delta) (hgamma_nonneg : 0 ≤ gamma) (hzeta_nonneg : 0 ≤ zeta) : min zeta 1 + 2 * √(8 * ↑params.m * min eps 1 + 4 * min delta 1) ≤ 2 * MIPStarRE.LDT.MainInductionStep.ldPastingInInductionNu params k eps delta gamma zeta

Upstream keeps this helper private since its Lean-module port (LionSR/MIPStarRE at 5fc363b); the port carries its own copy, with upstream's proof.

Scalar absorption for the degree-zero submeasurement consistency error.

theorem MIPRE.LIDT.Co.Pasting.polynomialEvaluation_averagedSliceAppendedSubMeas_eq_average {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (u : MIPStarRE.LDT.Point params.next) : polynomialEvaluationFamily params.next (averagedSliceAppendedSubMeas params family) u = averageIdxSubMeas (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Fq params)) (fun (x : MIPStarRE.LDT.Fq params) => family.evaluatedAtNextPoint (MIPStarRE.LDT.appendPoint params (MIPStarRE.LDT.truncatePoint params u) x)) ⋯

Evaluating the degree-zero appended-slice candidate is the height average of the original evaluated slice family at the same old point.

theorem MIPRE.LIDT.Co.Pasting.consistentWithPoints_min_one {𝔓 : 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 𝔓) (zeta : ℝ) (hcons : family.ConsistentWithPoints strategy zeta) : family.ConsistentWithPoints strategy (min zeta 1)

The point-consistency hypothesis may be truncated at the trivial unit bound.

theorem MIPRE.LIDT.Co.Pasting.degreeZero_averagedSlice_liftedVerticalLineConsistency_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) (hd_zero : params.d = 0) : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params.next)) (polynomialEvaluationFamily params.next (averagedSliceAppendedSubMeas params family)) (liftedVerticalLineAnswerFamily params strategy) (min zeta 1 + √(8 * ↑params.m * min eps 1 + 4 * min delta 1))

Axis/self-consistency form of the degree-zero lifted-line consistency estimate.

The degree-zero averaging argument uses the axis-parallel test and self-consistency, but not the diagonal-line test.

theorem MIPRE.LIDT.Co.Pasting.degreeZero_averagedSlice_liftedVerticalLineConsistency {𝔓 : 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) (hd_zero : params.d = 0) : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params.next)) (polynomialEvaluationFamily params.next (averagedSliceAppendedSubMeas params family)) (liftedVerticalLineAnswerFamily params strategy) (min zeta 1 + √(8 * ↑params.m * min eps 1 + 4 * min delta 1))

The averaged degree-zero pasted submeasurement is consistent with the lifted vertical-line answers.

theorem MIPRE.LIDT.Co.Pasting.degreeZero_averagedSlice_pointConsistency_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) (hd_zero : params.d = 0) : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params.next)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params.next (averagedSliceAppendedSubMeas params family)) (min zeta 1 + 2 * √(8 * ↑params.m * min eps 1 + 4 * min delta 1))

Axis/self-consistency form of the degree-zero point-consistency estimate before completion.

theorem MIPRE.LIDT.Co.Pasting.degreeZero_averagedSlice_pointConsistency {𝔓 : 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) (hd_zero : params.d = 0) : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params.next)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params.next (averagedSliceAppendedSubMeas params family)) (min zeta 1 + 2 * √(8 * ↑params.m * min eps 1 + 4 * min delta 1))

The averaged degree-zero pasted submeasurement is point-consistent before completion.

theorem MIPRE.LIDT.Co.Pasting.degreeZeroPastedPointConsistency_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 kappa zeta : ℝ) (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 (MIPStarRE.LDT.Polynomial params.next) 𝔓), H = Preliminaries.completeAtOutcome (averagedSliceAppendedSubMeas params family) (MIPStarRE.LDT.Pasting.pastedFallbackOutcome params) ∧ strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params.next)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params.next H.toSubMeas) (MIPStarRE.LDT.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.

theorem MIPRE.LIDT.Co.Pasting.degreeZeroPastedPointConsistency {𝔓 : 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 : ℝ) (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 (MIPStarRE.LDT.Polynomial params.next) 𝔓), H = Preliminaries.completeAtOutcome (averagedSliceAppendedSubMeas params family) (MIPStarRE.LDT.Pasting.pastedFallbackOutcome params) ∧ strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params.next)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params.next H.toSubMeas) (MIPStarRE.LDT.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.