Section 12 pasting: final pasting theorems

The completeness corollary cor:ld-pasting-N-completeness, the sub-measurement lemma lem:ld-pasting-sub-measurement and the pasting theorem thm:ld-pasting with its complementary branches: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/Bernoulli/Final.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 𝔓; errors are in ℝ. Every statement keeps the vendored argument list and order, and none has a swap, density or normalization hypothesis (the vendored ones had none either). Inside the proofs, three uses of the vendored strategy fields are replaced (section "Swap symmetry is a theorem"):

• in fromHToGBernoulliTailMass_lower_bound, the matrix Chernoff lemma is applied to the vector state strategy.state.toVecState without the vendored strategy.isNormalized, and the swap strategy.permInvState.swap_ev that moves the Bernoulli tail from the left register to the right one is S.ev_L_eq_ev_R, after bernoulliTailOperator_leftTensor;
• in ldPasting_of_one_le_error, bipartiteConsError_uniform_le_one strategy.state strategy.isNormalized is the keystone's strategy.state.bipartiteConsError_uniform_le_one;
• the nonnegativity of κ in fromHToGBernoulliTailMass_lower_bound is the ported kappa_nonneg_of_complete rather than an inline repetition of it.

The four arithmetic lemmas at the head of the vendored file mention no state, operator or measurement, so they are not ported: this file imports the vendored file and names them through an explicit open MIPStarRE.LDT.Pasting (…) list.

Not ported

References

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

• references/ldt-paper/ld-pasting.tex
• docs/paper-gaps/issue-1622-ld-pasting-degree-zero.tex

theorem MIPRE.LIDT.Co.Pasting.overAllOutcomesError_add_fromHToGError_le_ldPastingNu (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) : MIPStarRE.LDT.Pasting.overAllOutcomesError params eps delta gamma zeta k + MIPStarRE.LDT.Pasting.fromHToGError params gamma zeta k ≤ 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.

Arithmetic helper for cor:ld-pasting-N-completeness: absorb the overAllOutcomes and fromHToG scalar losses into ldPastingInInductionNu.

The proof uses that the corrected fromHToGError tail sum is a sub-sum of the full overAllOutcomesError sum and the slack 46 + 46 ≤ 100.

theorem MIPRE.LIDT.Co.Pasting.ldPasting_theta_inv_le (params : MIPStarRE.LDT.Parameters) : 1 / (1 - 1 / (200 * ↑params.m)) ≤ 1 + 1 / (100 * ↑params.m)

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

Paper arithmetic: for θ = 1/(200m), 1/(1-θ) ≤ 1 + 1/(100m).

theorem MIPRE.LIDT.Co.Pasting.ldPasting_chernoff_exponent_eq (params : MIPStarRE.LDT.Parameters) (k : ℕ) : -((1 / (200 * ↑params.m)) ^ 2 * ↑k) / 2 = -(↑k / (80000 * ↑params.m ^ 2))

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

Paper arithmetic: the matrix-Chernoff exponential at θ = 1/(200m) is the stated exp(-k/(80000m²)) term.

theorem MIPRE.LIDT.Co.Pasting.ldPasting_chernoff_size (params : MIPStarRE.LDT.Parameters) (k : ℕ) (hk : 400 * params.m * params.d ≤ k) : 2 * ↑params.d / (1 / (200 * ↑params.m)) ≤ ↑k

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

The public size assumption k ≥ 400md implies the matrix-Chernoff size condition k ≥ 2d/θ at θ = 1/(200m).

theorem MIPRE.LIDT.Co.Pasting.fromHToGBernoulliTailMass_lower_bound {𝔓 : 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) (kappa : ℝ) (family : IdxPolyFamily params 𝔓) (hcomplete : family.Complete strategy.state kappa) (k : ℕ) (hk : 400 * params.m * params.d ≤ k) : 1 - kappa * (1 + 1 / (100 * ↑params.m)) - Real.exp (-(↑k / (80000 * ↑params.m ^ 2))) ≤ fromHToGBernoulliTailMass params strategy.state family k

