Section 6 — Pasting Assembly: Answer-Valued Fields

This module assembles the answer-valued averaged family fields and the commutativity input used by the pasting theorem.

theorem MIPStarRE.LDT.MainInductionStep.answerSuccessorAveragedFamilyFields_ofMainInductionHypothesis {ι' : 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) : ∃ (family : IdxPolyFamily params ι') (kappa : Error), family.Complete strategy.state kappa ∧ ConsRel strategy.state (uniformDistribution (Point params.next)) strategy.pointMeasurement.toIdxSubMeas family.evaluatedAtNextPoint (selfImprovementInInductionError params.next eps delta gamma) ∧ family.StronglySelfConsistent strategy.state (selfImprovementInInductionError params.next eps delta gamma) ∧ IdxPolyFamily.SliceBoundednessInput (answerSelfImprovementCarrier params.next strategy) family (selfImprovementInInductionError params.next eps delta gamma) ∧ kappa ≤ ↑params.m ^ 2 * (mainInductionNu params.next k eps delta gamma + Real.exp (-(↑k / (80000 * ↑params.m ^ 2)))) + selfImprovementInInductionError params.next eps delta gamma ∧ selfImprovementInInductionError params.next eps delta gamma ≤ mainInductionNu params.next k eps delta gamma

Assemble the averaged polynomial family fields in the answer-valued successor route.

Paper origin: references/ldt-paper/inductive_step.tex:461-551. The statement records exactly the conclusions obtained from the recursive answer-valued slice measurements and the axis-parallel/self-consistency self-improvement theorem: averaged completeness, point consistency with the ambient answer-valued point measurement, strong self-consistency, the slice-boundedness input for the point-equivalent ordinary carrier, and the two scalar estimates for κ and ζ.

Lean-only: The final boundedness field is expressed using answerSelfImprovementCarrier only because the present boundedness interface is typed for ordinary strategies. This theorem does not invoke ldPastingInInductionSection, and does not assert that the carrier's dummy diagonal measurement satisfies the answer-valued diagonal-line test. This internal construction is tracked in issue #1507. Discharge: proved here from the recursive answer-valued slice measurements and the answer-valued self-improvement construction.

theorem MIPStarRE.LDT.MainInductionStep.answerLdPastingInInductionSectionOfComMainAndErrorBound {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params.next ι) (eps delta gamma : Error) (k : ℕ) (hgood : strategy.IsGood eps delta gamma) (family : IdxPolyFamily params ι) (kappa zeta : Error) (hcomplete : family.Complete strategy.state kappa) (hcons : ConsRel strategy.state (uniformDistribution (Point params.next)) strategy.pointMeasurement.toIdxSubMeas family.evaluatedAtNextPoint zeta) (hself : family.StronglySelfConsistent strategy.state zeta) (hbound : IdxPolyFamily.SliceBoundednessInput (answerSelfImprovementCarrier params.next strategy) family zeta) (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) (hk_pos : 1 ≤ k) (hk : 400 * params.m * params.d ≤ k) (hcom : Commutativity.ComMainConclusion params (answerSelfImprovementCarrier params.next strategy) family gamma zeta) (herror_le : ldPastingInInductionError params k eps delta gamma kappa zeta ≤ mainInductionError params.next k eps delta gamma) : AnswerMainInductionConclusion params.next strategy eps delta gamma k

Answer-valued induction-section pasting from an explicit commutativity input.

This theorem performs the checked final assembly once the answer-valued analogue of the Section 11 commutativity theorem has been supplied for the point-equivalent ordinary carrier. The hypotheses hcom and herror_le are not source assumptions; they are the internal commutativity construction and scalar absorption targets for the answer-valued pasting route.

theorem MIPStarRE.LDT.MainInductionStep.answerComMainForCarrier_ofAnswerGood {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params.next ι) (eps delta gamma zeta : Error) (hgood : strategy.IsGood eps delta gamma) (hgamma_nonneg : 0 ≤ gamma) (family : IdxPolyFamily params ι) (hcons : ConsRel strategy.state (uniformDistribution (Point params.next)) strategy.pointMeasurement.toIdxSubMeas family.evaluatedAtNextPoint zeta) (hself : family.StronglySelfConsistent strategy.state zeta) (hbound : IdxPolyFamily.SliceBoundednessInput (answerSelfImprovementCarrier params.next strategy) family zeta) : Commutativity.ComMainConclusion params (answerSelfImprovementCarrier params.next strategy) family gamma zeta

Answer-valued Section 11 commutativity input needed by the positive-degree pasting branch.

This is a Lean-only construction target, not a source theorem and not a hypothesis of thm:main-induction. It is the precise replacement for the invalid route through the ordinary carrier's dummy diagonal measurement: the conclusion is the ordinary ComMainConclusion for the point-equivalent carrier, but the intended proof must use the answer-valued diagonal verifier relation of strategy.

The proof first establishes the Section 10 point-commutativity estimate from the answer-valued diagonal-line test, transfers that estimate to the point-equivalent carrier, and then invokes the Section 11 scalar chain in its form that assumes point commutativity rather than an ordinary diagonal IsGood field.