Section 6 — Induction Step Data

This file records the intermediate conclusion structures and bookkeeping statements used in the induction step. It contains the conclusions of the induction-level self-improvement and pasting theorems, together with restricted failure profiles and the stage data for the paper's slice restriction, slice-wise induction, self-improvement, and pasting assembly.

References

• blueprint/src/chapter/ch10_induction.tex
• references/ldt-paper/inductive_step.tex

structure MIPStarRE.LDT.MainInductionStep.SelfImprovementInInductionSectionConclusion {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (_G : SubMeas (Polynomial params) ι) (H : ProjSubMeas (Polynomial params) ι) (Z : Quantum.Op ι) (eps delta gamma nu : Error) : Prop

Paper origin: references/ldt-paper/inductive_step.tex:249-286 (\label{thm:self-improvement-in-induction-section}).

Conclusion of the induction-level self-improvement theorem.

The strategy's state is bipartite (QuantumState (ι × ι)). Fields that involve bipartite-lifted operators use leftPlacedSubMeas / rightPlacedSubMeas / tensorFailureExpectation with honest bipartite structure.

• completeness : CompletenessAtLeast strategy.state H.liftLeft (1 - nu - selfImprovementInInductionError params eps delta gamma)

  The projective submeasurement remains almost complete.

• pointConsistency : ConsRel strategy.state (uniformDistribution (Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params H.toSubMeas) (selfImprovementInInductionError params eps delta gamma)

  The projective submeasurement stays point-consistent with the original strategy.

• strongSelfConsistency : BipartiteSSCRel strategy.state (uniformDistribution Unit) (constSubMeasFamily H.toSubMeas) (selfImprovementInInductionError params eps delta gamma)

  The output family is strongly self-consistent in the bipartite sense.

• selfCloseness : SDDRel strategy.state (uniformDistribution Unit) (constSubMeasFamily (leftPlacedSubMeas H.toSubMeas)) (constSubMeasFamily (rightPlacedSubMeas H.toSubMeas)) (selfImprovementInInductionError params eps delta gamma)

  The left and right placements of the output family stay close in squared distance.

• bounded : tensorFailureExpectation strategy.state Z H.toSubMeas ≤ selfImprovementInInductionError params eps delta gamma

  The dual witness Z controls the tensor failure expectation of H.

• dominatesAveragePointOperator (h : Polynomial params) : IdxPolyFamily.averagedPointEvaluationOperator strategy h ≤ Z

  Every averaged point-evaluation operator is dominated by the dual witness Z.

structure MIPStarRE.LDT.MainInductionStep.LdPastingInInductionSectionConclusion {ι : 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/inductive_step.tex:299-338 (\label{thm:ld-pasting-in-induction-section}).

Conclusion of the section-local pasting theorem.

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

  The pasted measurement is point-consistent with the ambient strategy.

structure MIPStarRE.LDT.MainInductionStep.RestrictedFailureProfile {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) : Type

Bookkeeping data x ↦ (ε_x, δ_x, γ_x) for the restricted strategies.

• axisParallel : Fq params → Error

  The axis-parallel failure bound attached to each slice height.

• selfConsistency : Fq params → Error

  The self-consistency failure bound attached to each slice height.

• diagonal : Fq params → Error

  The diagonal-line failure bound attached to each slice height.

• restrictedGood (x : Fq params) : (xRestrictedStrategy params strategy x).IsGood (self.axisParallel x) (self.selfConsistency x) (self.diagonal x)

  Each slice-restricted strategy is good with the recorded parameters.

structure MIPStarRE.LDT.MainInductionStep.AnswerRestrictedFailureProfile {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) : Type

Bookkeeping data for answer-valued restricted strategies.

This is the function-answer analogue of RestrictedFailureProfile: each slice is the restricted strategy interface from inductive_step.tex, lines 436--455.

• axisParallel : Fq params → Error

  The axis-parallel failure bound attached to each slice height.

• selfConsistency : Fq params → Error

  The self-consistency failure bound attached to each slice height.

• diagonal : Fq params → Error

  The diagonal-line failure bound attached to each slice height.

• restrictedGood (x : Fq params) : (xRestrictedAnswerSymStrat params strategy x).IsGood (self.axisParallel x) (self.selfConsistency x) (self.diagonal x)

  Each answer-valued slice-restricted strategy is good with the recorded parameters.

noncomputable def MIPStarRE.LDT.MainInductionStep.averageRestrictedAxisParallelError {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] {strategy : SymStrat params.next ι} (profile : RestrictedFailureProfile params strategy) : Error

Average restricted axis-parallel error over slices.

Equations

• MIPStarRE.LDT.MainInductionStep.averageRestrictedAxisParallelError params profile = MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Fq params)) profile.axisParallel

noncomputable def MIPStarRE.LDT.MainInductionStep.averageRestrictedSelfConsistencyError {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] {strategy : SymStrat params.next ι} (profile : RestrictedFailureProfile params strategy) : Error

Average restricted self-consistency error over slices.

Equations

• MIPStarRE.LDT.MainInductionStep.averageRestrictedSelfConsistencyError params profile = MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Fq params)) profile.selfConsistency

