Section 6 — Pasting Assembly: Averaged Family Fields

This module contains the scalar preliminary bound and the averaged family-field lemmas used by the answer-valued successor route.

theorem MIPStarRE.LDT.MainInductionStep.ldPastingInInductionNu_le_fifth_mainInductionNu (params : Parameters) [FieldModel params.q] (eps delta gamma : Error) (k : ℕ) (heps_nonneg : 0 ≤ eps) (hdelta_nonneg : 0 ≤ delta) (hgamma_nonneg : 0 ≤ gamma) (heps_le_one : eps ≤ 1) (hdelta_le_one : delta ≤ 1) (hgamma_le : gamma ≤ 1) (hdq_le_q : params.d ≤ params.q) : ldPastingInInductionNu params k eps delta gamma (selfImprovementInInductionError params.next eps delta gamma) ≤ 1 / 5 * mainInductionNu params.next k eps delta gamma

Paper inductive_step.tex:552-566: in the small-parameter regime, the induction-side ldPastingInInductionNu constructed from ζ = selfImprovementInInductionError is bounded by (1/5) · ν where ν = mainInductionNu. This bound discharges the first factor of the telescoping derivation inside assembleAveragedPastingData.error_le.

theorem MIPStarRE.LDT.MainInductionStep.selfImprovementInInductionError_le_one_of_mainInductionError_lt_one {ι : 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) : selfImprovementInInductionError params.next eps delta gamma ≤ 1

The nontrivial main-induction branch supplies the scalar side condition ζ ≤ 1 needed by the averaged pasting assembly.

Paper origin: references/ldt-paper/inductive_step.tex:486-551, where the small-error branch is the one in which the averaged self-improvement and pasting estimates are used.

theorem MIPStarRE.LDT.MainInductionStep.answer_selfImprovementInInductionError_le_one_of_mainInductionError_lt_one {ι : 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) : selfImprovementInInductionError params.next eps delta gamma ≤ 1

Answer-valued analogue of selfImprovementInInductionError_le_one_of_mainInductionError_lt_one.

This is a scalar consequence of the small-error branch for an ambient answer-valued strategy. It does not use the ordinary carrier strategy and does not assert that the answer-valued diagonal measurement is controlled by an ordinary diagonal test.

theorem MIPStarRE.LDT.MainInductionStep.average_answerSliceSelfImprovementError_le {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma : Error) (hgood : strategy.IsGood eps delta gamma) (hrestrict : AnswerSliceRestrictionData params strategy eps delta gamma) : (avgOver (uniformDistribution (Fq params)) fun (x : Fq params) => answerSliceSelfImprovementError params hrestrict x) ≤ selfImprovementInInductionError params.next eps delta gamma

The average of the answer-slice self-improvement errors is bounded by the ambient induction self-improvement error.

This is the ordinary ambient version: the restricted slices use the answer-valued interface, but the ambient strategy is an ordinary SymStrat.

theorem MIPStarRE.LDT.MainInductionStep.average_answerSliceError_le {ι : 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) : avgOver (uniformDistribution (Fq params)) hinduction.sliceError ≤ ↑params.m ^ 2 * (mainInductionNu params.next k eps delta gamma + Real.exp (-(↑k / (80000 * ↑params.m ^ 2))))

The average recursive answer-slice induction error satisfies the same bound as in the ordinary slice route.

The proof is a transport of the already checked ordinary averaging estimate through the answer-valued slice-to-ordinary data conversion.

theorem MIPStarRE.LDT.MainInductionStep.idxPolyFamily_averagedMass_eq_avg {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψ : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) : subMeasMass ψ family.averagedSubMeas.liftLeft = avgOver (uniformDistribution (Fq params)) fun (x : Fq params) => subMeasMass ψ (family.meas x).liftLeft

The mass of the averaged polynomial family is the average of the masses of the slice measurements.

This is the linearity calculation underlying the completeness part of the averaged pasting assembly.

theorem MIPStarRE.LDT.MainInductionStep.idxPolyFamily_complete_of_slice_bounds {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψ : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (sliceError sliceSelfError : Fq params → Error) (hcomplete : ∀ (x : Fq params), CompletenessAtLeast ψ (family.meas x).liftLeft (1 - sliceError x - sliceSelfError x)) : family.Complete ψ (avgOver (uniformDistribution (Fq params)) sliceError + avgOver (uniformDistribution (Fq params)) sliceSelfError)

Averaged completeness of a slice-indexed polynomial family from pointwise slice completeness.

This is the completeness component of the Section 6 averaging argument. The statement is family-level: it does not mention diagonal measurements, and hence can be reused in the answer-valued successor route.

theorem MIPStarRE.LDT.MainInductionStep.family_pointConsistencyError_eq_avg {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) {eps delta gamma : Error} {k : ℕ} {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) : bipartiteConsError strategy.state (uniformDistribution (Point params.next)) strategy.pointMeasurement.toIdxSubMeas hself.family.evaluatedAtNextPoint = avgOver (uniformDistribution (Fq params)) fun (x : Fq params) => bipartiteConsError strategy.state (uniformDistribution (Point params)) (xRestrictedStrategy params strategy x).pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params (hself.sliceProj x).toSubMeas)

