Section 6 — Ordinary Self-Improvement Data

Core public API for the ordinary self-improvement data: constructors for SelfImprovementData, the induction-section theorem selfImprovementInInductionSection, the monotone-witness cleanup mainInductionOfWitness, and the source-facing pasting theorem ldPastingInInductionSection.

The answer-valued slice-transport constructors are separated into SelfImprovementAssembly.AnswerSlice.

References

• blueprint/src/chapter/ch10_induction.tex

theorem MIPStarRE.LDT.MainInductionStep.mainInductionOfWitness {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta gamma : Error) (k : ℕ) (hwitness : ∃ (error : Error) (G : Measurement (Polynomial params) ι), ConsRel strategy.state (uniformDistribution (Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params G.toSubMeas) error ∧ error ≤ mainInductionError params k eps delta gamma) : ∃ (G : Measurement (Polynomial params) ι), ConsRel strategy.state (uniformDistribution (Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params G.toSubMeas) (mainInductionError params k eps delta gamma)

Monotone postprocessing of an explicit witness for the main-induction conclusion.

This helper is the final error ≤ mainInductionError cleanup step only; the actual Section 6 construction is carried by mainInductionBaseCase, mainInduction, and their predecessor, self-improvement, and pasting construction lemmas.

theorem MIPStarRE.LDT.MainInductionStep.selfImprovementInInductionSectionConclusion_ofSelfImprovementConclusion {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta gamma nu : Error) (G : SubMeas (Polynomial params) ι) (Gmeas : Measurement (Polynomial params) ι) (H : ProjSubMeas (Polynomial params) ι) (Z : Quantum.Op ι) (hfinal : SelfImprovement.SelfImprovementConclusion params strategy Gmeas H Z eps delta gamma nu) : SelfImprovementInInductionSectionConclusion params strategy G H Z eps delta gamma nu

Convert the Section 9 self-improvement conclusion into the Section 6 induction-level self-improvement conclusion.

The Section 6 conclusion records the original input submeasurement only as a parameter; its six mathematical fields concern the output projective submeasurement and the dual witness. This lemma isolates that transport, so the induction-section self-improvement target is not confused with measurement-completion bookkeeping.

theorem MIPStarRE.LDT.MainInductionStep.selfImprovementInInductionSection {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta gamma nu : Error) (hgood : strategy.IsGood eps delta gamma) (G : Measurement (Polynomial params) ι) (hcons : ConsRel strategy.state (uniformDistribution (Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params G.toSubMeas) nu) : ∃ (H : ProjSubMeas (Polynomial params) ι) (Z : Quantum.Op ι), SelfImprovementInInductionSectionConclusion params strategy G.toSubMeas H Z eps delta gamma nu

thm:self-improvement-in-induction-section.

Paper origin: references/ldt-paper/self_improvement.tex:631-811 (\label{thm:self-improvement}), used in the induction section at references/ldt-paper/inductive_step.tex:461-485. The labelled induction statement at references/ldt-paper/inductive_step.tex:249-286 states the input as a submeasurement, while the proved form at references/ldt-paper/self_improvement.tex:635-671 uses a measurement. This Lean statement follows the proved measurement-valued form needed in the induction proof.

The input (G) is a complete polynomial measurement, as in the paper's restated self-improvement theorem. The conclusion is phrased in the Section 6 record SelfImprovementInInductionSectionConclusion, whose fields are exactly the projective output estimates used in the inductive step. The proof applies SelfImprovement.selfImprovement and transports the resulting fields into the Section 6 record.

theorem MIPStarRE.LDT.MainInductionStep.selfImprovementInInductionSection_of_axisParallel_selfConsistency {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta gamma nu : Error) (haxis : strategy.axisParallelFailureProbability ≤ eps) (hself : strategy.selfConsistencyFailureProbability ≤ delta) (G : Measurement (Polynomial params) ι) (hcons : ConsRel strategy.state (uniformDistribution (Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params G.toSubMeas) nu) : ∃ (H : ProjSubMeas (Polynomial params) ι) (Z : Quantum.Op ι), SelfImprovementInInductionSectionConclusion params strategy G.toSubMeas H Z eps delta gamma nu

Induction-section self-improvement using only the two strategy bounds consumed by Section 9.

Paper origin: references/ldt-paper/self_improvement.tex:631-811.

This is a formalization-only strengthening of selfImprovementInInductionSection. The paper states the theorem in the standing context of an (eps, delta, gamma)-good strategy, but the displayed self-improvement construction uses the axis-parallel and point self-consistency bounds and its conclusion is independent of the diagonal-line error parameter.

noncomputable def MIPStarRE.LDT.MainInductionStep.SelfImprovementData.ofSelfImprovementInInductionSection {ι : Type uι} [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) (hslice : ∀ (x : Fq params), ∃ (H : ProjSubMeas (Polynomial params) ι) (Z : Quantum.Op ι), CompletenessAtLeast strategy.state H.liftLeft (1 - inductionPkg.sliceError x - sliceSelfImprovementError params restrictionPkg x) ∧ ConsRel strategy.state (uniformDistribution (Point params)) (xRestrictedStrategy params strategy x).pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params H.toSubMeas) (sliceSelfImprovementError params restrictionPkg x) ∧ BipartiteSSCRel strategy.state (uniformDistribution Unit) (constSubMeasFamily H.toSubMeas) (sliceSelfImprovementError params restrictionPkg x) ∧ SDDRel strategy.state (uniformDistribution Unit) (constSubMeasFamily (leftPlacedSubMeas H.toSubMeas)) (constSubMeasFamily (rightPlacedSubMeas H.toSubMeas)) (sliceSelfImprovementError params restrictionPkg x) ∧ tensorFailureExpectation strategy.state Z H.toSubMeas ≤ sliceSelfImprovementError params restrictionPkg x ∧ ∀ (h : Polynomial params), IdxPolyFamily.averagedSlicePointEvaluationOperator strategy x h ≤ Z) : SelfImprovementData params strategy eps delta gamma k restrictionPkg inductionPkg

Convert the slice-wise outputs feeding selfImprovementInInductionSection into the bookkeeping object expected by the later inductive step.

Paper origin: references/ldt-paper/inductive_step.tex:461-551, using the self-improvement theorem restated in references/ldt-paper/self_improvement.tex:631-811.

Because xRestrictedStrategy params strategy x is only a RestrictedSymStrat params ι rather than a full SymStrat params ι, the restricted-strategy outputs are supplied directly as the six paper-faithful fields recorded by SelfImprovementData.

Equations

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

structure MIPStarRE.LDT.MainInductionStep.SelfImprovementData.SliceStrategyTransport {ι : Type uι} [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ι)

Narrow transport record for running the Section 9 self-improvement theorem on each concrete Section 6 slice strategy.

Paper origin: references/ldt-paper/inductive_step.tex:461-551 and references/ldt-paper/self_improvement.tex:631-811; this records the formalization boundary needed to run the Section 9 theorem on concrete slice strategies.

For every slice the record asks for a concrete SymStrat params ι whose state, point-measurement interface, and averaged point operator agree with the restricted-slice bookkeeping used by Section 6. The equalities below do not derive the extra SymStrat fields (permInvState, densityFixed, or isNormalized) from the restricted strategy; those remain part of the supplied concrete slice strategies.

The Section 9 analytic proof debt is not stored in this record. The data-record constructor below calls the paper-facing theorem selfImprovementInInductionSection; its proof applies the Section 9 theorem and then transports the output estimates to the induction notation.

• sliceStrategy : Fq params → SymStrat params ι

  Concrete symmetric strategies realizing the slice interfaces.

• state_eq (x : Fq params) : (self.sliceStrategy x).state = strategy.state

  Each concrete slice strategy uses the ambient state.

• pointMeasurement_eq (x : Fq params) : (self.sliceStrategy x).pointMeasurement = (xRestrictedStrategy params strategy x).pointMeasurement

  Its point measurement agrees with the restricted-slice point interface.

• averagedPoint_eq (x : Fq params) (h : Polynomial params) : IdxPolyFamily.averagedPointEvaluationOperator (self.sliceStrategy x) h = IdxPolyFamily.averagedSlicePointEvaluationOperator strategy x h

  Its averaged point operator is the averaged slice point operator used by Section 6.

• good (x : Fq params) : (self.sliceStrategy x).IsGood (restrictionPkg.profile.axisParallel x) (restrictionPkg.profile.selfConsistency x) (restrictionPkg.profile.diagonal x)

  The concrete slice strategy is good with the restricted failure profile.

theorem MIPStarRE.LDT.MainInductionStep.SelfImprovementData.SliceStrategyTransport.averagedPoint_eq_of_pointMeasurement_eq {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (sliceStrategy : Fq params → SymStrat params ι) (hpoint : ∀ (x : Fq params), (sliceStrategy x).pointMeasurement = (xRestrictedStrategy params strategy x).pointMeasurement) (x : Fq params) (h : Polynomial params) : IdxPolyFamily.averagedPointEvaluationOperator (sliceStrategy x) h = IdxPolyFamily.averagedSlicePointEvaluationOperator strategy x h

The averaged slice point-operator compatibility is structural: once a concrete slice strategy's point measurement agrees with the restricted-slice point measurement, the averaged point operators agree by unfolding the two averages.

noncomputable def MIPStarRE.LDT.MainInductionStep.SelfImprovementData.SliceStrategyTransport.ofPointMeasurementEq {ι : Type uι} [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) (sliceStrategy : Fq params → SymStrat params ι) (state_eq : ∀ (x : Fq params), (sliceStrategy x).state = strategy.state) (pointMeasurement_eq : ∀ (x : Fq params), (sliceStrategy x).pointMeasurement = (xRestrictedStrategy params strategy x).pointMeasurement) (good : ∀ (x : Fq params), (sliceStrategy x).IsGood (restrictionPkg.profile.axisParallel x) (restrictionPkg.profile.selfConsistency x) (restrictionPkg.profile.diagonal x)) : SliceStrategyTransport params strategy eps delta gamma k restrictionPkg inductionPkg

Build SliceStrategyTransport without separately assuming averaged point-operator compatibility.

Paper origin: references/ldt-paper/inductive_step.tex:461-551; the averaged point-operator compatibility is a formal transport between the restricted slice interface and the Section 9 interface.

The only structural equality needed for that field is pointMeasurement_eq. The remaining inputs are the concrete slice strategies, their state transport, and their restricted-profile goodness.

Equations

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

theorem MIPStarRE.LDT.MainInductionStep.SelfImprovementData.SliceStrategyTransport.good_of_restrictedGood {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma : Error) (restrictionPkg : SliceRestrictionData params strategy eps delta gamma) (sliceStrategy : Fq params → SymStrat params ι) (state_eq : ∀ (x : Fq params), (sliceStrategy x).state = strategy.state) (pointMeasurement_eq : ∀ (x : Fq params), (sliceStrategy x).pointMeasurement = (xRestrictedStrategy params strategy x).pointMeasurement) (axisParallelMeasurement_eq : ∀ (x : Fq params), (sliceStrategy x).axisParallelMeasurement.toIdxProjMeas = (xRestrictedStrategy params strategy x).axisParallelMeasurement.toIdxProjMeas) (diagonalMeasurement_eq : ∀ (x : Fq params), (sliceStrategy x).diagonalMeasurement.toIdxProjMeas = (xRestrictedStrategy params strategy x).diagonalMeasurement) (x : Fq params) : (sliceStrategy x).IsGood (restrictionPkg.profile.axisParallel x) (restrictionPkg.profile.selfConsistency x) (restrictionPkg.profile.diagonal x)

Transport restricted-slice goodness to a concrete slice strategy once the state and the measurements used by the three LDT subtests agree with xRestrictedStrategy.

This is a structural helper for the successor route: it uses the restrictedGood field already stored in SliceRestrictionData.profile and does not introduce additional Section 9 analytic assumptions.

noncomputable def MIPStarRE.LDT.MainInductionStep.SelfImprovementData.SliceStrategyTransport.ofMeasurementEq {ι : Type uι} [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) (sliceStrategy : Fq params → SymStrat params ι) (state_eq : ∀ (x : Fq params), (sliceStrategy x).state = strategy.state) (pointMeasurement_eq : ∀ (x : Fq params), (sliceStrategy x).pointMeasurement = (xRestrictedStrategy params strategy x).pointMeasurement) (axisParallelMeasurement_eq : ∀ (x : Fq params), (sliceStrategy x).axisParallelMeasurement.toIdxProjMeas = (xRestrictedStrategy params strategy x).axisParallelMeasurement.toIdxProjMeas) (diagonalMeasurement_eq : ∀ (x : Fq params), (sliceStrategy x).diagonalMeasurement.toIdxProjMeas = (xRestrictedStrategy params strategy x).diagonalMeasurement) : SliceStrategyTransport params strategy eps delta gamma k restrictionPkg inductionPkg

Build SliceStrategyTransport from concrete slice strategies and measurement transport.

Paper origin: references/ldt-paper/inductive_step.tex:461-551 and references/ldt-paper/self_improvement.tex:631-811.

This constructor fills both structural fields that are forced by the restricted slice interface: averagedPoint_eq follows from point-measurement transport and good follows from the restricted failure profile plus state/axis/diagonal measurement transport. The remaining non-structural inputs are the concrete slice strategies themselves.

Equations

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

theorem MIPStarRE.LDT.MainInductionStep.SelfImprovementData.slice_outputs_ofSliceStrategyTransport {ι : Type uι} [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) (sliceTransport : SliceStrategyTransport params strategy eps delta gamma k restrictionPkg inductionPkg) (x : Fq params) : ∃ (H : ProjSubMeas (Polynomial params) ι) (Z : Quantum.Op ι), CompletenessAtLeast strategy.state H.liftLeft (1 - inductionPkg.sliceError x - sliceSelfImprovementError params restrictionPkg x) ∧ ConsRel strategy.state (uniformDistribution (Point params)) (xRestrictedStrategy params strategy x).pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params H.toSubMeas) (sliceSelfImprovementError params restrictionPkg x) ∧ BipartiteSSCRel strategy.state (uniformDistribution Unit) (constSubMeasFamily H.toSubMeas) (sliceSelfImprovementError params restrictionPkg x) ∧ SDDRel strategy.state (uniformDistribution Unit) (constSubMeasFamily (leftPlacedSubMeas H.toSubMeas)) (constSubMeasFamily (rightPlacedSubMeas H.toSubMeas)) (sliceSelfImprovementError params restrictionPkg x) ∧ tensorFailureExpectation strategy.state Z H.toSubMeas ≤ sliceSelfImprovementError params restrictionPkg x ∧ ∀ (h : Polynomial params), IdxPolyFamily.averagedSlicePointEvaluationOperator strategy x h ≤ Z

Concrete slice strategies give the slice-wise Section 9 outputs used by the ordinary self-improvement data in the successor step.

Paper origin: references/ldt-paper/inductive_step.tex:461-551 and references/ldt-paper/self_improvement.tex:631-811.

This is an internal transport theorem. It applies selfImprovementInInductionSection to each ordinary slice strategy supplied by SliceStrategyTransport, and then rewrites the state, point-measurement, and averaged-point conclusions back into the restricted-slice notation used in the successor step.

noncomputable def MIPStarRE.LDT.MainInductionStep.SelfImprovementData.ofSliceStrategyTransport {ι : Type uι} [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) (sliceTransport : SliceStrategyTransport params strategy eps delta gamma k restrictionPkg inductionPkg) : SelfImprovementData params strategy eps delta gamma k restrictionPkg inductionPkg

Convert per-slice structural slice data into the Section 6 self-improvement data.

Paper origin: references/ldt-paper/inductive_step.tex:461-551 and references/ldt-paper/self_improvement.tex:631-811.

The construction assumes the concrete slice strategies and their structural measurement transports. It applies the theorem selfImprovementInInductionSection slice-by-slice and transports its fields across the recorded equalities to the restricted-slice interface.

Equations

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

theorem MIPStarRE.LDT.MainInductionStep.ldPastingInInductionSection {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma kappa zeta : Error) (hgood : strategy.IsGood eps delta gamma) (family : IdxPolyFamily params ι) (hcomplete : family.Complete strategy.state kappa) (hcons : family.ConsistentWithPoints strategy zeta) (hself : family.StronglySelfConsistent strategy.state zeta) (hbound : IdxPolyFamily.SliceBoundednessInput strategy family zeta) (k : ℕ) (hk : 400 * params.m * params.d ≤ k) : ∃ (H : Measurement (Polynomial params.next) ι), LdPastingInInductionSectionConclusion params strategy family H eps delta gamma kappa zeta k

Source-facing Lean statement for thm:ld-pasting-in-induction-section.

Paper origin: references/ldt-paper/inductive_step.tex:299-338 (\label{thm:ld-pasting-in-induction-section}). The statement is the Chapter 6 restatement of thm:ld-pasting, with the error parameters named as they are used in the main-induction proof.

Source-faithful transport: This theorem invokes the unrestricted formal theorem Pasting.ldPasting and projects its point-consistency field into the induction-section conclusion record. It carries no additional assumption beyond the already formalized pasting theorem.