Specialize lem:chernoff-bernoulli-matrix to the averaged complete operator G = 𝔼_x ∑_g G^x_g and the paper's θ = 1/(200m).

This is the Bernoulli-tail lower-bound step in cor:ld-pasting-N-completeness: the matrix Chernoff lemma is applied to S.L G on the vector state, bernoulliTailOperator_leftTensor identifies its conclusion, and the swap S.ev_L_eq_ev_R transfers it to the right-register fromHToGBernoulliTailMass.

theorem MIPRE.LIDT.Co.Pasting.ldPastingNCompleteness_of_overAllOutcomes_fromHToG_tail {𝔓 : 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 : ℝ) (heps_nonneg : 0 ≤ eps) (hdelta_nonneg : 0 ≤ delta) (hgamma_nonneg : 0 ≤ gamma) (hzeta_nonneg : 0 ≤ zeta) (family : IdxPolyFamily params 𝔓) (k : ℕ) (hk_pos : 1 ≤ k) (hOAO : OverAllOutcomesStatement params strategy family eps delta gamma zeta k) (hFrom : FromHToGStatement params strategy strategy.state family gamma zeta k) (htail : 1 - kappa * (1 + 1 / (100 * ↑params.m)) - Real.exp (-(↑k / (80000 * ↑params.m ^ 2))) ≤ fromHToGBernoulliTailMass params strategy.state family k) : LdPastingNCompletenessStatement params strategy family kappa (MIPStarRE.LDT.MainInductionStep.ldPastingInInductionNu params k eps delta gamma zeta) k

Internal form of cor:ld-pasting-N-completeness from the two preceding mass-comparison inputs.

This theorem isolates the scalar assembly after lem:over-all-outcomes, lem:from-H-to-G, and the Bernoulli-tail lower bound have already been established.

theorem MIPRE.LIDT.Co.Pasting.ldPastingNCompleteness_of_tailLowerBound {𝔓 : 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) (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) (_hk : 400 * params.m * params.d ≤ k) (htail : 1 - kappa * (1 + 1 / (100 * ↑params.m)) - Real.exp (-(↑k / (80000 * ↑params.m ^ 2))) ≤ fromHToGBernoulliTailMass params strategy.state family k) : LdPastingNCompletenessStatement params strategy family kappa (MIPStarRE.LDT.MainInductionStep.ldPastingInInductionNu params k eps delta gamma zeta) k

cor:ld-pasting-N-completeness once the Bernoulli-tail lower bound is supplied explicitly.

This records the downstream scalar algebra after lem:over-all-outcomes and lem:from-H-to-G. The hypothesis htail is exactly the θ = 1 / (200m) specialization of lem:chernoff-bernoulli-matrix for the averaged complete operator G = \mathbb E_x \sum_g G^x_g, expressed as the concrete fromHToGBernoulliTailMass lower bound with error κ · (1 + 1/(100m)) + exp(-k / (80000 m²)).

theorem MIPRE.LIDT.Co.Pasting.ldPastingNCompleteness {𝔓 : 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) (hgamma_le : gamma ≤ 1) (hzeta_le : zeta ≤ 1) (hdq_le : params.d ≤ params.q) (hd : 0 < params.d) (family : IdxPolyFamily params 𝔓) (hcomplete : family.Complete strategy.state kappa) (hcons : family.ConsistentWithPoints strategy zeta) (hself : family.StronglySelfConsistent strategy.state zeta) (hbound : IdxPolyFamily.SliceBoundednessInput strategy family zeta) (k : ℕ) (hk_pos : 1 ≤ k) (hk : 400 * params.m * params.d ≤ k) : LdPastingNCompletenessStatement params strategy family kappa (MIPStarRE.LDT.MainInductionStep.ldPastingInInductionNu params k eps delta gamma zeta) k

cor:ld-pasting-N-completeness.