noncomputable def MIPStarRE.LDT.MainInductionStep.averageRestrictedDiagonalError {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] {strategy : SymStrat params.next ι} (profile : RestrictedFailureProfile params strategy) : Error

Average restricted diagonal-line error over slices.

Equations

• MIPStarRE.LDT.MainInductionStep.averageRestrictedDiagonalError params profile = MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Fq params)) profile.diagonal

noncomputable def MIPStarRE.LDT.MainInductionStep.averageAnswerRestrictedAxisParallelError {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] {strategy : SymStrat params.next ι} (profile : AnswerRestrictedFailureProfile params strategy) : Error

Average restricted axis-parallel error over answer-valued slices.

Equations

• MIPStarRE.LDT.MainInductionStep.averageAnswerRestrictedAxisParallelError params profile = MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Fq params)) profile.axisParallel

noncomputable def MIPStarRE.LDT.MainInductionStep.averageAnswerRestrictedSelfConsistencyError {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] {strategy : SymStrat params.next ι} (profile : AnswerRestrictedFailureProfile params strategy) : Error

Average restricted self-consistency error over answer-valued slices.

Equations

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

noncomputable def MIPStarRE.LDT.MainInductionStep.averageAnswerRestrictedDiagonalError {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] {strategy : SymStrat params.next ι} (profile : AnswerRestrictedFailureProfile params strategy) : Error

Average restricted diagonal-line error over answer-valued slices.

Equations

• MIPStarRE.LDT.MainInductionStep.averageAnswerRestrictedDiagonalError params profile = MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Fq params)) profile.diagonal

structure MIPStarRE.LDT.MainInductionStep.RestrictedProbabilitiesStatement {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma : Error) : Prop

Paper origin: references/ldt-paper/inductive_step.tex:374-412 (\label{lem:restricted-probabilities}).

Bookkeeping data for the restricted-probabilities lemma.

This records a slice-wise error profile together with the three averaged bounds that appear in the paper: the axis-parallel and diagonal branches both incur the same conditioning loss ((m + 1) / m), while the self-consistency branch restricts exactly.

• profileExists : ∃ (profile : RestrictedFailureProfile params strategy), averageRestrictedAxisParallelError params profile ≤ sliceConditioningLoss params * eps ∧ averageRestrictedSelfConsistencyError params profile ≤ delta ∧ averageRestrictedDiagonalError params profile ≤ sliceConditioningLoss params * gamma

  There is a slice-wise error profile realizing the three averaged restricted bounds.

structure MIPStarRE.LDT.MainInductionStep.AnswerRestrictedProbabilitiesStatement {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma : Error) : Prop

Paper origin: references/ldt-paper/inductive_step.tex:374-412 (\label{lem:restricted-probabilities}); answer-valued variant carrying the same axis-parallel/self-consistency/diagonal restriction bounds for the answer-restricted slice profile. This is an answer-valued variant of RestrictedProbabilitiesStatement against xRestrictedAnswerSymStrat rather than xRestrictedStrategy; no separate paper anchor exists for the answer-valued variant.

