Section 6 — Answer-valued restricted probability statement #
The answer-valued form of the restricted-probability bookkeeping for the main induction step:
the counterpart of
MIPRE/Background/LIDT/MIPStarRE/LDT/MainInductionStep/Theorems/RestrictedProbabilities/AnswerValued.lean
in the port of planning/c6b-plan.md (milestone M12, section "Port conventions").
Translation #
A strategy is a SymStrat params.next 𝔓 K or an AnswerSymStrat params.next 𝔓 K
(Co/Test/StrategyCore.lean), whose state is the symmetric model strategy.state : SymModel 𝔓 K;
the vendored qBipartiteConsDefect strategy.state A B and bipartiteConsError strategy.state 𝒟 A B
are strategy.state.qBipartiteConsDefect A B and strategy.state.bipartiteConsError 𝒟 A B, and
errors are real numbers (the vendored Error := ℝ). Every restriction keeps the state
(xRestrictedAnswerSymStrat_state, xRestrictedAnswerSymStratOfAnswer_state, by rfl), so each
restricted defect is a defect of strategy.state. The classical names (mainInductionError,
sliceTransverseDirectionWeight, sliceConditioningLoss, weighted_bound_to_average,
weighted_embedded_average_le_full_average, avgOver_uniform_restrictedDiagonalSample_append,
one_le_k_of_mainInductionError_lt_one, mainInductionSuccessorBound_pred) are the vendored
ones, imported through Co RestrictedProbabilities/Base and Co InductionParameterBounds/MainError
and reached through explicit open lists. No vendored statement here has a swap, density or
normalization hypothesis, so none is dropped. The vendored file-wide respectTransparency false is
not needed: the file sets no option.
Two threaded hypotheses #
answerSuccessorRestrictedSliceConclusions applies the predecessor
AnswerMainInductionHypothesis (Co MainInductionStep/Statements.lean), which quantifies only over
strategies whose model is a finite pair without abelian projections in its first player's
operators. So it takes, right after strategy, hS : strategy.state.toBipartite.IsFinitePair and
hA : NoAbelianProj strategy.state.toBipartite.opsA, and passes them unchanged to each slice
xRestrictedAnswerSymStratOfAnswer params strategy x, whose state is strategy.state by
definition. It does not take 1 ≤ params.d: the hypothesis is applied, not proved, here. Its
universe binder is AnswerMainInductionHypothesis.{uF, uP, uK}, with 𝔓 : Type uP and
K : Type uK, where the vendored one is .{uF, uι}. Every other declaration holds for any
symmetric model: restriction neither orthonormalizes nor solves a semidefinite program.
Proofs that differ from the vendored ones #
- The
try rflsteps of the vendored file arerflor gone, and itscalcchains ofavgOver_congrsteps areEq.transandavgOver_congrterms. AnswerRestrictedProbabilitiesStatement.ofWeightedBoundsand its answer-valued successor analogue rewrite the weighted bounds withavgOver_const_mul, as CoRestrictedProbabilities/Coredoes, in place of the vendoredsimpa.- In
answerSuccessor_weighted_axisParallel_boundthe carrier's goodness ishgood's axis-parallel and self-consistency fields, by definitional equality, with nosimpa. answerSuccessorRestrictedDiagonalSampleError_equses the M12 lemmarestrictAnswerDiagonalAnswerMeasurement_postprocess_zero(CoSelfImprovementAssembly/AnswerSlice.lean) and the appended-line identitycongrArg (DiagonalLine.mk _) hdir, as CoRestrictedProbabilities/Diagonaldoes, in place of the vendored unfoldingsimp.
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.texblueprint/src/chapter/ch10_induction.tex
The answer-valued slice has the same axis-parallel failure probability as the legacy restricted slice.
The answer-valued slice has the same self-consistency failure probability as the legacy restricted slice.
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.
The weighted average of the answer-valued restricted axis-parallel slice errors is bounded by the ambient axis-parallel test error.
The weighted average of the answer-valued restricted diagonal slice errors is bounded by the ambient diagonal-line test error.
Data answer-valued weighted restricted axis/diagonal bounds into the public answer-valued restricted-probabilities statement.
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.
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 𝔓 K and slices
xRestrictedAnswerSymStratOfAnswer.
- axisParallel : MIPStarRE.LDT.Fq params → ℝ
The axis-parallel failure bound attached to each slice height.
- selfConsistency : MIPStarRE.LDT.Fq params → ℝ
The self-consistency failure bound attached to each slice height.
- diagonal : MIPStarRE.LDT.Fq params → ℝ
The diagonal-line failure bound attached to each slice height.
- restrictedGood (x : MIPStarRE.LDT.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.
Instances For
Average restricted axis-parallel error over answer-valued successor slices.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Average restricted self-consistency error over answer-valued successor slices.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Average restricted diagonal-line error over answer-valued successor slices.
Equations
- MIPRE.LIDT.Co.MainInductionStep.averageAnswerSuccessorRestrictedDiagonalError params profile = MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Fq params)) profile.diagonal
Instances For
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 ≤ MIPStarRE.LDT.MainInductionStep.sliceConditioningLoss params * eps ∧ averageAnswerSuccessorRestrictedSelfConsistencyError params profile ≤ delta ∧ averageAnswerSuccessorRestrictedDiagonalError params profile ≤ MIPStarRE.LDT.MainInductionStep.sliceConditioningLoss params * gamma
There is a slice-wise answer-valued error profile realizing the three averaged restricted bounds.
Instances For
The weighted average of the answer-valued successor restricted axis-parallel slice errors is bounded by the ambient answer-valued axis-parallel test error.
Averaging the self-consistency defect over answer-valued successor restrictions recovers the ambient answer-valued self-consistency defect.
The j-restricted diagonal defect of the x-restricted answer-valued successor slice at
the sample s is the ambient defect at the embedded index and the sample with the height
appended to its base.
Per-index diagonal-line consistency defect of the x-restricted answer-valued successor
slice at index j, averaged over the restricted diagonal sample space.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Per-index diagonal-line consistency defect of the ambient answer-valued successor strategy
at index j, averaged over the ambient restricted diagonal sample space.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Averaging the restricted per-index diagonal error of the answer-valued successor slices over the slice height gives the ambient per-index error at the embedded index.
The average over slice heights of the answer-valued successor slices' diagonal failure probability is the average over embedded indices of the ambient per-index error.
The weighted average of the answer-valued successor restricted diagonal slice errors is bounded by the ambient answer-valued diagonal-line test error.
Assemble the weighted answer-valued successor restricted-probability bounds into the averaged statement.
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.
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. The model
hypotheses hS hA, which the predecessor hypothesis requires of each slice, pass to the slices
unchanged, a slice having the ambient state.