theorem MIPRE.LIDT.Co.Pasting.ldPastingNCompleteness_ofComMain_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) (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 𝔓) (hcomplete : family.Complete strategy.state kappa) (hcons : family.ConsistentWithPoints strategy zeta) (hself : family.StronglySelfConsistent strategy.state zeta) (hcom : Commutativity.ComMainConclusion params strategy family gamma zeta) (k : ℕ) (hk_pos : 1 ≤ k) (hk : 400 * params.m * params.d ≤ k) : LdPastingNCompletenessStatement params strategy family kappa (MIPStarRE.LDT.MainInductionStep.ldPastingInInductionNu params k eps delta gamma zeta) k

Internal form of cor:ld-pasting-N-completeness from the Section 11 commutativity conclusion.

theorem MIPRE.LIDT.Co.Pasting.ldPastingSubMeas {𝔓 : 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) (hgamma_le : gamma ≤ 1) (hzeta_le : zeta ≤ 1) (hdq_le : params.d ≤ params.q) (hd : 0 < params.d) (family : IdxPolyFamily params 𝔓) (hcomplete : family.Complete strategy.state kappa) (hcons : family.ConsistentWithPoints strategy zeta) (hself : family.StronglySelfConsistent strategy.state zeta) (hbound : IdxPolyFamily.SliceBoundednessInput strategy family zeta) (k : ℕ) (hk_pos : 1 ≤ k) (hk : 400 * params.m * params.d ≤ k) : ∃ (H : SubMeas (MIPStarRE.LDT.Polynomial params.next) 𝔓), H = constructedPastedSubMeas params family k ∧ LdPastingSubMeasConclusion params strategy family H eps delta gamma kappa zeta k

lem:ld-pasting-sub-measurement.

theorem MIPRE.LIDT.Co.Pasting.ldPastingNontrivial {𝔓 : 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) (hgamma_le : gamma ≤ 1) (hzeta_le : zeta ≤ 1) (hdq_le : params.d ≤ params.q) (hd : 0 < params.d) (family : IdxPolyFamily params 𝔓) (hcomplete : family.Complete strategy.state kappa) (hcons : family.ConsistentWithPoints strategy zeta) (hself : family.StronglySelfConsistent strategy.state zeta) (hbound : IdxPolyFamily.SliceBoundednessInput strategy family zeta) (k : ℕ) (hk_pos : 1 ≤ k) (hk : 400 * params.m * params.d ≤ k) : ∃ (H : Measurement (MIPStarRE.LDT.Polynomial params.next) 𝔓), H = constructedPastedMeasurement params family k ∧ LdPastingConclusion params strategy family H eps delta gamma kappa zeta k

Restricted nontrivial-regime Lean form of thm:ld-pasting.

The source theorem is references/ldt-paper/ld-pasting.tex, lines 12--50. Lines 52--55 explain that the proof may assume the nontrivial regime eps, delta, gamma, zeta, d / q ≤ 1, since the complementary cases are trivial. This declaration states the restricted assumptions gamma ≤ 1, zeta ≤ 1, params.d ≤ params.q, 0 < params.d, and 1 ≤ k. The unrestricted statement aligned with the paper is ldPasting; the degree-zero complementary branch is handled separately by ldPastingDegreeZeroBranch.

theorem MIPRE.LIDT.Co.Pasting.ldPasting_of_one_le_error {𝔓 : 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 : ℝ) (family : IdxPolyFamily params 𝔓) (k : ℕ) (herror : 1 ≤ MIPStarRE.LDT.MainInductionStep.ldPastingInInductionError params k eps delta gamma kappa zeta) : ∃ (H : Measurement (MIPStarRE.LDT.Polynomial params.next) 𝔓), LdPastingConclusion params strategy family H eps delta gamma kappa zeta k

Trivial consistency conclusion when the target pasting error is at least 1.

