Section 6 β Averaged Slice Error Bounds: Successor Outputs #
The recursive answer-valued slice measurements of the successor step, the self-improvement
outputs on those slices, and the comparison of the self-improvement error ΞΆ with the
next-stage induction parameter Ξ½. This is the counterpart of
MIPRE/Background/LIDT/MIPStarRE/LDT/MainInductionStep/Theorems/AvgSliceErrors/Successor.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;
Polynomial params is MIPStarRE.LDT.Polynomial params, MIPStarRE.Quantum.Op ΞΉ is π,
Error is β, H.toSubMeas.liftLeft is H.toSubMeas.liftLeft strategy.state,
leftPlacedSubMeas (ΞΉB := ΞΉ) is strategy.state.leftPlacedSubMeas (and rightPlacedSubMeas),
and the relations (ConsRel, BipartiteSSCRel, SDDRel, CompletenessAtLeast) are read on
strategy.state. The error functions (mainInductionError, mainInductionNu,
selfImprovementInInductionError, sliceConditioningLoss) and dq_ratio_le_one are the
vendored classical declarations, 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.
Threaded hypotheses #
answerSuccessorRecursiveSliceMeasurements_ofMainInductionHypothesis applies Co
answerSuccessorRestrictedSliceConclusions, which takes the model hypotheses
hS : strategy.state.toBipartite.IsFinitePair and
hA : NoAbelianProj strategy.state.toBipartite.opsA of the predecessor
AnswerMainInductionHypothesis; so it takes hS hA right after strategy.
answerSuccessorSelfImprovementOutputs_ofMainInductionHypothesis also runs
selfImprovementInInductionSection_of_axisParallel_selfConsistency (Co
SelfImprovementAssembly/Core) on each slice carrier, so it takes hS hA and
hd : 1 β€ params.d right after strategy. The slice carrier
answerSelfImprovementCarrier params (xRestrictedAnswerSymStratOfAnswer params strategy x) has the
ambient state by definition, so hS and hA pass to it unchanged; hd is a hypothesis on
params. The universe binder of the induction hypothesis is
AnswerMainInductionHypothesis.{uF, uP, uK}, with π : Type uP and K : Type uK, where the
vendored one is .{uF, uΞΉ}. The two ΞΆ β€ Ξ½ lemmas take no new hypothesis.
Proofs that differ from the vendored ones #
- In
answerSuccessorSelfImprovementOutputs_ofMainInductionHypothesisthe slice carrier's state, point measurement, failure probabilities and averaged point operator are those of the answer slice and of the ambient carrier by definitional equality, so the six output fields, the carrier's goodness (restrictedGood'saxisParallelTestandselfConsistencyTest) and its point consistency (hpoint x) are passed directly, with nosimpaand noaveragedPoint_eq_of_pointMeasurement_eqdetour, and the slice outputs are chosen withchooserather than throughClassical.choose_spec. - The two
ΞΆ β€ Ξ½lemmas, which the vendored file proves twice by the samecalc, share the private theoremselfImprovementInInductionError_le_mainInductionNu_of_nonneg, which takes the nonnegativity ofeps,delta,gammaand3 β€ kΒ² Β· m_nextin place of the strategy, and proves the comparison bymul_le_mul_of_nonneg_left/_rightsteps and onelinarithfor the coefficient, given the productm_next Β· 3 β€ m_next Β· (kΒ² Β· m_next).
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
Extract the recursive answer-valued slice measurements and their averaged main-induction error bound.
Paper origin: references/ldt-paper/inductive_step.tex:441-551. After the
restricted-probabilities theorem and the predecessor answer-valued induction
hypothesis are applied to the restricted slices, this theorem packages the
resulting measurements G^x and proves the displayed bound
\mathbb E_x \sigma_x \leq \sigma.
Lean-only: This is an internal construction theorem for the simultaneous
answer-valued successor route tracked in issue #1507; it does not add a
predecessor conclusion as an assumption to any source-facing theorem.
Discharge: proved here from the restricted-probabilities theorem and the
answer-valued predecessor induction hypothesis. The model hypotheses hS hA are those the
predecessor hypothesis requires of each slice (module docstring).
Apply self-improvement to the recursive answer-valued successor slices.
Paper origin: references/ldt-paper/inductive_step.tex:461-551. Starting from
the recursive answer-valued slice measurements supplied by the predecessor
induction hypothesis, this theorem constructs the projective slice
submeasurements \widehat G^x and witnesses Z^x, proves their four
self-improvement outputs, and keeps the averaged \zeta_x and \sigma_x
bounds available.
Lean-only: The ordinary carrier appears only in the domination field, where
its point measurement is the same last-coordinate restriction of the ambient
answer-valued point measurement. The proof invokes only the
axis-parallel/self-consistency form of self-improvement, and therefore does not
claim that the carrier's dummy diagonal measurement is a good diagonal
realization of the answer-valued strategy. This internal construction is
tracked in issue #1507. Discharge: proved here from the recursive slice
measurements and the formal self-improvement theorem. The hypotheses hS hA hd are those of
the predecessor hypothesis and of the ported self-improvement theorem (module docstring).
Paper's \eqref{eq:zeta-smaller-than-nu}: under the small-parameter
hypotheses, the averaged self-improvement interface error \zeta is bounded by
the next-stage induction parameter \nu.
Answer-valued analogue of
selfImprovementInInductionError_le_mainInductionNu.
This is the scalar part of the successor proof for an ambient answer-valued strategy. It uses only the answer-valued goodness bounds and does not replace the answer-valued diagonal measurement by an ordinary one.