Section 6 — Answer-Valued Self-Improvement Slice Transport

The answer-valued analogues of the Section 6 slice-transport constructors. The ordinary construction, including selfImprovementInInductionSection, lives in SelfImprovementAssembly.Core and is imported here so that the answer-valued construction can reuse the same Section 9 self-improvement theorem. This is the counterpart of the vendored MainInductionStep/Theorems/SelfImprovementAssembly/AnswerSlice.lean (under MIPRE/Background/LIDT/MIPStarRE/LDT/) in the port of planning/c6b-plan.md (milestone M12, section "Port conventions").

Translation

A strategy is a SymStrat params 𝔓 K, SymStrat params.next 𝔓 K or AnswerSymStrat params 𝔓 K, whose state is the symmetric model strategy.state : SymModel 𝔓 K; Polynomial params is MIPStarRE.LDT.Polynomial params, Z : MIPStarRE.Quantum.Op ι is Z : 𝔓, Error is ℝ, H.toSubMeas.liftLeft is H.toSubMeas.liftLeft strategy.state, leftPlacedSubMeas (ιB := ι) is strategy.state.leftPlacedSubMeas (and rightPlacedSubMeas), and the relations are read on strategy.state. The state-free dummyDiagonalCovariantMeasurement is generic over an ordered ⋆-ring R in the position of the vendored carrier ι. The vendored AnswerSymStrat and SymStrat fields permInvState, densityFixed and isNormalized, which answerSelfImprovementCarrier and xRestrictedAnswerSymStratOfAnswer copy from their argument, are theorems of the model here, so those two constructors set no such field, and xRestrictedAnswerSymStratOfAnswer_isNormalized, an equality of two proofs, loses @[simp], as xRestrictedAnswerSymStrat_isNormalized did (milestone M4). The vendored file-wide respectTransparency false is not needed: the file sets no option.

Three threaded hypotheses

As in SelfImprovementAssembly.Core, the four declarations that reach the ported SelfImprovement.selfImprovement take, right after strategy, hS : strategy.state.toBipartite.IsFinitePair, hA : NoAbelianProj strategy.state.toBipartite.opsA and hd : 1 ≤ params.d: AnswerSelfImprovementData.slice_outputs_ofSliceStrategyTransport, AnswerSelfImprovementData.slice_outputs_ofAnswerCarrier, AnswerSelfImprovementData.ofSliceStrategyTransport and AnswerSelfImprovementData.ofAnswerCarrier. They are stated for the ambient strategy. A concrete slice strategy of SliceStrategyTransport has the ambient state (state_eq), so hS and hA pass to it as hstate ▸ hS; the answer carrier has the ambient state by definition, so they pass to it unchanged; and hd is a hypothesis on params. The vendored statements, on finite carriers, need none of the three. AnswerSelfImprovementData.SliceStrategyTransport keeps its five vendored fields.

Proofs that differ from the vendored ones

• AnswerSelfImprovementData.slice_outputs_ofSliceStrategyTransport rewrites with state_eq in the goal rather than in each of the six hypotheses, as the ordinary one in Core does.
• AnswerSelfImprovementData.slice_outputs_ofAnswerCarrier closes the six fields by definitional equality: the carrier's state, point measurement and averaged point operator are those of the answer slice by rfl, and answerSliceSelfImprovementError unfolds to the error of the conclusion.
• AnswerSelfImprovementData.ofSelfImprovementInInductionSection builds the record from Classical.choose directly, as SelfImprovementData.ofSelfImprovementInInductionSection does.

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/self_improvement.tex
• blueprint/src/chapter/ch10_induction.tex

