Section 12 — Statements

This file records the Section 12 pasting conclusions as reusable proposition-valued structures. It gives the displayed error formulas and the statement structures for the switcheroo, completed-family, half-sandwich, recurrence, Chernoff, and final pasting steps.

References

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

noncomputable def MIPStarRE.LDT.Pasting.ldPastingCompletenessLowerBound (params : Parameters) (kappa nu : Error) (k : ℕ) : Error

The final completeness lower bound used in the pasting statements.

Equations

• MIPStarRE.LDT.Pasting.ldPastingCompletenessLowerBound params kappa nu k = 1 - kappa * (1 + 1 / (100 * ↑params.m)) - nu - Real.exp (-(↑k / (80000 * ↑params.m ^ 2)))

noncomputable def MIPStarRE.LDT.Pasting.commutativitySwitcherooError (zeta omega chi : Error) : Error

Displayed error term for lem:commutativity-switcheroo.

Equations

• MIPStarRE.LDT.Pasting.commutativitySwitcherooError zeta omega chi = 6 * Real.rpow zeta (1 / 2) + 6 * Real.rpow omega (1 / 2) + 4 * Real.rpow chi (1 / 2)

noncomputable def MIPStarRE.LDT.Pasting.commutingWithGCompleteError (params : Parameters) (gamma zeta : Error) : Error

Displayed error term for cor:commuting-with-G-complete.

Equations

• MIPStarRE.LDT.Pasting.commutingWithGCompleteError params gamma zeta = 36 * ↑params.m * (Real.rpow gamma (1 / 16) + Real.rpow zeta (1 / 16) + Real.rpow (↑params.d / ↑params.q) (1 / 16))

noncomputable def MIPStarRE.LDT.Pasting.commutingWithGIncompleteError (params : Parameters) (gamma zeta : Error) : Error

Displayed error term for cor:commuting-with-G-incomplete.

Equations

• MIPStarRE.LDT.Pasting.commutingWithGIncompleteError params gamma zeta = MIPStarRE.LDT.Pasting.commutingWithGCompleteError params gamma zeta

noncomputable def MIPStarRE.LDT.Pasting.pairwiseCompletePartCommutationError (params : Parameters) (gamma zeta : Error) : Error

Displayed error term for the pairwise complete-part commutation bound used in cor:G-hat-facts.

This is exactly the upstream thm:com-main error term. The proof of cor:G-hat-facts only weakens the exponent to 1/16 after adding the three incomplete-part commutation contributions.

Equations

• MIPStarRE.LDT.Pasting.pairwiseCompletePartCommutationError params gamma zeta = MIPStarRE.LDT.Commutativity.comMainError params gamma zeta

def MIPStarRE.LDT.Pasting.gHatSelfConsistencyError (zeta : Error) : Error

Displayed self-consistency error for \widehat G.

Equations

• MIPStarRE.LDT.Pasting.gHatSelfConsistencyError zeta = 2 * zeta

noncomputable def MIPStarRE.LDT.Pasting.gHatCommutationError (params : Parameters) (gamma zeta : Error) : Error

Displayed commutation error for \widehat G.

Equations

• MIPStarRE.LDT.Pasting.gHatCommutationError params gamma zeta = 138 * ↑params.m * (Real.rpow gamma (1 / 16) + Real.rpow zeta (1 / 16) + Real.rpow (↑params.d / ↑params.q) (1 / 16))

noncomputable def MIPStarRE.LDT.Pasting.commuteGHalfSandwichError (params : Parameters) (gamma zeta : Error) (k : ℕ) : Error

Displayed error term for commuting past k completed slices.

Equations

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

noncomputable def MIPStarRE.LDT.Pasting.ldSandwichLineOnePointError (params : Parameters) (eps delta gamma zeta : Error) (k : ℕ) : Error

Displayed error term for lem:ld-sandwich-line-one-point.

Equations

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

noncomputable def MIPStarRE.LDT.Pasting.hBConsistencyError (params : Parameters) (eps delta gamma zeta : Error) (k : ℕ) : Error

Displayed error term for lem:h-b-consistency.

Equations

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

noncomputable def MIPStarRE.LDT.Pasting.overAllOutcomesError (params : Parameters) (eps delta gamma zeta : Error) (k : ℕ) : Error

Displayed error term for lem:over-all-outcomes.

Equations

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

