Section 6 -- Answer-Valued Restricted Probability Statement

This module contains the answer-valued form of the restricted-probability bookkeeping for the main induction step.

References

• blueprint/src/chapter/ch10_induction.tex

theorem MIPStarRE.LDT.MainInductionStep.answerRestricted_axisParallelFailureProbability_eq {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (x : Fq params) : (xRestrictedAnswerSymStrat params strategy x).axisParallelFailureProbability = (xRestrictedStrategy params strategy x).axisParallelFailureProbability

The answer-valued slice has the same axis-parallel failure probability as the legacy restricted slice.

theorem MIPStarRE.LDT.MainInductionStep.answerRestricted_selfConsistencyFailureProbability_eq {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (x : Fq params) : (xRestrictedAnswerSymStrat params strategy x).selfConsistencyFailureProbability = (xRestrictedStrategy params strategy x).selfConsistencyFailureProbability

The answer-valued slice has the same self-consistency failure probability as the legacy restricted slice.

theorem MIPStarRE.LDT.MainInductionStep.answerRestricted_diagonalFailureProbability_eq {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (x : Fq params) : (xRestrictedAnswerSymStrat params strategy x).diagonalFailureProbability = (xRestrictedStrategy params strategy x).diagonalFailureProbability

The answer-valued slice has the same verifier-visible diagonal failure probability as the legacy restricted slice after evaluating line answers at the base point.

theorem MIPStarRE.LDT.MainInductionStep.answer_weighted_axisParallel_bound {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma : Error) (hgood : strategy.IsGood eps delta gamma) : (avgOver (uniformDistribution (Fq params)) fun (x : Fq params) => sliceTransverseDirectionWeight params * (xRestrictedAnswerSymStrat params strategy x).axisParallelFailureProbability) ≤ eps

The weighted average of the answer-valued restricted axis-parallel slice errors is bounded by the ambient axis-parallel test error.

theorem MIPStarRE.LDT.MainInductionStep.answer_weighted_diagonal_bound {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma : Error) (hgood : strategy.IsGood eps delta gamma) : (avgOver (uniformDistribution (Fq params)) fun (x : Fq params) => sliceTransverseDirectionWeight params * (xRestrictedAnswerSymStrat params strategy x).diagonalFailureProbability) ≤ gamma

The weighted average of the answer-valued restricted diagonal slice errors is bounded by the ambient diagonal-line test error.

theorem MIPStarRE.LDT.MainInductionStep.AnswerRestrictedProbabilitiesStatement.ofWeightedBounds {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma : Error) (hgood : strategy.IsGood eps delta gamma) (haxisWeightedBound : (avgOver (uniformDistribution (Fq params)) fun (x : Fq params) => sliceTransverseDirectionWeight params * (xRestrictedAnswerSymStrat params strategy x).axisParallelFailureProbability) ≤ eps) (hdiagonalWeightedBound : (avgOver (uniformDistribution (Fq params)) fun (x : Fq params) => sliceTransverseDirectionWeight params * (xRestrictedAnswerSymStrat params strategy x).diagonalFailureProbability) ≤ gamma) : AnswerRestrictedProbabilitiesStatement params strategy eps delta gamma

Data answer-valued weighted restricted axis/diagonal bounds into the public answer-valued restricted-probabilities statement.

theorem MIPStarRE.LDT.MainInductionStep.answerRestrictedProbabilities {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma : Error) (hgood : strategy.IsGood eps delta gamma) : AnswerRestrictedProbabilitiesStatement params strategy eps delta gamma

Answer-valued version of lem:restricted-probabilities.

Answer-valued successor restrictions

The preceding lemmas start from an ordinary successor strategy and build the answer-valued slice profile used in the current Section 6 successor route. For the simultaneous answer-valued induction theorem, the successor strategy itself has answer-valued diagonal measurements. The next definitions and lemmas record the corresponding restricted-probability theorem without replacing that diagonal measurement by an ordinary low-degree realization.

structure MIPStarRE.LDT.MainInductionStep.AnswerSuccessorRestrictedFailureProfile {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params.next ι) : Type

Slice-wise error profile obtained by restricting an answer-valued successor strategy.

This is the answer-valued analogue of AnswerRestrictedFailureProfile, but with source strategy AnswerSymStrat params.next ι and slices xRestrictedAnswerSymStratOfAnswer.

• axisParallel : Fq params → Error

  The axis-parallel failure bound attached to each slice height.

• selfConsistency : Fq params → Error

  The self-consistency failure bound attached to each slice height.

• diagonal : Fq params → Error

  The diagonal-line failure bound attached to each slice height.

• restrictedGood (x : Fq params) : (xRestrictedAnswerSymStratOfAnswer params strategy x).IsGood (self.axisParallel x) (self.selfConsistency x) (self.diagonal x)

  Each answer-valued slice is good with the recorded parameters.

noncomputable def MIPStarRE.LDT.MainInductionStep.averageAnswerSuccessorRestrictedAxisParallelError {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] {strategy : AnswerSymStrat params.next ι} (profile : AnswerSuccessorRestrictedFailureProfile params strategy) : Error

Average restricted axis-parallel error over answer-valued successor slices.

Equations

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

noncomputable def MIPStarRE.LDT.MainInductionStep.averageAnswerSuccessorRestrictedSelfConsistencyError {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] {strategy : AnswerSymStrat params.next ι} (profile : AnswerSuccessorRestrictedFailureProfile params strategy) : Error

Average restricted self-consistency error over answer-valued successor slices.

Equations

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

noncomputable def MIPStarRE.LDT.MainInductionStep.averageAnswerSuccessorRestrictedDiagonalError {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] {strategy : AnswerSymStrat params.next ι} (profile : AnswerSuccessorRestrictedFailureProfile params strategy) : Error

Average restricted diagonal-line error over answer-valued successor slices.

Equations

• MIPStarRE.LDT.MainInductionStep.averageAnswerSuccessorRestrictedDiagonalError params profile = MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Fq params)) profile.diagonal

structure MIPStarRE.LDT.MainInductionStep.AnswerSuccessorRestrictedProbabilitiesStatement {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params.next ι) (eps delta gamma : Error) : Prop

Restricted-probabilities statement for an answer-valued successor strategy.

This is a Lean-only statement needed for the simultaneous answer-valued induction route. It has the same three averaged conclusions as the restricted probabilities lemma (\label{lem:restricted-probabilities}), with xRestrictedAnswerSymStratOfAnswer as the slice strategy.

• profileExists : ∃ (profile : AnswerSuccessorRestrictedFailureProfile params strategy), averageAnswerSuccessorRestrictedAxisParallelError params profile ≤ sliceConditioningLoss params * eps ∧ averageAnswerSuccessorRestrictedSelfConsistencyError params profile ≤ delta ∧ averageAnswerSuccessorRestrictedDiagonalError params profile ≤ sliceConditioningLoss params * gamma

  There is a slice-wise answer-valued error profile realizing the three averaged restricted bounds.

theorem MIPStarRE.LDT.MainInductionStep.answerSuccessor_weighted_axisParallel_bound {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params.next ι) (eps delta gamma : Error) (hgood : strategy.IsGood eps delta gamma) : (avgOver (uniformDistribution (Fq params)) fun (x : Fq params) => sliceTransverseDirectionWeight params * (xRestrictedAnswerSymStratOfAnswer params strategy x).axisParallelFailureProbability) ≤ eps

The weighted average of the answer-valued successor restricted axis-parallel slice errors is bounded by the ambient answer-valued axis-parallel test error.

theorem MIPStarRE.LDT.MainInductionStep.answerSuccessor_selfConsistencyRestrictedAverage_eq {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params.next ι) : (avgOver (uniformDistribution (Fq params)) fun (x : Fq params) => (xRestrictedAnswerSymStratOfAnswer params strategy x).selfConsistencyFailureProbability) = strategy.selfConsistencyFailureProbability

Averaging the self-consistency defect over answer-valued successor restrictions recovers the ambient answer-valued self-consistency defect.

theorem MIPStarRE.LDT.MainInductionStep.answerSuccessor_weighted_diagonal_bound {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params.next ι) (eps delta gamma : Error) (hgood : strategy.IsGood eps delta gamma) : (avgOver (uniformDistribution (Fq params)) fun (x : Fq params) => sliceTransverseDirectionWeight params * (xRestrictedAnswerSymStratOfAnswer params strategy x).diagonalFailureProbability) ≤ gamma

The weighted average of the answer-valued successor restricted diagonal slice errors is bounded by the ambient answer-valued diagonal-line test error.

theorem MIPStarRE.LDT.MainInductionStep.AnswerSuccessorRestrictedProbabilitiesStatement.ofWeightedBounds {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params.next ι) (eps delta gamma : Error) (hgood : strategy.IsGood eps delta gamma) (haxisWeightedBound : (avgOver (uniformDistribution (Fq params)) fun (x : Fq params) => sliceTransverseDirectionWeight params * (xRestrictedAnswerSymStratOfAnswer params strategy x).axisParallelFailureProbability) ≤ eps) (hdiagonalWeightedBound : (avgOver (uniformDistribution (Fq params)) fun (x : Fq params) => sliceTransverseDirectionWeight params * (xRestrictedAnswerSymStratOfAnswer params strategy x).diagonalFailureProbability) ≤ gamma) : AnswerSuccessorRestrictedProbabilitiesStatement params strategy eps delta gamma

Assemble the weighted answer-valued successor restricted-probability bounds into the averaged statement.

theorem MIPStarRE.LDT.MainInductionStep.answerSuccessorRestrictedProbabilities {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params.next ι) (eps delta gamma : Error) (hgood : strategy.IsGood eps delta gamma) : AnswerSuccessorRestrictedProbabilitiesStatement params strategy eps delta gamma

Answer-valued restricted-probabilities theorem for an answer-valued successor strategy.

This is the restricted-probability input needed by a simultaneous answer-valued proof of the main induction theorem. It is a construction from the answer-valued successor strategy's own goodness hypotheses, not an additional theorem assumption.

theorem MIPStarRE.LDT.MainInductionStep.answerSuccessorRestrictedSliceConclusions {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params.next ι) (eps delta gamma : Error) (k : ℕ) (hgood : strategy.IsGood eps delta gamma) (hinduction : AnswerMainInductionHypothesis params) (hk_next : 400 * params.next.m * params.next.d ≤ k) (hsmall : mainInductionError params.next k eps delta gamma < 1) : ∃ (profile : AnswerSuccessorRestrictedFailureProfile params strategy), averageAnswerSuccessorRestrictedAxisParallelError params profile ≤ sliceConditioningLoss params * eps ∧ averageAnswerSuccessorRestrictedSelfConsistencyError params profile ≤ delta ∧ averageAnswerSuccessorRestrictedDiagonalError params profile ≤ sliceConditioningLoss params * gamma ∧ ∀ (x : Fq params), AnswerMainInductionConclusion params (xRestrictedAnswerSymStratOfAnswer params strategy x) (profile.axisParallel x) (profile.selfConsistency x) (profile.diagonal x) k

Recursive predecessor conclusions for the answer-valued successor slices.

Paper origin: references/ldt-paper/inductive_step.tex:441-454, in the answer-valued successor interface used by the simultaneous induction route.

This theorem is the formal content of the recursive call: from the answer-valued restricted-probabilities theorem and the predecessor answer-valued induction hypothesis, it obtains the main-induction conclusion for every restricted slice. The hypotheses k ≥ 1 and 400 * params.m * params.d ≤ k are derived here from the nontrivial successor branch, rather than being stored in a source theorem statement.