noncomputable def MIPRE.LIDT.Co.MainInductionStep.dummyDiagonalCovariantMeasurement (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (R : Type u_3) [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] : DiagonalCovariantMeasurement params R

A covariant diagonal measurement with a fixed zero polynomial outcome.

This measurement is used only as an inert diagonal component when applying the axis-parallel/self-consistency form of self-improvement to an answer-valued slice. The Section 9 conclusion obtained in this way is independent of the diagonal-line failure probability. It is state-free, so it is stated over any ordered ⋆-ring R, in the position of the vendored carrier.

Equations

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

noncomputable def MIPRE.LIDT.Co.MainInductionStep.answerSelfImprovementCarrier {𝔓 : 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) : SymStrat params 𝔓 K

Forget the answer-valued diagonal alphabet of a restricted slice, replacing it by an inert ordinary diagonal measurement.

The point, axis-parallel and state data are unchanged. This is therefore sufficient for the self-improvement theorem variant whose hypotheses are exactly the axis-parallel and point self-consistency bounds. The vendored fields permInvState, densityFixed and isNormalized are theorems of the model.

Equations

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

noncomputable def MIPRE.LIDT.Co.MainInductionStep.restrictAnswerDiagonalAnswerMeasurement {𝔓 : 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.next 𝔓 K) (x : MIPStarRE.LDT.Fq params) : IdxProjMeas (MIPStarRE.LDT.DiagonalLine params) (MIPStarRE.LDT.DiagonalLineAnswer params) 𝔓

Restrict an answer-valued diagonal-line measurement to the slice at height x.

This is the answer-valued analogue of restrictDiagonalAnswerMeasurement. Because the diagonal answer alphabet is the full function space on the line, restriction is the total map DiagonalLineAnswer.restrictAtHeight; no low-degree support theorem is needed to define this slice.

Equations

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

theorem MIPRE.LIDT.Co.MainInductionStep.restrictAnswerDiagonalAnswerMeasurement_transportInvariant {𝔓 : 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.next 𝔓 K) (x : MIPStarRE.LDT.Fq params) : DiagonalAnswerMeasurementTransportInvariant params (restrictAnswerDiagonalAnswerMeasurement params strategy x)

Transport covariance for the answer-valued restricted diagonal-line measurement.

@[simp]

theorem MIPRE.LIDT.Co.MainInductionStep.restrictAnswerDiagonalAnswerMeasurement_postprocess_zero {𝔓 : 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.next 𝔓 K) (x : MIPStarRE.LDT.Fq params) (ℓ : MIPStarRE.LDT.DiagonalLine params) : (postprocess (restrictAnswerDiagonalAnswerMeasurement params strategy x ℓ).toSubMeas fun (f : MIPStarRE.LDT.DiagonalLineAnswer params) => f MIPStarRE.LDT.zeroCoord) = postprocess (strategy.diagonalMeasurement.toIdxProjMeas (MIPStarRE.LDT.DiagonalLine.appendAtHeight params ℓ x)).toSubMeas fun (f : MIPStarRE.LDT.DiagonalLineAnswer params.next) => f MIPStarRE.LDT.zeroCoord

Evaluating the answer-valued restricted diagonal measurement at the base point recovers the ambient answer-valued diagonal readout.

noncomputable def MIPRE.LIDT.Co.MainInductionStep.xRestrictedAnswerSymStratOfAnswer {𝔓 : 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.next 𝔓 K) (x : MIPStarRE.LDT.Fq params) : AnswerSymStrat params 𝔓 K

The x-restricted strategy of an answer-valued successor strategy.

Paper origin: references/ldt-paper/inductive_step.tex:436-455, in the answer-valued strategy interface used for the recursive slice call.

This is the recursive restriction map needed for a simultaneous answer-valued form of the main induction theorem. It preserves the state, point measurement, axis-parallel measurement, and full answer-valued diagonal measurement on the slice. The vendored fields permInvState, densityFixed and isNormalized are theorems of the model.

Equations

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

@[simp]

theorem MIPRE.LIDT.Co.MainInductionStep.xRestrictedAnswerSymStratOfAnswer_state {𝔓 : 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.next 𝔓 K) (x : MIPStarRE.LDT.Fq params) : (xRestrictedAnswerSymStratOfAnswer params strategy x).state = strategy.state

Answer-valued slice restriction does not change the bipartite state.

@[simp]

theorem MIPRE.LIDT.Co.MainInductionStep.xRestrictedAnswerSymStratOfAnswer_pointMeasurement_apply {𝔓 : 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.next 𝔓 K) (x : MIPStarRE.LDT.Fq params) (u : MIPStarRE.LDT.Point params) : (xRestrictedAnswerSymStratOfAnswer params strategy x).pointMeasurement u = strategy.pointMeasurement (MIPStarRE.LDT.appendPoint params u x)

Answer-valued slice restriction reindexes point questions by appending the slice height.

theorem MIPRE.LIDT.Co.MainInductionStep.xRestrictedAnswerSymStratOfAnswer_isNormalized {𝔓 : 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.next 𝔓 K) (x : MIPStarRE.LDT.Fq params) : ⋯ = ⋯

Answer-valued slice restriction keeps the parent's normalization (the vendored statement equates the two normalization witnesses; here both are the model's).

