Section 6 — Pasting Assembly: Successor Assembly

This module contains the final answer-valued pasting invocation, averaged pasting data constructors, and ordinary successor assembly corollaries.

theorem MIPStarRE.LDT.MainInductionStep.answerLdPastingInInductionSectionOfSmallError {ι : 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) : AnswerMainInductionConclusion params.next strategy eps delta gamma k

Answer-valued induction-section pasting theorem for the small-error successor branch.

Paper origin: references/ldt-paper/ld-pasting.tex:12-50 and its use in references/ldt-paper/inductive_step.tex:541-551.

This is a Lean-only answer-valued analogue of the final pasting invocation needed in the simultaneous successor proof. Its hypotheses are the averaged family fields already proved from the recursive answer-valued slices: averaged completeness, consistency with the actual answer-valued point measurement, strong self-consistency, and the boundedness input currently typed through the point-equivalent ordinary carrier. The conclusion is the successor answer-valued main-induction consistency statement.

This proof uses the answer-valued point-commutativity theorem and the Section 11 scalar commutativity chain, so the diagonal-line input is the answer-valued verifier relation itself rather than an ordinary dummy diagonal carrier. It is an internal successor-construction theorem, not the source theorem thm:ld-pasting.

theorem MIPStarRE.LDT.MainInductionStep.answerMainInductionSuccessorNext_ofRecursiveHypothesisAndAnswerPasting {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params.next ι) (eps delta gamma : Error) (k : ℕ) (hgood : strategy.IsGood eps delta gamma) (hinduction : AnswerMainInductionHypothesis params) (hk_next : 400 * params.next.m * params.next.d ≤ k) (hsmall : mainInductionError params.next k eps delta gamma < 1) : AnswerMainInductionConclusion params.next strategy eps delta gamma k

Internal successor reduction from the predecessor answer-valued induction hypothesis and the answer-valued pasting theorem.

Paper origin: references/ldt-paper/inductive_step.tex:441-551.

Conditional: This theorem is not the source successor theorem. It records that, once the recursive predecessor hypothesis is available inside a genuine induction on the dimension, all remaining slice restriction, self-improvement, averaging, and scalar fields reduce the successor branch to answerLdPastingInInductionSectionOfSmallError. It is tracked in issue #1507. Discharge: proved here from the predecessor answer-valued induction hypothesis and the proved answer-valued pasting invocation.

theorem MIPStarRE.LDT.MainInductionStep.AnswerSelfImprovementData.complete_of_slice_bounds {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma : Error) (k : ℕ) (hrestrict : AnswerSliceRestrictionData params strategy eps delta gamma) (hinduction : AnswerPerSliceInductionData params strategy eps delta gamma hrestrict k) (hself : AnswerSelfImprovementData params strategy eps delta gamma k hrestrict hinduction) : hself.family.Complete strategy.state (avgOver (uniformDistribution (Fq params)) hinduction.sliceError + avgOver (uniformDistribution (Fq params)) fun (x : Fq params) => answerSliceSelfImprovementError params hrestrict x)

Averaged completeness of the family obtained from answer-valued self-improvement data.

theorem MIPStarRE.LDT.MainInductionStep.AnswerSelfImprovementData.consistentWithPoints_of_slice_bounds {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma : Error) (k : ℕ) (hgood : strategy.IsGood eps delta gamma) (hrestrict : AnswerSliceRestrictionData params strategy eps delta gamma) (hinduction : AnswerPerSliceInductionData params strategy eps delta gamma hrestrict k) (hself : AnswerSelfImprovementData params strategy eps delta gamma k hrestrict hinduction) : hself.family.ConsistentWithPoints strategy (selfImprovementInInductionError params.next eps delta gamma)

Averaged point-consistency of the family obtained from answer-valued self-improvement data, in the ordinary ambient interface.

theorem MIPStarRE.LDT.MainInductionStep.AnswerSelfImprovementData.stronglySelfConsistent_of_slice_bounds {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma : Error) (k : ℕ) (hgood : strategy.IsGood eps delta gamma) (hrestrict : AnswerSliceRestrictionData params strategy eps delta gamma) (hinduction : AnswerPerSliceInductionData params strategy eps delta gamma hrestrict k) (hself : AnswerSelfImprovementData params strategy eps delta gamma k hrestrict hinduction) : hself.family.StronglySelfConsistent strategy.state (selfImprovementInInductionError params.next eps delta gamma)

Averaged strong self-consistency of the family obtained from answer-valued self-improvement data.

theorem MIPStarRE.LDT.MainInductionStep.AnswerSelfImprovementData.sliceBoundednessInput_of_slice_bounds {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma : Error) (k : ℕ) (hgood : strategy.IsGood eps delta gamma) (hrestrict : AnswerSliceRestrictionData params strategy eps delta gamma) (hinduction : AnswerPerSliceInductionData params strategy eps delta gamma hrestrict k) (hself : AnswerSelfImprovementData params strategy eps delta gamma k hrestrict hinduction) : IdxPolyFamily.SliceBoundednessInput strategy hself.family (selfImprovementInInductionError params.next eps delta gamma)

