Section 6 — Pasting Assembly: Error Bounds

This module contains the scalar absorption and degree-zero answer-valued pasting constructions for the small-error branch.

theorem MIPStarRE.LDT.MainInductionStep.ldPastingInInductionError_le_mainInductionError_of_bounds (params : Parameters) [FieldModel params.q] (eps delta gamma : Error) (k : ℕ) (kappa zeta : Error) (heps_nonneg : 0 ≤ eps) (hdelta_nonneg : 0 ≤ delta) (hgamma_nonneg : 0 ≤ gamma) (hkappa_le : kappa ≤ ↑params.m ^ 2 * (mainInductionNu params.next k eps delta gamma + Real.exp (-(↑k / (80000 * ↑params.m ^ 2)))) + zeta) (hzeta_le_nu : zeta ≤ mainInductionNu params.next k eps delta gamma) (hnu_le : ldPastingInInductionNu params k eps delta gamma zeta ≤ 1 / 5 * mainInductionNu params.next k eps delta gamma) : ldPastingInInductionError params k eps delta gamma kappa zeta ≤ mainInductionError params.next k eps delta gamma

Scalar telescoping from the induction-section pasting error to the next main-induction error.

The lemma isolates the scalar inequality chain from the assembly of the averaged slice data: the bound on κ, the comparison ζ ≤ ν, and the bound on the pasting-section ν term.

theorem MIPStarRE.LDT.MainInductionStep.answerLdPastingInInductionError_le_mainInductionError_of_smallError {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params.next ι) (eps delta gamma kappa : Error) (k : ℕ) (hgood : strategy.IsGood eps delta gamma) (hsmall : mainInductionError params.next k eps delta gamma < 1) (hkappa_le : kappa ≤ ↑params.m ^ 2 * (mainInductionNu params.next k eps delta gamma + Real.exp (-(↑k / (80000 * ↑params.m ^ 2)))) + selfImprovementInInductionError params.next eps delta gamma) (hzeta_le_nu : selfImprovementInInductionError params.next eps delta gamma ≤ mainInductionNu params.next k eps delta gamma) : ldPastingInInductionError params k eps delta gamma kappa (selfImprovementInInductionError params.next eps delta gamma) ≤ mainInductionError params.next k eps delta gamma

Scalar absorption for the answer-valued pasting route.

This is the answer-valued counterpart of ldPastingInInductionError_le_mainInductionError_of_bounds. Its proof uses only the answer-valued scalar consequences of the small-error hypothesis; it does not pass through the ordinary carrier strategy.

theorem MIPStarRE.LDT.MainInductionStep.answerLdPastingInInductionSectionDegreeZeroOfSmallError {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params.next ι) (eps delta gamma : Error) (k : ℕ) (hgood : strategy.IsGood eps delta gamma) (hsmall : mainInductionError params.next k eps delta gamma < 1) (family : IdxPolyFamily params ι) (kappa : Error) (hcomplete : family.Complete strategy.state kappa) (hcons : ConsRel strategy.state (uniformDistribution (Point params.next)) strategy.pointMeasurement.toIdxSubMeas family.evaluatedAtNextPoint (selfImprovementInInductionError params.next eps delta gamma)) (_hself : family.StronglySelfConsistent strategy.state (selfImprovementInInductionError params.next eps delta gamma)) (_hbound : IdxPolyFamily.SliceBoundednessInput (answerSelfImprovementCarrier params.next strategy) family (selfImprovementInInductionError params.next eps delta gamma)) (hkappa_le : kappa ≤ ↑params.m ^ 2 * (mainInductionNu params.next k eps delta gamma + Real.exp (-(↑k / (80000 * ↑params.m ^ 2)))) + selfImprovementInInductionError params.next eps delta gamma) (hzeta_le_nu : selfImprovementInInductionError params.next eps delta gamma ≤ mainInductionNu params.next k eps delta gamma) (_hk : 400 * params.m * params.d ≤ k) (hd_zero : params.d = 0) : AnswerMainInductionConclusion params.next strategy eps delta gamma k

Degree-zero answer-valued pasting construction for the small-error successor branch.

This is the complementary case to the positive-degree branch handled by answerLdPastingInInductionSectionOfComMainAndErrorBound. The proof applies the axis/self-consistency form of the degree-zero pasting construction to the point-equivalent carrier and then uses the answer-valued scalar absorption estimate. It does not use the carrier's dummy ordinary diagonal measurement.

Paper location: the pasting invocation in references/ldt-paper/inductive_step.tex:541-551; this is the d = 0 complementary branch of the low-degree pasting theorem.