Bookkeeping data for the answer-valued restricted-probabilities lemma.

• profileExists : ∃ (profile : AnswerRestrictedFailureProfile params strategy), averageAnswerRestrictedAxisParallelError params profile ≤ sliceConditioningLoss params * eps ∧ averageAnswerRestrictedSelfConsistencyError params profile ≤ delta ∧ averageAnswerRestrictedDiagonalError params profile ≤ sliceConditioningLoss params * gamma

  There is a slice-wise answer-valued error profile realizing the three averaged bounds.

structure MIPStarRE.LDT.MainInductionStep.SliceRestrictionData {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma : Error) : Type

Bookkeeping data for the slice-restriction step of thm:main-induction.

Paper origin: references/ldt-paper/inductive_step.tex:374-412 (\label{lem:restricted-probabilities}) and references/ldt-paper/inductive_step.tex:441-454.

This records an explicit restricted failure profile together with the averaged bounds extracted from lem:restricted-probabilities.

• profile : RestrictedFailureProfile params strategy

  Slice-wise failure profile x ↦ (ε_x, δ_x, γ_x).

• axisAverageBound : averageRestrictedAxisParallelError params self.profile ≤ sliceConditioningLoss params * eps

  Averaged axis-parallel slice error bound.

• selfAverageBound : averageRestrictedSelfConsistencyError params self.profile ≤ delta

  Averaged self-consistency slice error bound.

• diagonalAverageBound : averageRestrictedDiagonalError params self.profile ≤ sliceConditioningLoss params * gamma

  Averaged diagonal slice error bound.

structure MIPStarRE.LDT.MainInductionStep.AnswerSliceRestrictionData {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma : Error) : Type

Answer-valued slice-restriction data record for the Section 6 induction step.

Paper origin: references/ldt-paper/inductive_step.tex:374-412 (\label{lem:restricted-probabilities}) and the recursive slice application in references/ldt-paper/inductive_step.tex:441-454.

• profile : AnswerRestrictedFailureProfile params strategy

  Slice-wise failure profile for the answer-valued restricted strategies.

• axisAverageBound : averageAnswerRestrictedAxisParallelError params self.profile ≤ sliceConditioningLoss params * eps

  Averaged axis-parallel slice error bound.

• selfAverageBound : averageAnswerRestrictedSelfConsistencyError params self.profile ≤ delta

  Averaged self-consistency slice error bound.

• diagonalAverageBound : averageAnswerRestrictedDiagonalError params self.profile ≤ sliceConditioningLoss params * gamma

  Averaged diagonal slice error bound.

structure MIPStarRE.LDT.MainInductionStep.PerSliceInductionData {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma : Error) (restrictionPkg : SliceRestrictionData params strategy eps delta gamma) (k : ℕ) : Type (max u_1 u_2)

Explicit per-slice output of the inductive hypothesis.

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

This is the recursion-entry data: given slice-restriction data, a proof of thm:main-induction in dimension m is expected to produce a measurement G^x for every slice height x.

• sliceError : Fq params → Error

  Slice-wise inductive error σ_x.

• sliceMeasurement : Fq params → Measurement (Polynomial params) ι

  Slice-wise inductive measurement G^x.

• pointConsistency (x : Fq params) : ConsRel strategy.state (uniformDistribution (Point params)) (xRestrictedStrategy params strategy x).pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params (self.sliceMeasurement x).toSubMeas) (self.sliceError x)

  Each G^x satisfies the dimension-m point-consistency conclusion.

• error_le (x : Fq params) : self.sliceError x ≤ mainInductionError params k (restrictionPkg.profile.axisParallel x) (restrictionPkg.profile.selfConsistency x) (restrictionPkg.profile.diagonal x)

  The slice-wise error is bounded by the dimension-m induction target.

structure MIPStarRE.LDT.MainInductionStep.AnswerPerSliceInductionData {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma : Error) (restrictionPkg : AnswerSliceRestrictionData params strategy eps delta gamma) (k : ℕ) : Type (max u_1 u_2)