noncomputable def MIPStarRE.LDT.Pasting.fromHToGError (params : Parameters) (gamma zeta : Error) (k : ℕ) : Error

Corrected error term for lem:from-H-to-G.

The paper states a linear-in-k ν₈, but its proof first accumulates k · (2√(2ζ) + 2√ν₄(k)); since ν₄(k) already contains k², the commutation contribution is quadratic in k. The Lean statement follows the proof's literal telescope and uses the corrected quadratic bound.

Equations

• MIPStarRE.LDT.Pasting.fromHToGError params gamma zeta k = 46 * ↑k ^ 2 * ↑params.m * (Real.rpow gamma (1 / 32) + Real.rpow zeta (1 / 32) + Real.rpow (↑params.d / ↑params.q) (1 / 32))

noncomputable def MIPStarRE.LDT.Pasting.fromHToGRecurrenceError (params : Parameters) (gamma zeta : Error) (k : ℕ) : Error

The per-step recurrence loss from the proof of lem:from-H-to-G.

Equations

• MIPStarRE.LDT.Pasting.fromHToGRecurrenceError params gamma zeta k = 2 * (2 * zeta).rpow (1 / 2) + 2 * Real.rpow (MIPStarRE.LDT.Pasting.commuteGHalfSandwichError params gamma zeta k) (1 / 2)

noncomputable def MIPStarRE.LDT.Pasting.fromHToGPaperTotalError (params : Parameters) (gamma zeta : Error) (k : ℕ) : Error

Literal telescope error from references/ldt-paper/ld-pasting.tex:1372.

The following paper line drops a factor of k from the commutation contribution; Lean keeps the iterated adjacent-step bound and absorbs it into the corrected quadratic fromHToGError.

Equations

• MIPStarRE.LDT.Pasting.fromHToGPaperTotalError params gamma zeta k = ↑k * MIPStarRE.LDT.Pasting.fromHToGRecurrenceError params gamma zeta k