@[simp]

theorem MIPRE.LIDT.Co.MainInductionStep.xRestrictedAnswerSymStratOfAnswer_diagonalMeasurement_apply {𝔓 : 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.next 𝔓 K) (x : MIPStarRE.LDT.Fq params) (ℓ : MIPStarRE.LDT.DiagonalLine params) : (xRestrictedAnswerSymStratOfAnswer params strategy x).diagonalMeasurement.toIdxProjMeas ℓ = restrictAnswerDiagonalAnswerMeasurement params strategy x ℓ

The diagonal measurement of an answer-valued slice is the full answer-valued restriction of the ambient diagonal measurement.

structure MIPRE.LIDT.Co.MainInductionStep.AnswerSelfImprovementData.SliceStrategyTransport {𝔓 : 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 (max u_1 u_2) u_3)

Transport data for producing the answer-valued self-improvement data from concrete per-slice symmetric strategies.

Paper origin: references/ldt-paper/inductive_step.tex:461-551 and references/ldt-paper/self_improvement.tex:631-811; this is the answer-valued restricted-slice interface for the same self-improvement step.

The answer-valued restriction xRestrictedAnswerSymStrat has the paper-faithful answer-valued diagonal interface, while the Section 9 self-improvement theorem is stated for ordinary SymStrats. This structure records the route through concrete ordinary slice strategies, together with the state and point-measurement transports needed to move the resulting conclusions back to the answer-valued restricted bookkeeping. The concrete slice strategies are SymStrat params 𝔓 K on the algebra and Hilbert space of the ambient strategy, so state_eq is an equality of symmetric models.

The legacy restricted strategy xRestrictedStrategy is not such an ordinary slice strategy. It is a RestrictedSymStrat, and its diagonal measurement is only the degree-bounded re-embedding of the sampled base-point value. Thus it does not by itself supply the transport-covariant diagonal measurement required by SymStrat.

An ordinary covariant realization is not a formal relabelling of the answer-valued strategy. Diagonal covariance after rebasing a line would force the ordinary polynomial outcome to reproduce all values of the function answer, not only the value at zeroCoord used by the diagonal test. Thus this route requires a genuine low-degree support/interpolation theorem for the answer-valued diagonal measurement; AnswerSelfImprovementData.ofAnswerCarrier avoids it.

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 answer-valued induction notation.

• sliceStrategy : MIPStarRE.LDT.Fq params → SymStrat params 𝔓 K

  Concrete symmetric strategies realizing the answer-restricted slice interfaces.

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

  Each concrete slice strategy uses the ambient state.

• pointMeasurement_eq (x : MIPStarRE.LDT.Fq params) : (self.sliceStrategy x).pointMeasurement = (xRestrictedAnswerSymStrat params strategy x).pointMeasurement

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