Explicit per-slice output of the inductive hypothesis for answer-valued slices.

Paper origin: references/ldt-paper/inductive_step.tex:441-454; answer-valued restriction interface for the same recursive call.

This is the function-answer recursion-entry data record: the recursive call is made on xRestrictedAnswerSymStrat, whose diagonal answers retain the whole restricted function instead of only its value at the base point.

• sliceError : Fq params → Error

  Slice-wise inductive error σ_x.

• sliceMeasurement : Fq params → Measurement (Polynomial params) ι

  Slice-wise inductive measurement G^x.

• pointConsistency (x : Fq params) : ConsRel strategy.state (uniformDistribution (Point params)) (xRestrictedAnswerSymStrat params strategy x).pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params (self.sliceMeasurement x).toSubMeas) (self.sliceError x)

  Each G^x satisfies the dimension-m point-consistency conclusion.

• error_le (x : Fq params) : self.sliceError x ≤ mainInductionError params k (restrictionPkg.profile.axisParallel x) (restrictionPkg.profile.selfConsistency x) (restrictionPkg.profile.diagonal x)

  The slice-wise error is bounded by the dimension-m induction target.

def MIPStarRE.LDT.MainInductionStep.AnswerMainInductionConclusion {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params ι) (eps delta gamma : Error) (k : ℕ) : Prop

Paper origin: references/ldt-paper/inductive_step.tex:7-18 (\label{thm:main-induction}); answer-valued analogue.

Main-induction conclusion for a function-answer symmetric strategy.

This is the answer-valued analogue of the conclusion of thm:main-induction. It is used as the explicit predecessor induction hypothesis for the paper-faithful answer-valued restriction route: for a strategy in dimension m, it supplies a global polynomial measurement consistent with the point measurement at the Section 6 error mainInductionError.

Equations

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

def MIPStarRE.LDT.MainInductionStep.AnswerMainInductionHypothesis (params : Parameters) [FieldModel params.q] : Prop

Predicate form of the answer-valued predecessor main-induction hypothesis.

This is a Lean-only interface for the induction step in references/ldt-paper/inductive_step.tex:441-454. It is deliberately stated at mainInductionError strength and for AnswerSymStrat, so callers can instantiate the paper-faithful xRestrictedAnswerSymStrat slices without appealing to the public Test.mainFormal theorem.

The explicit .{u,v} universe binder decouples the universe of FieldModel's carrier K : Type u from the universe of the dimension index ι : Type v. Without this separation, a proof that instantiates FieldModel.{0} (as many Test.MainTheorem applications do) would also force ι to Type 0, making it impossible to apply the hypothesis to the role-register space Role × ι when the index universe exceeds 0.

Equations

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

noncomputable def MIPStarRE.LDT.MainInductionStep.sliceSelfImprovementError {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] {strategy : SymStrat params.next ι} {eps delta gamma : Error} (restrictionPkg : SliceRestrictionData params strategy eps delta gamma) (x : Fq params) : Error

The slice-local self-improvement error ζ_x.

Equations

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

noncomputable def MIPStarRE.LDT.MainInductionStep.answerSliceSelfImprovementError {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] {strategy : SymStrat params.next ι} {eps delta gamma : Error} (restrictionPkg : AnswerSliceRestrictionData params strategy eps delta gamma) (x : Fq params) : Error

The slice-local self-improvement error ζ_x for answer-valued slices.

Equations

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

structure MIPStarRE.LDT.MainInductionStep.SelfImprovementData {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma : Error) (k : ℕ) (restrictionPkg : SliceRestrictionData params strategy eps delta gamma) (inductionPkg : PerSliceInductionData params strategy eps delta gamma restrictionPkg k) : Type (max u_1 u_2)

Slice-wise output of the induction-level self-improvement stage.

Paper origin: references/ldt-paper/inductive_step.tex:461-551 (\label{thm:self-improvement-in-induction-section} in use inside the proof of \label{thm:main-induction}).