structure MIPStarRE.LDT.Pasting.LdPastingConclusion {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (H : Measurement (Polynomial params.next) ι) (eps delta gamma kappa zeta : Error) (k : ℕ) : Prop

Paper origin: references/ldt-paper/ld-pasting.tex:12-50 (\label{thm:ld-pasting}), conclusion in \label{item:ld-pasting-N-consistency} (lines 45-49).

Analytic conclusion for thm:ld-pasting once a witness H has been fixed.

The theorem ldPastingNontrivial separately records that the chosen witness is the canonical construction constructedPastedMeasurement params family k, so this structure stores only the quantitative conclusion from the paper.

• pointConsistency : ConsRel strategy.state (uniformDistribution (Point params.next)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params.next H.toSubMeas) (MainInductionStep.ldPastingInInductionError params k eps delta gamma kappa zeta)

structure MIPStarRE.LDT.Pasting.LdPastingSubMeasConclusion {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (H : SubMeas (Polynomial params.next) ι) (eps delta gamma kappa zeta : Error) (k : ℕ) : Prop

Paper origin: references/ldt-paper/ld-pasting.tex:118-131 (\label{lem:ld-pasting-sub-measurement}).

Analytic conclusion for lem:ld-pasting-sub-measurement once a witness H has been fixed.

The theorem ldPastingSubMeas separately records that the chosen witness is the canonical construction constructedPastedSubMeas params family k, so this structure stores only the quantitative properties proved about that witness.

• pointConsistency : ConsRel strategy.state (uniformDistribution (Point params.next)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params.next H) (MainInductionStep.ldPastingInInductionNu params k eps delta gamma zeta)
• completeness : CompletenessAtLeast strategy.state H.liftLeft (ldPastingCompletenessLowerBound params kappa (MainInductionStep.ldPastingInInductionNu params k eps delta gamma zeta) k)

structure MIPStarRE.LDT.Pasting.GCompleteSelfConsistencyStatement {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (zeta : Error) : Prop

Paper origin: references/ldt-paper/ld-pasting.tex:514-536 (\label{lem:g-complete-self-consistency}); the \widehat G rewrite at eq:gselfconall (references/ldt-paper/ld-pasting.tex:821) is the family of self-consistency bounds compared against here.

Lean statement for lem:g-complete-self-consistency. ψbi is the bipartite state on d * d (passed as strategy.state by callers).

• completePartSelfConsistency : SDDRel ψbi (uniformDistribution (SliceQuestion params)) family.meas.toIdxSubMeas.liftLeft family.meas.toIdxSubMeas.liftRight zeta

  Stores self-consistency of the full slice family family.meas because the cor:G-hat-facts decomposition expands \widehat G self-consistency into the original slice-family term plus the incomplete part, not the postprocessed complete-part family.

structure MIPStarRE.LDT.Pasting.GBotSelfConsistencyStatement {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (zeta : Error) : Prop

Paper origin: references/ldt-paper/ld-pasting.tex:537-558 (\label{cor:g-bot-self-consistency}); incomplete-part complement of \label{lem:g-complete-self-consistency} and the eq:gselfconall self-consistency family at line 821.

Lean statement for cor:g-bot-self-consistency.

• incompletePartSelfConsistency : SDDRel ψbi (uniformDistribution (SliceQuestion params)) (incompletePartLeftFamily params family) (incompletePartRightFamily params family) zeta

structure MIPStarRE.LDT.Pasting.CommutativitySwitcherooStatement {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (M : IdxProjSubMeas (Fq params) Outcome ι) (zeta omega chi : Error) : Prop

Paper origin: references/ldt-paper/ld-pasting.tex:560-720 (\label{lem:commutativity-switcheroo}).

Lean statement for lem:commutativity-switcheroo.

• aggregateCommutation : SDDOpRel ψbi (uniformDistribution (SlicePairQuestion params)) (switcherooAggregateLeft params family M) (switcherooAggregateRight params family M) (commutativitySwitcherooError zeta omega chi)

structure MIPStarRE.LDT.Pasting.CommutingWithGCompleteStatement {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (gamma zeta : Error) : Prop

Paper origin: references/ldt-paper/ld-pasting.tex:721-774 (\label{cor:commuting-with-G-complete}).

Lean statement for cor:commuting-with-G-complete.

• pairwiseCompletePartCommutation : SDDOpRel ψbi (uniformDistribution (SlicePairQuestion params)) (fun (q : SlicePairQuestion params) => (CommutativityPoints.orderedProductOpFamily (family.meas q.1).toSubMeas (family.meas q.2).toSubMeas).leftPlacedOpFamily) (fun (q : SlicePairQuestion params) => (CommutativityPoints.reversedProductOpFamily (family.meas q.1).toSubMeas (family.meas q.2).toSubMeas).leftPlacedOpFamily) (pairwiseCompletePartCommutationError params gamma zeta)
• pointWithCompletePartCommutation : SDDOpRel ψbi (uniformDistribution (SlicePairQuestion params)) (completePartPointProductLeft params family) (completePartPointProductRight params family) (commutingWithGCompleteError params gamma zeta)
• completePartCommutation : SDDOpRel ψbi (uniformDistribution (SlicePairQuestion params)) (completePartTotalProductLeft params family) (completePartTotalProductRight params family) (commutingWithGCompleteError params gamma zeta)

structure MIPStarRE.LDT.Pasting.CommutingWithGIncompleteStatement {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (gamma zeta : Error) : Prop

Paper origin: references/ldt-paper/ld-pasting.tex:775-816 (\label{cor:commuting-with-G-incomplete}).

Lean statement for cor:commuting-with-G-incomplete.

• pointWithIncompletePartCommutation : SDDOpRel ψbi (uniformDistribution (SlicePairQuestion params)) (incompletePartPointProductLeft params family) (incompletePartPointProductRight params family) (commutingWithGIncompleteError params gamma zeta)
• incompletePartCommutation : SDDOpRel ψbi (uniformDistribution (SlicePairQuestion params)) (incompletePartTotalProductLeft params family) (incompletePartTotalProductRight params family) (commutingWithGIncompleteError params gamma zeta)

structure MIPStarRE.LDT.Pasting.GHatFactsStatement {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (gamma zeta : Error) : Prop

Paper origin: references/ldt-paper/ld-pasting.tex:817-862 (\label{cor:G-hat-facts}); the displayed \widehat G self-consistency and commutation lines eq:gselfconall and eq:gcomall are at lines 821 and 823.

Lean statement for cor:G-hat-facts.

• completedSelfConsistency : SDDRel ψbi (uniformDistribution (SliceQuestion params)) (gHatSelfConsistencyLeftFamily params family) (gHatSelfConsistencyRightFamily params family) (gHatSelfConsistencyError zeta)
• completedCommutation : SDDOpRel ψbi (uniformDistribution (SlicePairQuestion params)) (gHatPairProductLeft params family) (gHatPairProductRight params family) (gHatCommutationError params gamma zeta)

structure MIPStarRE.LDT.Pasting.CommuteGHalfSandwichStatement {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (gamma zeta : Error) (k : ℕ) : Prop

Paper origin: references/ldt-paper/ld-pasting.tex:872-917 (\label{lem:commute-g-half-sandwich}).

Lean statement for lem:commute-g-half-sandwich.

• repeatedCommutation : SDDOpRel ψbi (uniformDistribution (PointTuple params k)) (gHatHalfSandwichLeft params family k) (gHatHalfSandwichRight params family k) (commuteGHalfSandwichError params gamma zeta k)

structure MIPStarRE.LDT.Pasting.LdSandwichLineOnePointStatement {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (eps delta gamma zeta : Error) (k i : ℕ) : Prop

Paper origin: references/ldt-paper/ld-pasting.tex:918-1040 (\label{lem:ld-sandwich-line-one-point}).

Lean statement for lem:ld-sandwich-line-one-point.

• linePointComparison : ConsRel strategy.state (uniformDistribution (SandwichedLineQuestion params k)) (ldSandwichLineOnePointLeftFamily params strategy family k i) (ldSandwichLineOnePointRightFamily params strategy family k i) (ldSandwichLineOnePointError params eps delta gamma zeta k)

structure MIPStarRE.LDT.Pasting.HBConsistencyStatement {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (eps delta gamma zeta : Error) (k : ℕ) : Prop

Paper origin: references/ldt-paper/ld-pasting.tex:1041-1140 (\label{lem:h-b-consistency}).

Lean statement for lem:h-b-consistency.

• lineConsistency : ConsRel strategy.state (uniformDistribution (VerticalLineQuestion params)) (hRestrictionToVerticalLine params (constructedPastedSubMeas params family k)) (verticalLineMeasurementFamily params strategy) (hBConsistencyError params eps delta gamma zeta k)

noncomputable def MIPStarRE.LDT.Pasting.overAllOutcomesPastedMass {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (k : ℕ) : Error

Scalar expectation of the pasted submeasurement mass appearing on the left-hand side of lem:over-all-outcomes.

Equations

• MIPStarRE.LDT.Pasting.overAllOutcomesPastedMass params strategy family k = MIPStarRE.LDT.subMeasMass strategy.state (MIPStarRE.LDT.Pasting.constructedPastedSubMeas params family k).liftLeft

noncomputable def MIPStarRE.LDT.Pasting.overAllOutcomesExpansionMass {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (k : ℕ) : Error

Scalar expectation of the all-outcomes expansion on the right-hand side of lem:over-all-outcomes.

Equations

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

structure MIPStarRE.LDT.Pasting.OverAllOutcomesStatement {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (eps delta gamma zeta : Error) (k : ℕ) : Prop

Paper origin: references/ldt-paper/ld-pasting.tex:1141-1294 (\label{lem:over-all-outcomes}).

Lean statement for lem:over-all-outcomes.

The paper's displayed statement is a scalar approximation of expectation values, not a stronger ≈_δ relation between already-collapsed Unit-indexed submeasurements. Accordingly, this structure stores only the absolute-value bound between the pasted mass and the all-outcomes expansion mass.

• totalOutcomeExpansion : |overAllOutcomesPastedMass params strategy family k - overAllOutcomesExpansionMass params strategy family k| ≤ overAllOutcomesError params eps delta gamma zeta k

noncomputable def MIPStarRE.LDT.Pasting.fromHToGTailStageMass {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (prefixLen : ℕ) {tailLen : ℕ} (τtail : GHatType tailLen) : Error

Scalar expectation of one per-tail contribution in lem:from-H-to-G.

This is the single-τ_{≥ℓ} term appearing inside the aggregate stage mass from references/ldt-paper/ld-pasting.tex, equation eq:i-think-this-is-what-i'm-supposed-to-prove-2 (lines 1386–1391), and the mirrored blueprint discussion in blueprint/src/chapter/ch09_pasting.tex. The parameter prefixLen is the Lean 0-based stage index. In the ambient k-step recurrence, the remaining tail length is tailLen = k - prefixLen.

Equations

• MIPStarRE.LDT.Pasting.fromHToGTailStageMass params ψbi family prefixLen τtail = MIPStarRE.LDT.ev ψbi (MIPStarRE.LDT.Pasting.fromHToGTailStageFamily params family prefixLen τtail ()).total

noncomputable def MIPStarRE.LDT.Pasting.fromHToGStageMass {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (k ℓ : ℕ) : Error

Scalar expectation of the full Lean stage-ℓ quantity from lem:from-H-to-G.

This is the aggregate quantity displayed in references/ldt-paper/ld-pasting.tex, equation eq:i-think-this-is-what-i'm-supposed-to-prove-2 (lines 1386–1391), and in the matching blueprint section blueprint/src/chapter/ch09_pasting.tex. Lean uses 0-based indexing: stage ℓ here corresponds to the paper's stage ℓ + 1, so the remaining tail has length k - ℓ. Accordingly, this sums over all remaining tail types τ_{≥ℓ} ∈ {0,1}^{k-ℓ}, while the next Lean stage ℓ + 1 sums over the shorter tails τ_{>ℓ}.

Equations

• MIPStarRE.LDT.Pasting.fromHToGStageMass params ψbi family k ℓ = ∑ τtail : MIPStarRE.LDT.Pasting.GHatType (k - ℓ), MIPStarRE.LDT.Pasting.fromHToGTailStageMass params ψbi family ℓ τtail

noncomputable def MIPStarRE.LDT.Pasting.fromHToGAllOutcomesMass {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (k : ℕ) : Error

Scalar expectation of the left-hand side of lem:from-H-to-G, i.e. the uniform average of the eligible pasted-sandwich total mass.

Equations

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

noncomputable def MIPStarRE.LDT.Pasting.fromHToGBernoulliTailMass {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (k : ℕ) : Error

Scalar expectation of the Bernoulli-tail polynomial F(G) on the bipartite state from lem:from-H-to-G.

Equations

• MIPStarRE.LDT.Pasting.fromHToGBernoulliTailMass params ψbi family k = MIPStarRE.LDT.subMeasMass ψbi ((MIPStarRE.LDT.Pasting.bernoulliTailFromFamily params family k).liftRight ())

structure MIPStarRE.LDT.Pasting.FromHToGStatement {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (gamma zeta : Error) (k : ℕ) : Prop

Paper origin: references/ldt-paper/ld-pasting.tex:1295-1670 (\label{lem:from-H-to-G}).

Lean statement for lem:from-H-to-G.

The paper's displayed statement is a scalar approximation of expectation values, not a new ≈_δ relation between submeasurements. Accordingly, this statement stores only the final all-outcomes vs. Bernoulli-tail comparison; the adjacent-stage estimates are recorded by the internal construction lemmas.

• bernoulliPolynomialRewrite : |fromHToGAllOutcomesMass params strategy ψbi family k - fromHToGBernoulliTailMass params ψbi family k| ≤ fromHToGError params gamma zeta k

structure MIPStarRE.LDT.Pasting.ChernoffBernoulliMatrixStatement {ι : Type u_2} [Fintype ι] [DecidableEq ι] (ψ : QuantumState ι) (theta : Error) (k degree : ℕ) (X : Quantum.Op ι) (kappa : Error) (hXpsd : 0 ≤ X) (hXleOne : X ≤ 1) : Prop

Paper origin: references/ldt-paper/ld-pasting.tex:1671-1798 (\label{lem:chernoff-bernoulli-matrix}); the operator-Chernoff inequality is proved by applying continuous functional calculus to the scalar tail polynomial and the scalar Chernoff bound eq:by-chernoff at line 1739.

Lean statement for lem:chernoff-bernoulli-matrix.

• matrixTailBound : CompletenessAtLeast ψ (bernoulliTailSubMeas k degree X hXpsd hXleOne) (1 - kappa / (1 - theta) - Real.exp (-(theta ^ 2 * ↑k) / 2))

structure MIPStarRE.LDT.Pasting.LdPastingNCompletenessStatement {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (kappa nu : Error) (k : ℕ) : Prop

Paper origin: references/ldt-paper/ld-pasting.tex:1799-1849 (\label{cor:ld-pasting-N-completeness}).

Lean statement for cor:ld-pasting-N-completeness.

• completenessBound : CompletenessAtLeast strategy.state (constructedPastedSubMeas params family k).liftLeft (ldPastingCompletenessLowerBound params kappa nu k)