Section 6 — Induction Step Data

The intermediate conclusion structures and bookkeeping statements of the induction step: the conclusions of the induction-level self-improvement and pasting theorems, the restricted failure profiles, and the stage data for the paper's slice restriction, slice-wise induction, self-improvement and pasting assembly. This is the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/MainInductionStep/Statements.lean in the port of planning/c6b-plan.md (milestone M4, section "Port conventions").

A strategy is a SymStrat params.next 𝔓 K (Co/Test/StrategyCore.lean), whose state is the symmetric model strategy.state : SymModel 𝔓 K; the vendored QuantumState (ι × ι) statements become statements about that model, with local operators in 𝔓 (the vendored Op ι) placed by strategy.state.L and strategy.state.R, and errors in ℝ (the vendored Error). The left and right placements leftPlacedSubMeas (ιB := ι) and rightPlacedSubMeas (ιA := ι) are strategy.state.leftPlacedSubMeas and strategy.state.rightPlacedSubMeas, and tensorFailureExpectation is the one-algebra form of Co/MainInductionStep/Defs.lean.

AnswerMainInductionHypothesis quantifies over the local algebra 𝔓 and the Hilbert space K of a symmetric model, in their own universes, where the vendored hypothesis quantifies over a finite carrier ι, and only over strategies whose model is a finite pair (strategy.state.toBipartite.IsFinitePair) without abelian projections in its first player's operators (NoAbelianProj strategy.state.toBipartite.opsA). These are the hypotheses hS, hA of the ported orthonormalization (Co/MakingMeasurementsProjective/Orthonormalization.lean), which the successor step of the induction reaches through self-improvement (the vendored SelfImprovementTop/Core.lean, line 433); restriction to a slice keeps the state (xRestrictedAnswerSymStrat_state), so they pass to the slices, and milestone M13 discharges them for the doubled model with Doubling.isFinitePair and Doubling.noAbelianProj_iff. This departs from the vendored statement, whose finite carriers need no such hypothesis.

The error constants (mainInductionError, selfImprovementInInductionError, ldPastingInInductionError, sliceConditioningLoss) are the vendored classical declarations, imported through Co/MainInductionStep/Defs.lean and named through an explicit open list.

Not ported

Every declaration of the vendored file has a counterpart here.

References

In LionSR/MIPStarRE at commit 507e8122, not in this repository:

• references/ldt-paper/inductive_step.tex
• references/ldt-paper/ld-pasting.tex