theorem MIPStarRE.LDT.MainInductionStep.family_answerRestrictedPointConsistencyError_eq_avg {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) : bipartiteConsError strategy.state (uniformDistribution (Point params.next)) strategy.pointMeasurement.toIdxSubMeas family.evaluatedAtNextPoint = avgOver (uniformDistribution (Fq params)) fun (x : Fq params) => bipartiteConsError strategy.state (uniformDistribution (Point params)) (xRestrictedAnswerSymStrat params strategy x).pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params (family.meas x).toSubMeas)

Point-consistency averaging for answer-valued restricted slices of an ordinary ambient successor strategy.

theorem MIPStarRE.LDT.MainInductionStep.answer_family_pointConsistencyError_eq_avg {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params.next ι) (family : IdxPolyFamily params ι) : bipartiteConsError strategy.state (uniformDistribution (Point params.next)) strategy.pointMeasurement.toIdxSubMeas family.evaluatedAtNextPoint = avgOver (uniformDistribution (Fq params)) fun (x : Fq params) => bipartiteConsError strategy.state (uniformDistribution (Point params)) (xRestrictedAnswerSymStratOfAnswer params strategy x).pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params (family.meas x).toSubMeas)

Answer-valued point-consistency averaging over the last coordinate.

This is the same Fubini/reindexing calculation as family_pointConsistencyError_eq_avg, but for an ambient answer-valued successor strategy. It is one of the identities needed to assemble the answer-valued successor branch without replacing the diagonal-line answer measurement by an ordinary polynomial-valued one.

theorem MIPStarRE.LDT.MainInductionStep.answer_family_consistency_of_slice_bounds {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params.next ι) (family : IdxPolyFamily params ι) (sliceError : Fq params → Error) (zeta : Error) (hpoint : ∀ (x : Fq params), ConsRel strategy.state (uniformDistribution (Point params)) (xRestrictedAnswerSymStratOfAnswer params strategy x).pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params (family.meas x).toSubMeas) (sliceError x)) (havg : avgOver (uniformDistribution (Fq params)) sliceError ≤ zeta) : ConsRel strategy.state (uniformDistribution (Point params.next)) strategy.pointMeasurement.toIdxSubMeas family.evaluatedAtNextPoint zeta

Average slice-wise point consistency for an answer-valued successor strategy.

If the slice family is point-consistent with each answer-valued restricted strategy at error sliceError x, and the slice errors average to at most zeta, then the evaluated family is point-consistent with the ambient answer-valued point measurement at error zeta.

theorem MIPStarRE.LDT.MainInductionStep.idxPolyFamily_stronglySelfConsistent_of_slice_bounds {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψ : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (sliceError : Fq params → Error) (zeta : Error) (hself : ∀ (x : Fq params), SDDRel ψ (uniformDistribution Unit) (constSubMeasFamily (leftPlacedSubMeas (family.meas x).toSubMeas)) (constSubMeasFamily (rightPlacedSubMeas (family.meas x).toSubMeas)) (sliceError x)) (havg : avgOver (uniformDistribution (Fq params)) sliceError ≤ zeta) : family.StronglySelfConsistent ψ zeta

Average slice-wise left/right closeness into strong self-consistency of the slice-indexed family.

This is the strong self-consistency component of the Section 6 averaging argument. It depends only on the state and the slice measurements, not on the diagonal part of a strategy.

theorem MIPStarRE.LDT.MainInductionStep.idxPolyFamily_sliceBoundednessInput_of_slice_bounds {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (sliceError : Fq params → Error) (zeta : Error) (hbounded : ∀ (x : Fq params), tensorFailureExpectation strategy.state (family.witness x) (family.meas x).toSubMeas ≤ sliceError x) (havg : avgOver (uniformDistribution (Fq params)) sliceError ≤ zeta) (hdom : ∀ (x : Fq params) (g : Polynomial params), IdxPolyFamily.averagedSlicePointEvaluationOperator strategy x g ≤ family.witness x) : IdxPolyFamily.SliceBoundednessInput strategy family zeta

Average slice-wise boundedness into the boundedness input used by the induction-section pasting theorem.

This is the boundedness component of the Section 6 averaging argument for an ordinary successor strategy. The hypotheses are exactly the slice-wise residual estimate and the paper domination condition E_u A^{u,x}_{g(u)} <= Z^x.

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 averaging the slice-wise boundedness estimates and the domination condition.