Because xRestrictedStrategy is a section-local restricted strategy rather than literally a SymStrat params interface—it does not carry the ambient permInvState witness, the diagonal reparametrization-invariance field, or the downstream role-symmetrization API—this data records directly the four paper-faithful properties that will later be averaged into the pasting inputs.

• sliceProj : Fq params → ProjSubMeas (Polynomial params) ι

  Slice-wise projective submeasurement Ĝ^x.

• sliceWitness : Fq params → Quantum.Op ι

  Slice-wise PSD witness Z^x.

• completeness (x : Fq params) : CompletenessAtLeast strategy.state (self.sliceProj x).liftLeft (1 - inductionPkg.sliceError x - sliceSelfImprovementError params restrictionPkg x)

  Slice-wise completeness bound.

• pointConsistency (x : Fq params) : ConsRel strategy.state (uniformDistribution (Point params)) (xRestrictedStrategy params strategy x).pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params (self.sliceProj x).toSubMeas) (sliceSelfImprovementError params restrictionPkg x)

  Slice-wise consistency with the restricted point measurement.

• strongSelfConsistency (x : Fq params) : BipartiteSSCRel strategy.state (uniformDistribution Unit) (constSubMeasFamily (self.sliceProj x).toSubMeas) (sliceSelfImprovementError params restrictionPkg x)

  Slice-wise strong self-consistency.

• selfCloseness (x : Fq params) : SDDRel strategy.state (uniformDistribution Unit) (constSubMeasFamily (leftPlacedSubMeas (self.sliceProj x).toSubMeas)) (constSubMeasFamily (rightPlacedSubMeas (self.sliceProj x).toSubMeas)) (sliceSelfImprovementError params restrictionPkg x)

  Slice-wise left/right closeness needed for the averaged self-consistency input.

• bounded (x : Fq params) : tensorFailureExpectation strategy.state (self.sliceWitness x) (self.sliceProj x).toSubMeas ≤ sliceSelfImprovementError params restrictionPkg x

  Slice-wise boundedness residual.

• dominatesAveragePointOperator (x : Fq params) (h : Polynomial params) : IdxPolyFamily.averagedSlicePointEvaluationOperator strategy x h ≤ self.sliceWitness x

  Slice-wise domination of the averaged point operator.

noncomputable def MIPStarRE.LDT.MainInductionStep.SelfImprovementData.family {ι : Type u_1} [Fintype ι] [DecidableEq ι] {params : Parameters} [FieldModel params.q] {strategy : SymStrat params.next ι} {eps delta gamma : Error} {k : ℕ} {restrictionPkg : SliceRestrictionData params strategy eps delta gamma} {inductionPkg : PerSliceInductionData params strategy eps delta gamma restrictionPkg k} (pkg : SelfImprovementData params strategy eps delta gamma k restrictionPkg inductionPkg) : IdxPolyFamily params ι

The slice-indexed polynomial family obtained by collecting the improved slice measurements Ĝ^x together with the slice-wise witnesses Z^x.

Equations

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

@[simp]

theorem MIPStarRE.LDT.MainInductionStep.SelfImprovementData.family_meas {ι : Type u_1} [Fintype ι] [DecidableEq ι] {params : Parameters} [FieldModel params.q] {strategy : SymStrat params.next ι} {eps delta gamma : Error} {k : ℕ} {restrictionPkg : SliceRestrictionData params strategy eps delta gamma} {inductionPkg : PerSliceInductionData params strategy eps delta gamma restrictionPkg k} (pkg : SelfImprovementData params strategy eps delta gamma k restrictionPkg inductionPkg) : pkg.family.meas = pkg.sliceProj

@[simp]

theorem MIPStarRE.LDT.MainInductionStep.SelfImprovementData.family_witness {ι : Type u_1} [Fintype ι] [DecidableEq ι] {params : Parameters} [FieldModel params.q] {strategy : SymStrat params.next ι} {eps delta gamma : Error} {k : ℕ} {restrictionPkg : SliceRestrictionData params strategy eps delta gamma} {inductionPkg : PerSliceInductionData params strategy eps delta gamma restrictionPkg k} (pkg : SelfImprovementData params strategy eps delta gamma k restrictionPkg inductionPkg) (x : Fq params) : pkg.family.witness x = pkg.sliceWitness x

