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

The base cases (m = 1) and the trivial large-error branches of the ordinary and answer-valued main induction statements. This is the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/MainInductionStep/Theorems/MainTheorems/Base.lean in the port of planning/c6b-plan.md (milestone M12, section "Port conventions").

Translation

A strategy is a SymStrat params 𝔓 K or an AnswerSymStrat params 𝔓 K (Co/Test/StrategyCore.lean), whose state is the symmetric model strategy.state : SymModel 𝔓 K; Polynomial params is MIPStarRE.LDT.Polynomial params, measurements live in the local algebra 𝔓 (the vendored Op ι), errors are real numbers (the vendored Error := ℝ), and ConsRel is read on strategy.state. The geometry of axis-parallel lines, zeroPoint, axisLinePolynomialToPolynomial (the vendored Basic/LinePolynomialEmbedding.lean, classical and imported, as it has no Co counterpart) and the scalar lemmas throughPoint_eq_zeroPoint_of_m_eq_one and min_eps_one_le_mainInductionError_of_m_eq_one are the vendored classical declarations, reached through explicit open lists. The vendored file-wide respectTransparency false is not needed: the file sets no option.

Dropped hypotheses

The vendored bounds of the axis-parallel failure probability and of the trivial witness's consistency defect by 1 pass strategy.isNormalized to bipartiteConsError_uniform_le_one; here that is the keystone's strategy.state.bipartiteConsError_uniform_le_one, with no normalization argument (the vector state of a model is a unit vector). No statement takes a new hypothesis: neither the base case nor the large-error branch orthonormalizes.

Proofs that differ from the vendored ones

• The one-dimensional argument, which the vendored file writes out twice (for SymStrat and for AnswerSymStrat), is the private theorem exists_polynomialMeasurement_consRel_of_m_eq_one, stated for a point measurement and an axis-parallel measurement: the polynomial measurement is the canonical line's measurement read as a global polynomial, and its evaluation family is the sampled line family by covariance (AxisParallelCovariantMeasurement.reparamInvariant) and throughPoint_eq_zeroPoint_of_m_eq_one. Both base cases apply it.
• The nonnegativity of ε, δ and γ is eps_nonneg_of_isGood and its siblings (Co/Test/StrategyFailures.lean), which the vendored file proves inline.

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

theorem MIPRE.LIDT.Co.MainInductionStep.mainInductionBaseCase {𝔓 : Type uP} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type uK} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (eps delta gamma : ℝ) (k : ℕ) (hm1 : params.m = 1) (hgood : strategy.IsGood eps delta gamma) : ∃ (G : Measurement (MIPStarRE.LDT.Polynomial params) 𝔓), strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params G.toSubMeas) (MIPStarRE.LDT.MainInductionStep.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 MIPRE.LIDT.Co.MainInductionStep.answerMainInductionBaseCase {𝔓 : Type uP} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type uK} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : AnswerSymStrat params 𝔓 K) (eps delta gamma : ℝ) (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 MIPRE.LIDT.Co.MainInductionStep.mainInductionOfOneLeError {𝔓 : Type uP} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type uK} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (eps delta gamma : ℝ) (k : ℕ) (herror : 1 ≤ MIPStarRE.LDT.MainInductionStep.mainInductionError params k eps delta gamma) : ∃ (G : Measurement (MIPStarRE.LDT.Polynomial params) 𝔓), strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params G.toSubMeas) (MIPStarRE.LDT.MainInductionStep.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 MIPRE.LIDT.Co.MainInductionStep.answerMainInductionOfOneLeError {𝔓 : Type uP} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type uK} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : AnswerSymStrat params 𝔓 K) (eps delta gamma : ℝ) (k : ℕ) (herror : 1 ≤ MIPStarRE.LDT.MainInductionStep.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.