Section 6 — Definitions

This file contains restriction/lifting maps, section-local error terms, averaging operators, and tensor-placement bookkeeping for the induction step.

References

• references/ldt-paper/inductive_step.tex

def MIPStarRE.LDT.MainInductionStep.liftAxisAnswer (params : Parameters) [FieldModel params.q] (x : Fq params) : AxisLinePolynomial params → AxisLinePolynomial params.next

Lift an axis-line answer from the restricted slice back to the ambient space.

Equations

• MIPStarRE.LDT.MainInductionStep.liftAxisAnswer params x f = MIPStarRE.LDT.AxisLinePolynomial.appendAtHeight params f x

structure MIPStarRE.LDT.MainInductionStep.RestrictedSymStrat (params : Parameters) [FieldModel params.q] (ι : Type u_2) [Fintype ι] [DecidableEq ι] : Type (max u_2 u_3)

Restricted slice data keeps the point and axis-parallel measurements complete, and packages a genuine projective measurement on the slice's diagonal answer space.

The paper's outcome-level formula would send a slice polynomial f to the ambient outcome append_x(f). With the current ambient diagonal answer encoding, that map is not total on all ambient outcomes, so here we preserve the verifier-visible base-point readout used in Chapter 10 instead: first postprocess the ambient slice-preserving diagonal measurement to its value at zeroCoord in F_q, then re-embed that F_q-valued projective measurement into the honest slice answer space DiagonalLinePolynomial params using canonical representatives.

This yields a complete projective measurement on the (m,q,d) diagonal answer space whose base-point evaluation agrees with the ambient slice-preserving branch, eliminating the earlier lossy submeasurement while remaining faithful to the restricted diagonal test actually formalized here.

• state : QuantumState (ι × ι)

  The bipartite state carried by the restricted strategy.

• isNormalized : self.state.IsNormalized

  The restricted strategy reuses the ambient state's normalization witness.

• pointMeasurement : IdxProjMeas (Point params) (Fq params) ι

  The restricted point measurement.

• axisParallelMeasurement : AxisParallelCovariantMeasurement params ι

  The restricted axis-parallel line measurement, packaged with transport covariance.

• diagonalMeasurement : IdxProjMeas (DiagonalLine params) (DiagonalLinePolynomial params) ι

  The restricted diagonal-line measurement on the honest slice answer space.

noncomputable def MIPStarRE.LDT.MainInductionStep.RestrictedSymStrat.axisParallelPointAnswerFamily {params : Parameters} [FieldModel params.q] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (strategy : RestrictedSymStrat params ι) : IdxSubMeas (AxisParallelTestSample params) (Fq params) ι

Sampled point answers in the axis-parallel lines test. Point player receives u (base point) and answers at u.

Equations

• strategy.axisParallelPointAnswerFamily = MIPStarRE.LDT.axisParallelPointAnswerFamilyOf strategy.pointMeasurement

noncomputable def MIPStarRE.LDT.MainInductionStep.RestrictedSymStrat.axisParallelLineAnswerFamily {params : Parameters} [FieldModel params.q] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (strategy : RestrictedSymStrat params ι) : IdxSubMeas (AxisParallelTestSample params) (Fq params) ι

Sampled line answers in the axis-parallel lines test, evaluated at the base point u (parameter zeroCoord).

Equations

• strategy.axisParallelLineAnswerFamily = MIPStarRE.LDT.axisParallelLineAnswerFamilyOf strategy.axisParallelMeasurement.toIdxProjMeas

noncomputable def MIPStarRE.LDT.MainInductionStep.RestrictedSymStrat.restrictedDiagonalPointAnswerFamily {params : Parameters} [FieldModel params.q] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (strategy : RestrictedSymStrat params ι) (j : Fin params.m) : IdxSubMeas (RestrictedDiagonalSample params j) (Fq params) ι

Sampled point answers in the j-restricted diagonal test. Point player receives u and answers at u.

Equations

• strategy.restrictedDiagonalPointAnswerFamily j = MIPStarRE.LDT.diagonalPointAnswerFamilyOf strategy.pointMeasurement j