• averagedPoint_eq (x : MIPStarRE.LDT.Fq params) (h : MIPStarRE.LDT.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 : MIPStarRE.LDT.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 answer-restricted failure profile.

theorem MIPRE.LIDT.Co.MainInductionStep.AnswerSelfImprovementData.SliceStrategyTransport.averagedPoint_eq_of_pointMeasurement_eq {𝔓 : 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) (sliceStrategy : MIPStarRE.LDT.Fq params → SymStrat params 𝔓 K) (hpoint : ∀ (x : MIPStarRE.LDT.Fq params), (sliceStrategy x).pointMeasurement = (xRestrictedAnswerSymStrat params strategy x).pointMeasurement) (x : MIPStarRE.LDT.Fq params) (h : MIPStarRE.LDT.Polynomial params) : IdxPolyFamily.averagedPointEvaluationOperator (sliceStrategy x) h = IdxPolyFamily.averagedSlicePointEvaluationOperator strategy x h

The averaged point-operator compatibility for answer-valued slices follows from point-measurement transport.

Both sides unfold to the same average over strategy.pointMeasurement (appendPoint params u x) once the concrete slice point measurement is identified with xRestrictedAnswerSymStrat.

noncomputable def MIPRE.LIDT.Co.MainInductionStep.AnswerSelfImprovementData.SliceStrategyTransport.ofPointMeasurementEq {𝔓 : 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) (sliceStrategy : MIPStarRE.LDT.Fq params → SymStrat params 𝔓 K) (state_eq : ∀ (x : MIPStarRE.LDT.Fq params), (sliceStrategy x).state = strategy.state) (pointMeasurement_eq : ∀ (x : MIPStarRE.LDT.Fq params), (sliceStrategy x).pointMeasurement = (xRestrictedAnswerSymStrat params strategy x).pointMeasurement) (good : ∀ (x : MIPStarRE.LDT.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 answer-valued 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 answer-valued restricted slice interface and the Section 9 interface.

The structural averaged-point field is derived from 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 MIPRE.LIDT.Co.MainInductionStep.AnswerSelfImprovementData.SliceStrategyTransport.good_of_restrictedGood {𝔓 : 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) (sliceStrategy : MIPStarRE.LDT.Fq params → SymStrat params 𝔓 K) (state_eq : ∀ (x : MIPStarRE.LDT.Fq params), (sliceStrategy x).state = strategy.state) (pointMeasurement_eq : ∀ (x : MIPStarRE.LDT.Fq params), (sliceStrategy x).pointMeasurement = (xRestrictedAnswerSymStrat params strategy x).pointMeasurement) (axisParallelMeasurement_eq : ∀ (x : MIPStarRE.LDT.Fq params), (sliceStrategy x).axisParallelMeasurement.toIdxProjMeas = (xRestrictedAnswerSymStrat params strategy x).axisParallelMeasurement.toIdxProjMeas) (diagonalZeroCoord_eq : ∀ (x : MIPStarRE.LDT.Fq params) (ℓ : MIPStarRE.LDT.DiagonalLine params), (postprocess ((sliceStrategy x).diagonalMeasurement.toIdxProjMeas ℓ).toSubMeas fun (f : MIPStarRE.LDT.DiagonalLinePolynomial params) => f.toFun MIPStarRE.LDT.zeroCoord) = postprocess ((xRestrictedAnswerSymStrat params strategy x).diagonalMeasurement.toIdxProjMeas ℓ).toSubMeas fun (f : MIPStarRE.LDT.DiagonalLineAnswer params) => f MIPStarRE.LDT.zeroCoord) (x : MIPStarRE.LDT.Fq params) : (sliceStrategy x).IsGood (restrictionPkg.profile.axisParallel x) (restrictionPkg.profile.selfConsistency x) (restrictionPkg.profile.diagonal x)

Transport answer-restricted goodness to a concrete slice strategy once the state and verifier-visible measurements agree with xRestrictedAnswerSymStrat.

The diagonal compatibility is stated only after postprocessing both diagonal answer alphabets to their zeroCoord value; this is the comparison used by the LDT diagonal subtest and avoids claiming a false equality between DiagonalLinePolynomial and DiagonalLineAnswer families.

noncomputable def MIPRE.LIDT.Co.MainInductionStep.AnswerSelfImprovementData.SliceStrategyTransport.ofMeasurementEq {𝔓 : 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) (sliceStrategy : MIPStarRE.LDT.Fq params → SymStrat params 𝔓 K) (state_eq : ∀ (x : MIPStarRE.LDT.Fq params), (sliceStrategy x).state = strategy.state) (pointMeasurement_eq : ∀ (x : MIPStarRE.LDT.Fq params), (sliceStrategy x).pointMeasurement = (xRestrictedAnswerSymStrat params strategy x).pointMeasurement) (axisParallelMeasurement_eq : ∀ (x : MIPStarRE.LDT.Fq params), (sliceStrategy x).axisParallelMeasurement.toIdxProjMeas = (xRestrictedAnswerSymStrat params strategy x).axisParallelMeasurement.toIdxProjMeas) (diagonalZeroCoord_eq : ∀ (x : MIPStarRE.LDT.Fq params) (ℓ : MIPStarRE.LDT.DiagonalLine params), (postprocess ((sliceStrategy x).diagonalMeasurement.toIdxProjMeas ℓ).toSubMeas fun (f : MIPStarRE.LDT.DiagonalLinePolynomial params) => f.toFun MIPStarRE.LDT.zeroCoord) = postprocess ((xRestrictedAnswerSymStrat params strategy x).diagonalMeasurement.toIdxProjMeas ℓ).toSubMeas fun (f : MIPStarRE.LDT.DiagonalLineAnswer params) => f MIPStarRE.LDT.zeroCoord) : SliceStrategyTransport params strategy eps delta gamma k restrictionPkg inductionPkg

Build answer-valued SliceStrategyTransport from concrete slice strategies and verifier-visible 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 forced by the answer-restricted interface: averaged point compatibility follows from point-measurement transport, and goodness follows from the answer-restricted failure profile plus state, axis-parallel, and diagonal zero-coordinate transport.

Equations

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

noncomputable def MIPRE.LIDT.Co.MainInductionStep.AnswerSelfImprovementData.ofSelfImprovementInInductionSection {𝔓 : 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) (hslice : ∀ (x : MIPStarRE.LDT.Fq params), ∃ (H : ProjSubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (Z : 𝔓), strategy.state.CompletenessAtLeast (SubMeas.liftLeft strategy.state H.toSubMeas) (1 - inductionPkg.sliceError x - answerSliceSelfImprovementError params restrictionPkg x) ∧ strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) (xRestrictedAnswerSymStrat params strategy x).pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params H.toSubMeas) (answerSliceSelfImprovementError params restrictionPkg x) ∧ strategy.state.BipartiteSSCRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily H.toSubMeas) (answerSliceSelfImprovementError params restrictionPkg x) ∧ strategy.state.SDDRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily (strategy.state.leftPlacedSubMeas H.toSubMeas)) (constSubMeasFamily (strategy.state.rightPlacedSubMeas H.toSubMeas)) (answerSliceSelfImprovementError params restrictionPkg x) ∧ tensorFailureExpectation strategy.state Z H.toSubMeas ≤ answerSliceSelfImprovementError params restrictionPkg x ∧ ∀ (h : MIPStarRE.LDT.Polynomial params), IdxPolyFamily.averagedSlicePointEvaluationOperator strategy x h ≤ Z) : AnswerSelfImprovementData params strategy eps delta gamma k restrictionPkg inductionPkg