@[simp]

theorem MIPStarRE.LDT.MainInductionStep.SelfImprovementData.family_dominationTarget {ι : Type u_1} [Fintype ι] [DecidableEq ι] {params : Parameters} [FieldModel params.q] {strategy : SymStrat params.next ι} {eps delta gamma : Error} {k : ℕ} {restrictionPkg : SliceRestrictionData params strategy eps delta gamma} {inductionPkg : PerSliceInductionData params strategy eps delta gamma restrictionPkg k} (pkg : SelfImprovementData params strategy eps delta gamma k restrictionPkg inductionPkg) (x : Fq params) (g : Polynomial params) : pkg.family.dominationTarget x g = IdxPolyFamily.averagedSlicePointEvaluationOperator strategy x g

structure MIPStarRE.LDT.MainInductionStep.AnswerSelfImprovementData {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma : Error) (k : ℕ) (restrictionPkg : AnswerSliceRestrictionData params strategy eps delta gamma) (inductionPkg : AnswerPerSliceInductionData params strategy eps delta gamma restrictionPkg k) : Type (max u_1 u_2)

Slice-wise output of the induction-level self-improvement stage for answer-valued restricted strategies.

Paper origin: references/ldt-paper/inductive_step.tex:461-551; answer-valued restriction interface for the same self-improvement stage.

This mirrors SelfImprovementData, but its point-consistency field is stated against xRestrictedAnswerSymStrat, the function-answer restricted strategy.

• sliceProj : Fq params → ProjSubMeas (Polynomial params) ι

  Slice-wise projective submeasurement Ĝ^x.

• sliceWitness : Fq params → Quantum.Op ι

  Slice-wise PSD witness Z^x.

• completeness (x : Fq params) : CompletenessAtLeast strategy.state (self.sliceProj x).liftLeft (1 - inductionPkg.sliceError x - answerSliceSelfImprovementError params restrictionPkg x)

  Slice-wise completeness bound.

• pointConsistency (x : Fq params) : ConsRel strategy.state (uniformDistribution (Point params)) (xRestrictedAnswerSymStrat params strategy x).pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params (self.sliceProj x).toSubMeas) (answerSliceSelfImprovementError params restrictionPkg x)

  Slice-wise consistency with the answer-valued restricted point measurement.

• strongSelfConsistency (x : Fq params) : BipartiteSSCRel strategy.state (uniformDistribution Unit) (constSubMeasFamily (self.sliceProj x).toSubMeas) (answerSliceSelfImprovementError params restrictionPkg x)

  Slice-wise strong self-consistency.

• selfCloseness (x : Fq params) : SDDRel strategy.state (uniformDistribution Unit) (constSubMeasFamily (leftPlacedSubMeas (self.sliceProj x).toSubMeas)) (constSubMeasFamily (rightPlacedSubMeas (self.sliceProj x).toSubMeas)) (answerSliceSelfImprovementError params restrictionPkg x)

  Slice-wise left/right closeness needed for the averaged self-consistency data record.

• bounded (x : Fq params) : tensorFailureExpectation strategy.state (self.sliceWitness x) (self.sliceProj x).toSubMeas ≤ answerSliceSelfImprovementError params restrictionPkg x

  Slice-wise boundedness residual.

• dominatesAveragePointOperator (x : Fq params) (h : Polynomial params) : IdxPolyFamily.averagedSlicePointEvaluationOperator strategy x h ≤ self.sliceWitness x

  Slice-wise domination of the averaged point operator.

noncomputable def MIPStarRE.LDT.MainInductionStep.AnswerSelfImprovementData.family {ι : Type u_1} [Fintype ι] [DecidableEq ι] {params : Parameters} [FieldModel params.q] {strategy : SymStrat params.next ι} {eps delta gamma : Error} {k : ℕ} {restrictionPkg : AnswerSliceRestrictionData params strategy eps delta gamma} {inductionPkg : AnswerPerSliceInductionData params strategy eps delta gamma restrictionPkg k} (pkg : AnswerSelfImprovementData params strategy eps delta gamma k restrictionPkg inductionPkg) : IdxPolyFamily params ι

