Section 6 — Main Induction Theorems: Base and Large-Error Branches

This module contains the base cases and the trivial large-error branches for the ordinary and answer-valued main induction statements.

theorem MIPStarRE.LDT.MainInductionStep.mainInductionBaseCase {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta gamma : Error) (k : ℕ) (hm1 : params.m = 1) (hgood : strategy.IsGood 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)

Direct base case of thm:main-induction when m = 1.

The paper uses the unique axis-parallel line measurement as the global polynomial measurement in this case.

theorem MIPStarRE.LDT.MainInductionStep.answerMainInductionBaseCase {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params ι) (eps delta gamma : Error) (k : ℕ) (hm1 : params.m = 1) (hgood : strategy.IsGood eps delta gamma) : AnswerMainInductionConclusion params strategy eps delta gamma k

Answer-valued base case of the main induction when m = 1.

Paper origin: references/ldt-paper/inductive_step.tex:441-454, specialized to the base dimension.

The proof is the same one-dimensional argument as mainInductionBaseCase. Only the axis-parallel line measurement is used to construct the global polynomial measurement, so the function-valued diagonal answer interface plays no role in this case.

theorem MIPStarRE.LDT.MainInductionStep.mainInductionOfOneLeError {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta gamma : Error) (k : ℕ) (herror : 1 ≤ 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)

Trivial branch of thm:main-induction when the target error is at least 1.

Paper origin: references/ldt-paper/inductive_step.tex:441-551, where the successor proof reduces to the nontrivial small-error regime before invoking the pasting argument. In the complementary branch the normalized consistency defect is bounded by 1, so a distinguished trivial polynomial measurement suffices.

theorem MIPStarRE.LDT.MainInductionStep.answerMainInductionOfOneLeError {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params ι) (eps delta gamma : Error) (k : ℕ) (herror : 1 ≤ mainInductionError params k eps delta gamma) : AnswerMainInductionConclusion params strategy eps delta gamma k

Trivial branch of the answer-valued main induction when the target error is at least 1.

This is the answer-valued analogue of mainInductionOfOneLeError. It supplies the large-error branch needed by a simultaneous answer-valued induction proof: the diagonal answer interface is irrelevant because the consistency defect between the point measurement and a distinguished trivial polynomial measurement is bounded by 1.