Convert the slice-wise outputs feeding the answer-valued restricted-strategy self-improvement stage into the bookkeeping object expected by the answer-valued successor-step construction.

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

Equations

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

theorem MIPRE.LIDT.Co.MainInductionStep.AnswerSelfImprovementData.slice_outputs_ofSliceStrategyTransport {𝔓 : 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) (hS : strategy.state.toBipartite.IsFinitePair) (hA : NoAbelianProj strategy.state.toBipartite.opsA) (hd : 1 ≤ params.d) (eps delta gamma : ℝ) (k : ℕ) (restrictionPkg : AnswerSliceRestrictionData params strategy eps delta gamma) (inductionPkg : AnswerPerSliceInductionData params strategy eps delta gamma restrictionPkg k) (sliceTransport : SliceStrategyTransport params strategy eps delta gamma k restrictionPkg inductionPkg) (x : MIPStarRE.LDT.Fq params) : ∃ (H : ProjSubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (Z : 𝔓), strategy.state.CompletenessAtLeast (SubMeas.liftLeft strategy.state H.toSubMeas) (1 - inductionPkg.sliceError x - answerSliceSelfImprovementError params restrictionPkg x) ∧ strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) (xRestrictedAnswerSymStrat params strategy x).pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params H.toSubMeas) (answerSliceSelfImprovementError params restrictionPkg x) ∧ strategy.state.BipartiteSSCRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily H.toSubMeas) (answerSliceSelfImprovementError params restrictionPkg x) ∧ strategy.state.SDDRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily (strategy.state.leftPlacedSubMeas H.toSubMeas)) (constSubMeasFamily (strategy.state.rightPlacedSubMeas H.toSubMeas)) (answerSliceSelfImprovementError params restrictionPkg x) ∧ tensorFailureExpectation strategy.state Z H.toSubMeas ≤ answerSliceSelfImprovementError params restrictionPkg x ∧ ∀ (h : MIPStarRE.LDT.Polynomial params), IdxPolyFamily.averagedSlicePointEvaluationOperator strategy x h ≤ Z

Concrete answer-valued slice strategies give the slice-wise Section 9 outputs used by the answer-valued self-improvement data.

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 answer-restricted notation of the successor step. The hypotheses hS and hA are stated for the ambient strategy and pass to each slice strategy through state_eq; hd is a hypothesis on params.