The slice-indexed polynomial family obtained from answer-valued restricted self-improvement outputs.

Equations

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

@[simp]

theorem MIPStarRE.LDT.MainInductionStep.AnswerSelfImprovementData.family_meas {ι : Type u_1} [Fintype ι] [DecidableEq ι] {params : Parameters} [FieldModel params.q] {strategy : SymStrat params.next ι} {eps delta gamma : Error} {k : ℕ} {restrictionPkg : AnswerSliceRestrictionData params strategy eps delta gamma} {inductionPkg : AnswerPerSliceInductionData params strategy eps delta gamma restrictionPkg k} (pkg : AnswerSelfImprovementData params strategy eps delta gamma k restrictionPkg inductionPkg) : pkg.family.meas = pkg.sliceProj

@[simp]

theorem MIPStarRE.LDT.MainInductionStep.AnswerSelfImprovementData.family_witness {ι : Type u_1} [Fintype ι] [DecidableEq ι] {params : Parameters} [FieldModel params.q] {strategy : SymStrat params.next ι} {eps delta gamma : Error} {k : ℕ} {restrictionPkg : AnswerSliceRestrictionData params strategy eps delta gamma} {inductionPkg : AnswerPerSliceInductionData params strategy eps delta gamma restrictionPkg k} (pkg : AnswerSelfImprovementData params strategy eps delta gamma k restrictionPkg inductionPkg) (x : Fq params) : pkg.family.witness x = pkg.sliceWitness x

@[simp]

theorem MIPStarRE.LDT.MainInductionStep.AnswerSelfImprovementData.family_dominationTarget {ι : Type u_1} [Fintype ι] [DecidableEq ι] {params : Parameters} [FieldModel params.q] {strategy : SymStrat params.next ι} {eps delta gamma : Error} {k : ℕ} {restrictionPkg : AnswerSliceRestrictionData params strategy eps delta gamma} {inductionPkg : AnswerPerSliceInductionData params strategy eps delta gamma restrictionPkg k} (pkg : AnswerSelfImprovementData params strategy eps delta gamma k restrictionPkg inductionPkg) (x : Fq params) (g : Polynomial params) : pkg.family.dominationTarget x g = IdxPolyFamily.averagedSlicePointEvaluationOperator strategy x g

structure MIPStarRE.LDT.MainInductionStep.AveragedPastingData {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma : Error) (k : ℕ) {restrictionPkg : SliceRestrictionData params strategy eps delta gamma} {inductionPkg : PerSliceInductionData params strategy eps delta gamma restrictionPkg k} (selfPkg : SelfImprovementData params strategy eps delta gamma k restrictionPkg inductionPkg) : Type

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

Averaged pasting inputs distilled from the per-slice self-improvement data.

This records exactly the hypotheses needed to invoke thm:ld-pasting-in-induction-section after the slice-wise self-improvement outputs have been averaged.

• kappa : Error

  Averaged completeness parameter κ.

• zeta : Error

  Averaged self-improvement / pasting interface parameter ζ.

• complete : selfPkg.family.Complete strategy.state self.kappa

  Averaged completeness of the slice family.

• consistent : selfPkg.family.ConsistentWithPoints strategy self.zeta

  Averaged point-consistency of the slice family.

• selfConsistent : selfPkg.family.StronglySelfConsistent strategy.state self.zeta

  Averaged strong self-consistency of the slice family.

• bounded : IdxPolyFamily.SliceBoundednessInput strategy selfPkg.family self.zeta

  Averaged boundedness input for the pasting theorem.

• error_le : ldPastingInInductionError params k eps delta gamma self.kappa self.zeta ≤ mainInductionError params.next k eps delta gamma

  Error telescoping from the induction-section pasting bound to the next-stage target.