The consistency defect of two submeasurements against the state of a symmetric model is always at most 1; hence a scalar lower bound 1 ≤ ldPastingInInductionError ... is enough to produce the final conclusion with a distinguished trivial measurement.

theorem MIPRE.LIDT.Co.Pasting.ldPasting_of_one_le_nu_or_zero_k {𝔓 : 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 : ℝ) (family : IdxPolyFamily params 𝔓) (hcomplete : family.Complete strategy.state kappa) (k : ℕ) (hnu : 1 ≤ k → 1 ≤ MIPStarRE.LDT.MainInductionStep.ldPastingInInductionNu params k eps delta gamma zeta) : ∃ (H : Measurement (MIPStarRE.LDT.Polynomial params.next) 𝔓), LdPastingConclusion params strategy family H eps delta gamma kappa zeta k

Trivial consistency conclusion from the complementary scalar branches.

If k is positive, it suffices to show that the ν term in the pasting error is at least 1; if k = 0, the exponential term already gives the trivial bound.

theorem MIPRE.LIDT.Co.Pasting.ldPastingLargeGammaBranch {𝔓 : 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) (_hself : family.StronglySelfConsistent strategy.state zeta) (_hbound : IdxPolyFamily.SliceBoundednessInput strategy family zeta) (k : ℕ) (_hk : 400 * params.m * params.d ≤ k) (hgamma : 1 < gamma) : ∃ (H : Measurement (MIPStarRE.LDT.Polynomial params.next) 𝔓), LdPastingConclusion params strategy family H eps delta gamma kappa zeta k

Complementary branch for thm:ld-pasting when gamma > 1.

Paper origin: references/ldt-paper/ld-pasting.tex:52-55, where this is one of the large-error cases in which the final consistency bound is trivial. This is one of the proved complementary cases for thm:ld-pasting.

theorem MIPRE.LIDT.Co.Pasting.ldPastingLargeZetaBranch {𝔓 : 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) (_hself : family.StronglySelfConsistent strategy.state zeta) (_hbound : IdxPolyFamily.SliceBoundednessInput strategy family zeta) (k : ℕ) (_hk : 400 * params.m * params.d ≤ k) (hzeta : 1 < zeta) : ∃ (H : Measurement (MIPStarRE.LDT.Polynomial params.next) 𝔓), LdPastingConclusion params strategy family H eps delta gamma kappa zeta k

Complementary branch for thm:ld-pasting when zeta > 1.

Paper origin: references/ldt-paper/ld-pasting.tex:52-55, where this is one of the large-error cases in which the final consistency bound is trivial. This is one of the proved complementary cases for thm:ld-pasting.

theorem MIPRE.LIDT.Co.Pasting.ldPastingLargeDegreeRatioBranch {𝔓 : 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) (_hself : family.StronglySelfConsistent strategy.state zeta) (_hbound : IdxPolyFamily.SliceBoundednessInput strategy family zeta) (k : ℕ) (_hk : 400 * params.m * params.d ≤ k) (hdq : params.q < params.d) : ∃ (H : Measurement (MIPStarRE.LDT.Polynomial params.next) 𝔓), LdPastingConclusion params strategy family H eps delta gamma kappa zeta k

Complementary branch for thm:ld-pasting when d > q.

Paper origin: references/ldt-paper/ld-pasting.tex:52-55, where this is the large-error case (d/q) ≥ 1. This is one of the proved complementary cases for thm:ld-pasting.

theorem MIPRE.LIDT.Co.Pasting.ldPastingZeroKBranch {𝔓 : 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) (_hself : family.StronglySelfConsistent strategy.state zeta) (_hbound : IdxPolyFamily.SliceBoundednessInput strategy family zeta) (k : ℕ) (_hk : 400 * params.m * params.d ≤ k) (hk_zero : k = 0) : ∃ (H : Measurement (MIPStarRE.LDT.Polynomial params.next) 𝔓), LdPastingConclusion params strategy family H eps delta gamma kappa zeta k

Complementary branch for thm:ld-pasting when k = 0.

