Section 6 â Definitions #
Restriction maps, the restricted strategy, its failure surrogates and the tensor-failure
expectation of the induction step: the counterpart of
MIPRE/Background/LIDT/MIPStarRE/LDT/MainInductionStep/Defs.lean in the port of
planning/c6b-plan.md (milestone M4, section "Port conventions").
A strategy here is a SymStrat params.next đ K (Co/Test/StrategyCore.lean): the local
operators live in the C*-algebra đ, the state is a symmetric model strategy.state : SymModel đ K. Restricting a strategy to the slice at height x reindexes its measurement
families and keeps its state, as in the vendored file. The restricted strategy
RestrictedSymStrat keeps the vendored fields except isNormalized, which is a theorem of the
model (RestrictedSymStrat.isNormalized); the vendored AnswerSymStrat fields permInvState
and densityFixed, set by xRestrictedAnswerSymStrat, are not fields of the ported
AnswerSymStrat (Co/Test/StrategyCore.lean).
The vendored tensorFailureExpectation is stated for a state on a product ΚA à ΚB of two
carriers. Its vendored uses (MainInductionStep/Theorems/{PastingAssembly, SelfImprovementAssembly}) apply it to the state of a symmetric strategy, so here it is narrowed
to one local algebra in a symmetric model, S.ev (S.L Z * S.R (1 - H.total)), as M3 narrowed the
heterogeneous triangle lemmas (planning/c6b-plan.md, "Departures in M3 and M5").
The classical half of the vendored file (the answer lift and its equivalence, the canonical
diagonal representative, the error constants and the slice weights) is not ported: this file
imports the vendored file and names those declarations through an explicit
open MIPStarRE.LDT.MainInductionStep (âĻ) list.
Not ported #
liftAxisAnswer: classical, imported.axisLinePolynomialEquiv: classical, imported.diagonalValueRepresentative: classical, imported.mainInductionNu: classical, imported.mainInductionError: classical, imported.selfImprovementInInductionError: classical, imported.ldPastingInInductionNu: classical, imported.ldPastingInInductionError: classical, imported.sliceTransverseDirectionWeight: classical, imported.sliceConditioningLoss: classical, imported.
Ported elsewhere #
The field isNormalized of RestrictedSymStrat is the theorem RestrictedSymStrat.isNormalized
below.
References #
In LionSR/MIPStarRE at commit 507e8122, not in this repository:
references/ldt-paper/inductive_step.tex
Restricted slice data keeps the point and axis-parallel measurements complete, and packages a genuine projective measurement on the slice's diagonal answer space.
The paper's outcome-level formula would send a slice polynomial f to the
ambient outcome append_x(f). With the current ambient diagonal answer
encoding, that map is not total on all ambient outcomes, so here we preserve the
verifier-visible base-point readout used in Chapter 10 instead: first
postprocess the ambient slice-preserving diagonal measurement to its value at
zeroCoord in F_q, then re-embed that F_q-valued projective measurement
into the honest slice answer space DiagonalLinePolynomial params using
canonical representatives.
The vendored field isNormalized is a theorem of the symmetric model state
(RestrictedSymStrat.isNormalized).
- state : SymModel đ K
The bipartite state carried by the restricted strategy.
- pointMeasurement : IdxProjMeas (MIPStarRE.LDT.Point params) (MIPStarRE.LDT.Fq params) đ
The restricted point measurement.
- axisParallelMeasurement : AxisParallelCovariantMeasurement params đ
The restricted axis-parallel line measurement, packaged with transport covariance.
- diagonalMeasurement : IdxProjMeas (MIPStarRE.LDT.DiagonalLine params) (MIPStarRE.LDT.DiagonalLinePolynomial params) đ
The restricted diagonal-line measurement on the honest slice answer space.
Instances For
The state of a restricted strategy is normalized (the vendored field
RestrictedSymStrat.isNormalized, a theorem of the model).
Sampled point answers in the axis-parallel lines test.
Point player receives u (base point) and answers at u.
Equations
Instances For
Sampled line answers in the axis-parallel lines test,
evaluated at the base point u (parameter zeroCoord).
Equations
Instances For
Sampled point answers in the j-restricted diagonal test.
Point player receives u and answers at u.
Equations
- strategy.restrictedDiagonalPointAnswerFamily j = MIPRE.LIDT.Co.diagonalPointAnswerFamilyOf strategy.pointMeasurement j
Instances For
Sampled diagonal-line answers in the j-restricted diagonal
test, evaluated at the base point (parameter zeroCoord).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Failure surrogate for the axis-parallel lines test.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Failure surrogate for the self-consistency test.
Equations
- strategy.selfConsistencyFailureProbability = strategy.state.bipartiteSSCError (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurement.toIdxSubMeas
Instances For
Failure surrogate for the diagonal lines test.
Averages over restriction index j, then the
j-restricted diagonal test.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Goodness data for a restricted strategy.
The restricted axis-parallel test fails with probability at most
eps.The restricted self-consistency test fails with probability at most
delta.The restricted diagonal-line test fails with probability at most
gamma.
Instances For
Restrict an axis-parallel line measurement to the slice at height x.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Restricting an axis-parallel measurement reindexes outcomes by slice extension.
The restricted axis-parallel measurement is transport-covariant.
Restrict a diagonal-line measurement to the slice at height x.
This is not literally the paper's outcome reindexing
f âĻ DiagonalLinePolynomial.appendAtHeight params f x; that map only covers the
degree-params.m * params.d ambient outcomes. Instead we preserve the only
statistic used by the restricted diagonal test formalized here, namely the
base-point answer at zeroCoord: restrict the ambient line question to the slice-preserving
line, postprocess the ambient projective measurement to its zeroCoord value in F_q, and
re-embed that F_q-valued projective measurement into the honest slice answer space via
diagonalValueRepresentative.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Restrict a diagonal-line measurement to the slice at height x, using the
paper-level function-answer alphabet.
Unlike restrictDiagonalMeasurement, this keeps the whole line answer function
rather than only the value at zeroCoord. The map is total because
DiagonalLineAnswer has no degree-bound subtype proof to preserve.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Transport covariance for the function-valued restricted diagonal-line measurement.
The x-restricted strategy with function-valued diagonal-line
answers.
This matches the slice-restriction interface in inductive_step.tex, lines
436--455. It is kept parallel to xRestrictedStrategy, whose diagonal field uses the
degree-bounded answer alphabet and therefore only preserves the sampled
base-point readout.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The function-answer restricted strategy reuses the ambient bipartite state.
The function-answer restricted strategy reindexes point questions by appending the slice height.
The function-answer restricted strategy has the parent's normalization (the vendored statement equates the two normalization witnesses; here both are the model's).
The function-answer restricted diagonal measurement is the answer-valued restriction of the ambient diagonal measurement.
Evaluating the answer-valued restricted diagonal measurement at the base point recovers the ambient slice-preserving diagonal readout.
The x-restricted strategy from the proof of the main induction theorem.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Restricting a strategy does not change its bipartite state.
Restricting a strategy keeps the parent's normalization (the vendored statement equates the two normalization witnesses; here both are the model's).
Restricting a strategy reindexes point questions by appending the slice height.
Postprocessing the restricted diagonal measurement at the base point recovers exactly the ambient slice-preserving diagonal answer distribution at the base point.
Tensor-failure expectation in a symmetric model:
â¨Î¨| (Z â I)(I â (I - ÎŖ H_a)) |ΨâŠ, with Z on the first factor and H on the second.
The vendored definition allows a state on two different carriers; its uses are all on the state of a symmetric strategy, so it is stated with one local algebra (module docstring).