noncomputable def MIPStarRE.LDT.MainInductionStep.RestrictedSymStrat.restrictedDiagonalLineAnswerFamily {params : Parameters} [FieldModel params.q] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (strategy : RestrictedSymStrat params ι) (j : Fin params.m) : IdxSubMeas (RestrictedDiagonalSample params j) (Fq params) ι

Sampled diagonal-line answers in the j-restricted diagonal test, evaluated at the base point (parameter zeroCoord).

Equations

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

noncomputable def MIPStarRE.LDT.MainInductionStep.RestrictedSymStrat.axisParallelFailureProbability {params : Parameters} [FieldModel params.q] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (strategy : RestrictedSymStrat params ι) : Error

Failure surrogate for the axis-parallel lines test.

Equations

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

noncomputable def MIPStarRE.LDT.MainInductionStep.RestrictedSymStrat.selfConsistencyFailureProbability {params : Parameters} [FieldModel params.q] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (strategy : RestrictedSymStrat params ι) : Error

Failure surrogate for the self-consistency test.

Equations

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

noncomputable def MIPStarRE.LDT.MainInductionStep.RestrictedSymStrat.diagonalFailureProbability {params : Parameters} [FieldModel params.q] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (strategy : RestrictedSymStrat params ι) : Error

Failure surrogate for the diagonal lines test. Averages over restriction index j, then the j-restricted diagonal test.

Equations

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

structure MIPStarRE.LDT.MainInductionStep.RestrictedSymStrat.IsGood {params : Parameters} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [FieldModel params.q] (strategy : RestrictedSymStrat params ι) (eps delta gamma : Error) : Prop

Goodness data for a restricted strategy.

• axisParallelTest : strategy.axisParallelFailureProbability ≤ eps

  The restricted axis-parallel test fails with probability at most eps.

• selfConsistencyTest : strategy.selfConsistencyFailureProbability ≤ delta

  The restricted self-consistency test fails with probability at most delta.

• diagonalLineTest : strategy.diagonalFailureProbability ≤ gamma

  The restricted diagonal-line test fails with probability at most gamma.

def MIPStarRE.LDT.MainInductionStep.axisLinePolynomialEquiv (params : Parameters) [FieldModel params.q] (x : Fq params) : AxisLinePolynomial params ≃ AxisLinePolynomial params.next

Equivalence between slice and ambient axis-line polynomials at a fixed height x: liftAxisAnswer sends a slice polynomial to its ambient lift, with AxisLinePolynomial.restrictAtHeight as inverse.

Equations

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