Averaged boundedness of the family obtained from answer-valued self-improvement data, in the ordinary ambient pasting interface.

Lean-only: This is an internal adapter for the induction-section pasting interface, tracked in issue #1507. Paper origin: references/ldt-paper/inductive_step.tex:461-551. Discharge: proved here by applying idxPolyFamily_sliceBoundednessInput_of_slice_bounds to the answer-valued self-improvement data.

noncomputable def MIPStarRE.LDT.MainInductionStep.assembleAveragedPastingData {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma : Error) (k : ℕ) (hgood : strategy.IsGood eps delta gamma) (hsmall : mainInductionError params.next k eps delta gamma < 1) (hgamma_le : gamma ≤ 1) (hzeta_le : selfImprovementInInductionError params.next eps delta gamma ≤ 1) (hdq_le_q : params.d ≤ params.q) (hrestrict : SliceRestrictionData params strategy eps delta gamma) (hinduction : PerSliceInductionData params strategy eps delta gamma hrestrict k) (hself : SelfImprovementData params strategy eps delta gamma k hrestrict hinduction) (_hk : 400 * params.m * params.d ≤ k) : AveragedPastingData params strategy eps delta gamma k hself

Paper origin: references/ldt-paper/ld-pasting.tex:12-50 (\label{thm:ld-pasting}) and references/ldt-paper/inductive_step.tex:239-342.

The remaining averaged step from per-slice self-improvement data to the pasting hypotheses.

This is where the paper's E_x[σ_x], E_x[ζ_x], and σ* ≤ mainInductionError bookkeeping will eventually live.

Equations

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

noncomputable def MIPStarRE.LDT.MainInductionStep.assembleAveragedPastingDataOfSmallError {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma : Error) (k : ℕ) (hgood : strategy.IsGood eps delta gamma) (hsmall : mainInductionError params.next k eps delta gamma < 1) (hrestrict : SliceRestrictionData params strategy eps delta gamma) (hinduction : PerSliceInductionData params strategy eps delta gamma hrestrict k) (hself : SelfImprovementData params strategy eps delta gamma k hrestrict hinduction) (hk : 400 * params.m * params.d ≤ k) : AveragedPastingData params strategy eps delta gamma k hself

Assemble the averaged pasting data in the nontrivial small-error branch.

Paper origin: references/ldt-paper/inductive_step.tex:486-551. The small-error hypothesis supplies γ ≤ 1, ζ ≤ 1, and d ≤ q, so callers do not carry those scalar estimates as separate proof inputs.

Equations

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

theorem MIPStarRE.LDT.MainInductionStep.mainInductionFromAnswerStageDataOfSmallErrorDirect {ι' : Type uι'} [Fintype ι'] [DecidableEq ι'] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι') (eps delta gamma : Error) (k : ℕ) (hgood : strategy.IsGood eps delta gamma) (hsmall : mainInductionError params.next k eps delta gamma < 1) (answerRestrict : AnswerSliceRestrictionData params strategy eps delta gamma) (answerInduction : AnswerPerSliceInductionData params strategy eps delta gamma answerRestrict k) (answerSelf : AnswerSelfImprovementData params strategy eps delta gamma k answerRestrict answerInduction) (hk : 400 * params.m * params.d ≤ k) : ∃ (H : Measurement (Polynomial params.next) ι'), ConsRel strategy.state (uniformDistribution (Point params.next)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params.next H.toSubMeas) (mainInductionError params.next k eps delta gamma)

Direct answer-valued small-error successor assembly over an ordinary ambient strategy.

This is the same mathematical assembly as mainInductionFromAnswerStageDataOfSmallError, but it invokes the induction-section pasting theorem directly from the answer-valued slice self-improvement data rather than first converting that data into the legacy SelfImprovementData record.

theorem MIPStarRE.LDT.MainInductionStep.mainInductionFromAnswerStageDataOfSmallError {ι' : Type uι'} [Fintype ι'] [DecidableEq ι'] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι') (eps delta gamma : Error) (k : ℕ) (hgood : strategy.IsGood eps delta gamma) (hsmall : mainInductionError params.next k eps delta gamma < 1) (answerRestrict : AnswerSliceRestrictionData params strategy eps delta gamma) (answerInduction : AnswerPerSliceInductionData params strategy eps delta gamma answerRestrict k) (answerSelf : AnswerSelfImprovementData params strategy eps delta gamma k answerRestrict answerInduction) (hk : 400 * params.m * params.d ≤ k) : ∃ (H : Measurement (Polynomial params.next) ι'), ConsRel strategy.state (uniformDistribution (Point params.next)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params.next H.toSubMeas) (mainInductionError params.next k eps delta gamma)

Answer-valued small-error successor assembly.

Paper origin: references/ldt-paper/inductive_step.tex:441-551. This is the internal answer-valued route through the successor proof: answer-valued restricted slice data supply the averaged pasting fields directly, the small-error branch supplies the scalar side conditions for averaged pasting, and the induction-section pasting theorem produces the next-dimensional measurement.