This branch is a boundary case for the reduction to the nontrivial theorem, whose proof assumes 1 ≤ k. The scalar calculation showing that the exponential term gives the trivial bound is the vendored one_le_ldPastingError_of_k_eq_zero.

theorem MIPRE.LIDT.Co.Pasting.ldPastingDegreeZeroBranch {𝔓 : 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) (_hself : family.StronglySelfConsistent strategy.state zeta) (_hbound : IdxPolyFamily.SliceBoundednessInput strategy family zeta) (k : ℕ) (_hk : 400 * params.m * params.d ≤ k) (hd_zero : params.d = 0) (_hk_pos : 1 ≤ k) : ∃ (H : Measurement (MIPStarRE.LDT.Polynomial params.next) 𝔓), LdPastingConclusion params strategy family H eps delta gamma kappa zeta k

Degree-zero complementary branch for the unrestricted source theorem.

Paper origin: references/ldt-paper/ld-pasting.tex:12-55. The paper's large-error reduction names the cases eps, delta, gamma, zeta, d/q ≥ 1; it does not explicitly add 0 < d as a hypothesis of thm:ld-pasting. Thus the Lean theorem should not add 0 < d as an assumption of that cited theorem.

Upstream issue #1622 recorded the need for a direct proof of this degree-zero branch; see docs/paper-gaps/issue-1622-ld-pasting-degree-zero.tex upstream. The nontrivial argument cannot simply be reused: its hBConsistency aggregation passes from distinct sampled heights to independent sampled heights and absorbs the resulting k^2/q loss through the displayed (d/q)^(1/32) term. When d = 0, that term is zero, so the branch requires a separate argument rather than an additional hypothesis on ldPasting.

theorem MIPRE.LIDT.Co.Pasting.ldPastingNontrivialPublicBranch {𝔓 : 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) (hgamma_le : gamma ≤ 1) (hzeta_le : zeta ≤ 1) (hdq_le : params.d ≤ params.q) (hd : 0 < params.d) (family : IdxPolyFamily params 𝔓) (hcomplete : family.Complete strategy.state kappa) (hcons : family.ConsistentWithPoints strategy zeta) (hself : family.StronglySelfConsistent strategy.state zeta) (hbound : IdxPolyFamily.SliceBoundednessInput strategy family zeta) (k : ℕ) (hk_pos : 1 ≤ k) (hk : 400 * params.m * params.d ≤ k) : ∃ (H : Measurement (MIPStarRE.LDT.Polynomial params.next) 𝔓), LdPastingConclusion params strategy family H eps delta gamma kappa zeta k

Projection from the restricted nontrivial construction.

The restricted construction theorem ldPastingNontrivial proves the nontrivial analytic regime for the canonical pasted measurement. This auxiliary statement records the projection from the restricted construction theorem to the conclusion needed by the unrestricted theorem, without changing the statement of thm:ld-pasting.

theorem MIPRE.LIDT.Co.Pasting.ldPasting {𝔓 : 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) (hself : family.StronglySelfConsistent strategy.state zeta) (hbound : IdxPolyFamily.SliceBoundednessInput strategy family zeta) (k : ℕ) (hk : 400 * params.m * params.d ≤ k) : ∃ (H : Measurement (MIPStarRE.LDT.Polynomial params.next) 𝔓), LdPastingConclusion params strategy family H eps delta gamma kappa zeta k

Paper-aligned form of thm:ld-pasting.

Paper origin: references/ldt-paper/ld-pasting.tex, lines 12--50. The following lines 52--55 explain that the proof may restrict to the regime eps, delta, gamma, zeta, d / q ≤ 1, because the complementary cases are trivial. The restricted theorem ldPastingNontrivial proves the nontrivial regime, and the large-gamma, large-zeta, large-d / q, and k = 0 complementary branches are proved above, including the degree-zero case, so this declaration keeps the unrestricted paper statement visible without adding the non-paper assumptions from the restricted theorem.