structure MIPRE.LIDT.Co.MainInductionStep.SelfImprovementInInductionSectionConclusion {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (_G : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (H : ProjSubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (Z : 𝔓) (eps delta gamma nu : ℝ) : 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 the symmetric model strategy.state. Fields that involve placed operators use leftPlacedSubMeas / rightPlacedSubMeas / tensorFailureExpectation of that model.

• completeness : strategy.state.CompletenessAtLeast (SubMeas.liftLeft strategy.state H.toSubMeas) (1 - nu - MIPStarRE.LDT.MainInductionStep.selfImprovementInInductionError params eps delta gamma)

  The projective submeasurement remains almost complete.

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

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

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

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

• selfCloseness : strategy.state.SDDRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily (strategy.state.leftPlacedSubMeas H.toSubMeas)) (constSubMeasFamily (strategy.state.rightPlacedSubMeas H.toSubMeas)) (MIPStarRE.LDT.MainInductionStep.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 ≤ MIPStarRE.LDT.MainInductionStep.selfImprovementInInductionError params eps delta gamma

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

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

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

structure MIPRE.LIDT.Co.MainInductionStep.LdPastingInInductionSectionConclusion {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (_family : IdxPolyFamily params 𝔓) (H : Measurement (MIPStarRE.LDT.Polynomial params.next) 𝔓) (eps delta gamma kappa zeta : ℝ) (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 : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params.next)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params.next H.toSubMeas) (MIPStarRE.LDT.MainInductionStep.ldPastingInInductionError params k eps delta gamma kappa zeta)

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

structure MIPRE.LIDT.Co.MainInductionStep.RestrictedFailureProfile {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) : Type

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

• axisParallel : MIPStarRE.LDT.Fq params → ℝ

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

• selfConsistency : MIPStarRE.LDT.Fq params → ℝ

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

• diagonal : MIPStarRE.LDT.Fq params → ℝ

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

• restrictedGood (x : MIPStarRE.LDT.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 MIPRE.LIDT.Co.MainInductionStep.AnswerRestrictedFailureProfile {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) : 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 : MIPStarRE.LDT.Fq params → ℝ

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

• selfConsistency : MIPStarRE.LDT.Fq params → ℝ

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

• diagonal : MIPStarRE.LDT.Fq params → ℝ

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

• restrictedGood (x : MIPStarRE.LDT.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 MIPRE.LIDT.Co.MainInductionStep.averageRestrictedAxisParallelError {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] {strategy : SymStrat params.next 𝔓 K} (profile : RestrictedFailureProfile params strategy) : ℝ

Average restricted axis-parallel error over slices.

Equations

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

noncomputable def MIPRE.LIDT.Co.MainInductionStep.averageRestrictedSelfConsistencyError {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] {strategy : SymStrat params.next 𝔓 K} (profile : RestrictedFailureProfile params strategy) : ℝ

Average restricted self-consistency error over slices.

Equations

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

noncomputable def MIPRE.LIDT.Co.MainInductionStep.averageRestrictedDiagonalError {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] {strategy : SymStrat params.next 𝔓 K} (profile : RestrictedFailureProfile params strategy) : ℝ

Average restricted diagonal-line error over slices.

Equations

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

noncomputable def MIPRE.LIDT.Co.MainInductionStep.averageAnswerRestrictedAxisParallelError {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] {strategy : SymStrat params.next 𝔓 K} (profile : AnswerRestrictedFailureProfile params strategy) : ℝ

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

Equations

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

noncomputable def MIPRE.LIDT.Co.MainInductionStep.averageAnswerRestrictedSelfConsistencyError {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] {strategy : SymStrat params.next 𝔓 K} (profile : AnswerRestrictedFailureProfile params strategy) : ℝ

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

Equations

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

noncomputable def MIPRE.LIDT.Co.MainInductionStep.averageAnswerRestrictedDiagonalError {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] {strategy : SymStrat params.next 𝔓 K} (profile : AnswerRestrictedFailureProfile params strategy) : ℝ

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

Equations

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

structure MIPRE.LIDT.Co.MainInductionStep.RestrictedProbabilitiesStatement {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (eps delta gamma : ℝ) : 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 ≤ MIPStarRE.LDT.MainInductionStep.sliceConditioningLoss params * eps ∧ averageRestrictedSelfConsistencyError params profile ≤ delta ∧ averageRestrictedDiagonalError params profile ≤ MIPStarRE.LDT.MainInductionStep.sliceConditioningLoss params * gamma

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

structure MIPRE.LIDT.Co.MainInductionStep.AnswerRestrictedProbabilitiesStatement {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (eps delta gamma : ℝ) : 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 ≤ MIPStarRE.LDT.MainInductionStep.sliceConditioningLoss params * eps ∧ averageAnswerRestrictedSelfConsistencyError params profile ≤ delta ∧ averageAnswerRestrictedDiagonalError params profile ≤ MIPStarRE.LDT.MainInductionStep.sliceConditioningLoss params * gamma

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

structure MIPRE.LIDT.Co.MainInductionStep.SliceRestrictionData {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (eps delta gamma : ℝ) : 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 ≤ MIPStarRE.LDT.MainInductionStep.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 ≤ MIPStarRE.LDT.MainInductionStep.sliceConditioningLoss params * gamma

  Averaged diagonal slice error bound.

structure MIPRE.LIDT.Co.MainInductionStep.AnswerSliceRestrictionData {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (eps delta gamma : ℝ) : 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 ≤ MIPStarRE.LDT.MainInductionStep.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 ≤ MIPStarRE.LDT.MainInductionStep.sliceConditioningLoss params * gamma

  Averaged diagonal slice error bound.

structure MIPRE.LIDT.Co.MainInductionStep.PerSliceInductionData {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (eps delta gamma : ℝ) (restrictionPkg : SliceRestrictionData params strategy eps delta gamma) (k : ℕ) : Type (max u_1 u_3)

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 : MIPStarRE.LDT.Fq params → ℝ

  Slice-wise inductive error σ_x.

• sliceMeasurement : MIPStarRE.LDT.Fq params → Measurement (MIPStarRE.LDT.Polynomial params) 𝔓

  Slice-wise inductive measurement G^x.

• pointConsistency (x : MIPStarRE.LDT.Fq params) : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.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 : MIPStarRE.LDT.Fq params) : self.sliceError x ≤ MIPStarRE.LDT.MainInductionStep.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 MIPRE.LIDT.Co.MainInductionStep.AnswerPerSliceInductionData {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (eps delta gamma : ℝ) (restrictionPkg : AnswerSliceRestrictionData params strategy eps delta gamma) (k : ℕ) : Type (max u_1 u_3)

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 : MIPStarRE.LDT.Fq params → ℝ

  Slice-wise inductive error σ_x.

• sliceMeasurement : MIPStarRE.LDT.Fq params → Measurement (MIPStarRE.LDT.Polynomial params) 𝔓

  Slice-wise inductive measurement G^x.

• pointConsistency (x : MIPStarRE.LDT.Fq params) : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.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 : MIPStarRE.LDT.Fq params) : self.sliceError x ≤ MIPStarRE.LDT.MainInductionStep.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 MIPRE.LIDT.Co.MainInductionStep.AnswerMainInductionConclusion {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : AnswerSymStrat params 𝔓 K) (eps delta gamma : ℝ) (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 MIPRE.LIDT.Co.MainInductionStep.AnswerMainInductionHypothesis (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.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 main theorem.

It quantifies over symmetric models: a local C*-algebra 𝔓 : Type v and a Hilbert space K : Type w, where the vendored hypothesis quantifies over a finite carrier ι : Type v, and over strategies whose model is a finite pair without abelian projections in its first player's operators, the hypotheses hS, hA of the ported orthonormalization, which the successor step reaches through self-improvement; the vendored hypothesis has none. The explicit .{u,v,w} universe binder keeps the three universes apart, as the vendored binder .{u,v} keeps the universe of FieldModel's carrier apart from that of the carrier, so that a proof that instantiates FieldModel.{0} can still apply the hypothesis to a model in higher universes.

Equations

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

noncomputable def MIPRE.LIDT.Co.MainInductionStep.sliceSelfImprovementError {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] {strategy : SymStrat params.next 𝔓 K} {eps delta gamma : ℝ} (restrictionPkg : SliceRestrictionData params strategy eps delta gamma) (x : MIPStarRE.LDT.Fq params) : ℝ

The slice-local self-improvement error ζ_x.

Equations

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

noncomputable def MIPRE.LIDT.Co.MainInductionStep.answerSliceSelfImprovementError {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] {strategy : SymStrat params.next 𝔓 K} {eps delta gamma : ℝ} (restrictionPkg : AnswerSliceRestrictionData params strategy eps delta gamma) (x : MIPStarRE.LDT.Fq params) : ℝ

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 MIPRE.LIDT.Co.MainInductionStep.SelfImprovementData {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (eps delta gamma : ℝ) (k : ℕ) (restrictionPkg : SliceRestrictionData params strategy eps delta gamma) (inductionPkg : PerSliceInductionData params strategy eps delta gamma restrictionPkg k) : Type (max u_1 u_3)

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 (its diagonal measurement carries no reparametrization-invariance field, and it has no role-symmetrization API), this data records directly the paper-faithful properties that will later be averaged into the pasting inputs.

• sliceProj : MIPStarRE.LDT.Fq params → ProjSubMeas (MIPStarRE.LDT.Polynomial params) 𝔓

  Slice-wise projective submeasurement Ĝ^x.

• sliceWitness : MIPStarRE.LDT.Fq params → 𝔓

  Slice-wise PSD witness Z^x.

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

  Slice-wise completeness bound.

• pointConsistency (x : MIPStarRE.LDT.Fq params) : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.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 : MIPStarRE.LDT.Fq params) : strategy.state.BipartiteSSCRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily (self.sliceProj x).toSubMeas) (sliceSelfImprovementError params restrictionPkg x)

  Slice-wise strong self-consistency.

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

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

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

  Slice-wise boundedness residual.

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

  Slice-wise domination of the averaged point operator.

noncomputable def MIPRE.LIDT.Co.MainInductionStep.SelfImprovementData.family {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] {strategy : SymStrat params.next 𝔓 K} {eps delta gamma : ℝ} {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 MIPRE.LIDT.Co.MainInductionStep.SelfImprovementData.family_meas {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] {strategy : SymStrat params.next 𝔓 K} {eps delta gamma : ℝ} {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

The slice family of pkg.family is the improved slice family Ĝ^x.

@[simp]

theorem MIPRE.LIDT.Co.MainInductionStep.SelfImprovementData.family_witness {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] {strategy : SymStrat params.next 𝔓 K} {eps delta gamma : ℝ} {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 : MIPStarRE.LDT.Fq params) : pkg.family.witness x = pkg.sliceWitness x

The witness of pkg.family is the slice witness Z^x.

@[simp]

theorem MIPRE.LIDT.Co.MainInductionStep.SelfImprovementData.family_dominationTarget {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] {strategy : SymStrat params.next 𝔓 K} {eps delta gamma : ℝ} {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 : MIPStarRE.LDT.Fq params) (g : MIPStarRE.LDT.Polynomial params) : pkg.family.dominationTarget x g = IdxPolyFamily.averagedSlicePointEvaluationOperator strategy x g

The domination target of pkg.family is the averaged slice-point evaluation operator.

structure MIPRE.LIDT.Co.MainInductionStep.AnswerSelfImprovementData {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (eps delta gamma : ℝ) (k : ℕ) (restrictionPkg : AnswerSliceRestrictionData params strategy eps delta gamma) (inductionPkg : AnswerPerSliceInductionData params strategy eps delta gamma restrictionPkg k) : Type (max u_1 u_3)

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 : MIPStarRE.LDT.Fq params → ProjSubMeas (MIPStarRE.LDT.Polynomial params) 𝔓

  Slice-wise projective submeasurement Ĝ^x.

• sliceWitness : MIPStarRE.LDT.Fq params → 𝔓

  Slice-wise PSD witness Z^x.

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

  Slice-wise completeness bound.

• pointConsistency (x : MIPStarRE.LDT.Fq params) : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.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 : MIPStarRE.LDT.Fq params) : strategy.state.BipartiteSSCRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily (self.sliceProj x).toSubMeas) (answerSliceSelfImprovementError params restrictionPkg x)

  Slice-wise strong self-consistency.

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

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

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

  Slice-wise boundedness residual.

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

  Slice-wise domination of the averaged point operator.

noncomputable def MIPRE.LIDT.Co.MainInductionStep.AnswerSelfImprovementData.family {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] {strategy : SymStrat params.next 𝔓 K} {eps delta gamma : ℝ} {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 MIPRE.LIDT.Co.MainInductionStep.AnswerSelfImprovementData.family_meas {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] {strategy : SymStrat params.next 𝔓 K} {eps delta gamma : ℝ} {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

The slice family of pkg.family is the improved slice family Ĝ^x.

@[simp]

theorem MIPRE.LIDT.Co.MainInductionStep.AnswerSelfImprovementData.family_witness {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] {strategy : SymStrat params.next 𝔓 K} {eps delta gamma : ℝ} {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 : MIPStarRE.LDT.Fq params) : pkg.family.witness x = pkg.sliceWitness x

The witness of pkg.family is the slice witness Z^x.

@[simp]

theorem MIPRE.LIDT.Co.MainInductionStep.AnswerSelfImprovementData.family_dominationTarget {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] {strategy : SymStrat params.next 𝔓 K} {eps delta gamma : ℝ} {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 : MIPStarRE.LDT.Fq params) (g : MIPStarRE.LDT.Polynomial params) : pkg.family.dominationTarget x g = IdxPolyFamily.averagedSlicePointEvaluationOperator strategy x g

The domination target of pkg.family is the averaged slice-point evaluation operator.

structure MIPRE.LIDT.Co.MainInductionStep.AveragedPastingData {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (eps delta gamma : ℝ) (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 : ℝ

  Averaged completeness parameter κ.

• zeta : ℝ

  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 : MIPStarRE.LDT.MainInductionStep.ldPastingInInductionError params k eps delta gamma self.kappa self.zeta ≤ MIPStarRE.LDT.MainInductionStep.mainInductionError params.next k eps delta gamma

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