noncomputable def MIPStarRE.LDT.MainInductionStep.restrictAxisParallelMeasurement {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (x : Fq params) : IdxProjMeas (AxisParallelLine params) (AxisLinePolynomial params) ι

Restrict an axis-parallel line measurement to the slice at height x.

Equations

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

noncomputable def MIPStarRE.LDT.MainInductionStep.diagonalValueRepresentative (params : Parameters) [FieldModel params.q] (a : Fq params) : DiagonalLinePolynomial params

Canonical honest slice answer with prescribed value at the base point.

We use the constant polynomial because the restricted diagonal branch only reads line answers at zeroCoord.

Equations

• MIPStarRE.LDT.MainInductionStep.diagonalValueRepresentative params a = { poly := Polynomial.C (MIPStarRE.LDT.decodeScalar a), degreeBounded := ⋯ }

noncomputable def MIPStarRE.LDT.MainInductionStep.restrictDiagonalMeasurement {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (x : Fq params) : IdxProjMeas (DiagonalLine params) (DiagonalLinePolynomial params) ι

Restrict a diagonal-line measurement to the slice at height x.

This is not literally the paper's outcome reindexing f ↦ DiagonalLinePolynomial.appendAtHeight params f x; that map only covers the degree-params.m * params.d ambient outcomes. Instead we preserve the only statistic used by the restricted diagonal test formalized here, namely the base-point answer at zeroCoord.

Concretely we:

1. restrict the ambient line question to the slice-preserving line,
2. postprocess the ambient projective measurement to its zeroCoord value in F_q, and
3. re-embed that F_q-valued projective measurement into the honest slice answer space via diagonalValueRepresentative.

This produces a complete projective measurement on DiagonalLinePolynomial params whose induced base-point answer distribution is exactly the same as the ambient slice-preserving diagonal measurement.

Equations

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

noncomputable def MIPStarRE.LDT.MainInductionStep.restrictDiagonalAnswerMeasurement {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (x : Fq params) : IdxProjMeas (DiagonalLine params) (DiagonalLineAnswer params) ι

Restrict a diagonal-line measurement to the slice at height x, using the paper-level function-answer alphabet.

Unlike restrictDiagonalMeasurement, this keeps the whole line answer function rather than only the value at zeroCoord. The map is total because DiagonalLineAnswer has no degree-bound subtype proof to preserve.

Equations

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

noncomputable def MIPStarRE.LDT.MainInductionStep.xRestrictedAnswerSymStrat {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (x : Fq params) : AnswerSymStrat params ι

The x-restricted strategy with function-valued diagonal-line answers.

This matches the slice-restriction interface in inductive_step.tex, lines 436--455. It is kept parallel to the current xRestrictedStrategy, whose diagonal field uses the legacy degree-bounded answer alphabet and therefore only preserves the sampled base-point readout.

Equations

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

@[simp]

theorem MIPStarRE.LDT.MainInductionStep.xRestrictedAnswerSymStrat_state {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (x : Fq params) : (xRestrictedAnswerSymStrat params strategy x).state = strategy.state

The function-answer restricted strategy reuses the ambient bipartite state.

@[simp]

theorem MIPStarRE.LDT.MainInductionStep.xRestrictedAnswerSymStrat_pointMeasurement_apply {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (x : Fq params) (u : Point params) : (xRestrictedAnswerSymStrat params strategy x).pointMeasurement u = strategy.pointMeasurement (appendPoint params u x)

The function-answer restricted strategy reindexes point questions by appending the slice height.

@[simp]

theorem MIPStarRE.LDT.MainInductionStep.xRestrictedAnswerSymStrat_isNormalized {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (x : Fq params) : ⋯ = ⋯

The function-answer restricted strategy reuses the parent normalization witness.

@[simp]

theorem MIPStarRE.LDT.MainInductionStep.xRestrictedAnswerSymStrat_diagonalMeasurement_apply {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (x : Fq params) (ℓ : DiagonalLine params) : (xRestrictedAnswerSymStrat params strategy x).diagonalMeasurement.toIdxProjMeas ℓ = restrictDiagonalAnswerMeasurement params strategy x ℓ

The function-answer restricted diagonal measurement is the answer-valued restriction of the ambient diagonal measurement.

@[simp]

theorem MIPStarRE.LDT.MainInductionStep.restrictDiagonalAnswerMeasurement_postprocess_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (x : Fq params) (ℓ : DiagonalLine params) : (postprocess (restrictDiagonalAnswerMeasurement params strategy x ℓ).toSubMeas fun (f : DiagonalLineAnswer params) => f zeroCoord) = postprocess (strategy.diagonalMeasurement.toIdxProjMeas (DiagonalLine.appendAtHeight params ℓ x)).toSubMeas fun (f : DiagonalLinePolynomial params.next) => f.toFun zeroCoord

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

noncomputable def MIPStarRE.LDT.MainInductionStep.xRestrictedStrategy {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (x : Fq params) : RestrictedSymStrat params ι

The x-restricted strategy from the proof of the main induction theorem.

Equations

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

@[simp]

theorem MIPStarRE.LDT.MainInductionStep.xRestrictedStrategy_state {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (x : Fq params) : (xRestrictedStrategy params strategy x).state = strategy.state

Restricting a strategy does not change its bipartite state.

@[simp]

theorem MIPStarRE.LDT.MainInductionStep.xRestrictedStrategy_isNormalized {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (x : Fq params) : ⋯ = ⋯

Restricting a strategy reuses the parent strategy's normalization witness.

@[simp]

theorem MIPStarRE.LDT.MainInductionStep.xRestrictedStrategy_pointMeasurement_apply {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (x : Fq params) (u : Point params) : (xRestrictedStrategy params strategy x).pointMeasurement u = strategy.pointMeasurement (appendPoint params u x)

Restricting a strategy reindexes point questions by appending the slice height.

@[simp]

theorem MIPStarRE.LDT.MainInductionStep.restrictAxisParallelMeasurement_outcome {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (x : Fq params) (ℓ : AxisParallelLine params) (f : AxisLinePolynomial params) : (restrictAxisParallelMeasurement params strategy x ℓ).outcome f = (strategy.axisParallelMeasurement.toIdxProjMeas (AxisParallelLine.appendAtHeight params ℓ x)).outcome (liftAxisAnswer params x f)

Restricting an axis-parallel measurement reindexes outcomes by slice extension.

@[simp]

theorem MIPStarRE.LDT.MainInductionStep.restrictDiagonalMeasurement_postprocess_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (x : Fq params) (ℓ : DiagonalLine params) : (postprocess (restrictDiagonalMeasurement params strategy x ℓ).toSubMeas fun (f : DiagonalLinePolynomial params) => f.toFun zeroCoord) = postprocess (strategy.diagonalMeasurement.toIdxProjMeas (DiagonalLine.appendAtHeight params ℓ x)).toSubMeas fun (f : DiagonalLinePolynomial params.next) => f.toFun zeroCoord

Postprocessing the restricted diagonal measurement at the base point recovers exactly the ambient slice-preserving diagonal answer distribution at the base point.

noncomputable def MIPStarRE.LDT.MainInductionStep.mainInductionNu (params : Parameters) (k : ℕ) (eps delta gamma : Error) : Error

The intermediate ν from thm:main-induction.

Equations

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

noncomputable def MIPStarRE.LDT.MainInductionStep.mainInductionError (params : Parameters) (k : ℕ) (eps delta gamma : Error) : Error

The explicit σ of thm:main-induction.

Equations

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

noncomputable def MIPStarRE.LDT.MainInductionStep.selfImprovementInInductionError (params : Parameters) (eps delta _gamma : Error) : Error

The section-local self-improvement error.

Equations

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

noncomputable def MIPStarRE.LDT.MainInductionStep.ldPastingInInductionNu (params : Parameters) (k : ℕ) (eps delta gamma zeta : Error) : Error

The intermediate ν from the section-local pasting theorem.

Equations

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

noncomputable def MIPStarRE.LDT.MainInductionStep.ldPastingInInductionError (params : Parameters) (k : ℕ) (eps delta gamma kappa zeta : Error) : Error

The section-local pasting consistency error.

Equations

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

noncomputable def MIPStarRE.LDT.MainInductionStep.tensorFailureExpectation {Outcome : Type u_2} {ιA : Type u_3} {ιB : Type u_4} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] [Fintype Outcome] (ψ : QuantumState (ιA × ιB)) (Z : Quantum.Op ιA) (H : SubMeas Outcome ιB) : Error

Tensor-failure expectation on a bipartite space.

Computes ⟨ψ| (Z ⊗ I)(I ⊗ (I - Σ H_a)) |ψ⟩ where Z acts on the left register and H acts on the right register.

Equations

• MIPStarRE.LDT.MainInductionStep.tensorFailureExpectation ψ Z H = MIPStarRE.LDT.ev ψ (MIPStarRE.LDT.leftTensor Z * MIPStarRE.LDT.rightTensor (1 - H.total))

noncomputable def MIPStarRE.LDT.MainInductionStep.sliceTransverseDirectionWeight (params : Parameters) : Error

Probability that a sampled test line in F_q^{m+1} is not parallel to the new axis.

Equations

• MIPStarRE.LDT.MainInductionStep.sliceTransverseDirectionWeight params = ↑params.m / ↑(params.m + 1)

noncomputable def MIPStarRE.LDT.MainInductionStep.sliceConditioningLoss (params : Parameters) : Error

Reciprocal loss incurred when conditioning away the new axis direction.

In lem:restricted-probabilities, the axis-parallel and diagonal branches use this same conditioning step, so both averaged slice bounds carry the paper's common factor ((m + 1) / m).

Equations

• MIPStarRE.LDT.MainInductionStep.sliceConditioningLoss params = ↑(params.m + 1) / ↑params.m