theorem MIPRE.LIDT.Co.MainInductionStep.AnswerSelfImprovementData.slice_outputs_ofAnswerCarrier {𝔓 : 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) (hS : strategy.state.toBipartite.IsFinitePair) (hA : NoAbelianProj strategy.state.toBipartite.opsA) (hd : 1 ≤ params.d) (eps delta gamma : ℝ) (k : ℕ) (restrictionPkg : AnswerSliceRestrictionData params strategy eps delta gamma) (inductionPkg : AnswerPerSliceInductionData params strategy eps delta gamma restrictionPkg k) (x : MIPStarRE.LDT.Fq params) : ∃ (H : ProjSubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (Z : 𝔓), strategy.state.CompletenessAtLeast (SubMeas.liftLeft strategy.state H.toSubMeas) (1 - inductionPkg.sliceError x - answerSliceSelfImprovementError params restrictionPkg x) ∧ strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) (xRestrictedAnswerSymStrat params strategy x).pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params H.toSubMeas) (answerSliceSelfImprovementError params restrictionPkg x) ∧ strategy.state.BipartiteSSCRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily H.toSubMeas) (answerSliceSelfImprovementError params restrictionPkg x) ∧ strategy.state.SDDRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily (strategy.state.leftPlacedSubMeas H.toSubMeas)) (constSubMeasFamily (strategy.state.rightPlacedSubMeas H.toSubMeas)) (answerSliceSelfImprovementError params restrictionPkg x) ∧ tensorFailureExpectation strategy.state Z H.toSubMeas ≤ answerSliceSelfImprovementError params restrictionPkg x ∧ ∀ (h : MIPStarRE.LDT.Polynomial params), IdxPolyFamily.averagedSlicePointEvaluationOperator strategy x h ≤ Z

The answer-valued restricted slices directly give the slice-wise Section 9 outputs once self-improvement is applied in its axis-parallel/self-consistency form.

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

The ordinary carrier used in the proof keeps the slice state, point measurement, and axis-parallel measurement, and replaces only the diagonal measurement by an inert covariant measurement. This is sufficient because the called self-improvement theorem consumes only the axis-parallel and point self-consistency bounds. The carrier has the ambient state by definition, so the hypotheses hS and hA on the ambient strategy are its own; hd is a hypothesis on params.

noncomputable def MIPRE.LIDT.Co.MainInductionStep.AnswerSelfImprovementData.ofSliceStrategyTransport {𝔓 : 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) (hS : strategy.state.toBipartite.IsFinitePair) (hA : NoAbelianProj strategy.state.toBipartite.opsA) (hd : 1 ≤ params.d) (eps delta gamma : ℝ) (k : ℕ) (restrictionPkg : AnswerSliceRestrictionData params strategy eps delta gamma) (inductionPkg : AnswerPerSliceInductionData params strategy eps delta gamma restrictionPkg k) (sliceTransport : SliceStrategyTransport params strategy eps delta gamma k restrictionPkg inductionPkg) : AnswerSelfImprovementData params strategy eps delta gamma k restrictionPkg inductionPkg

Convert concrete per-slice structural data into the answer-valued 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 ordinary slice strategies and their structural measurement transports. It applies the theorem selfImprovementInInductionSection slice-by-slice and transports its fields back to the answer-valued restricted-slice interface via the recorded state and point-measurement equalities. It takes the hypotheses hS, hA and hd of slice_outputs_ofSliceStrategyTransport.

Equations

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

noncomputable def MIPRE.LIDT.Co.MainInductionStep.AnswerSelfImprovementData.ofAnswerCarrier {𝔓 : 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) (hS : strategy.state.toBipartite.IsFinitePair) (hA : NoAbelianProj strategy.state.toBipartite.opsA) (hd : 1 ≤ params.d) (eps delta gamma : ℝ) (k : ℕ) (restrictionPkg : AnswerSliceRestrictionData params strategy eps delta gamma) (inductionPkg : AnswerPerSliceInductionData params strategy eps delta gamma restrictionPkg k) : AnswerSelfImprovementData params strategy eps delta gamma k restrictionPkg inductionPkg

Construct the answer-valued Section 6 self-improvement data directly from the answer-valued restricted slices.

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

This removes the ordinary slice-realization assumption from the self-improvement stage. The construction uses the ordinary carrier only as a device for invoking the Section 9 theorem in the form whose hypotheses are the axis-parallel and point self-consistency estimates. It takes the hypotheses hS, hA and hd of slice_outputs_ofAnswerCarrier.

Equations

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