Section 8 global variance: collision expansion and Schwartz–Zippel bounds #
The counterpart of
MIPRE/Background/LIDT/MIPStarRE/LDT/GlobalVariance/Theorems/CollisionExpansion.lean in the
port of planning/c6b-plan.md (milestone M6, section "Port conventions"): the lem:generalize-b
wrappers (generalizeB_of_pointwise, generalizeB), the expansion of the line-collision
residual over line/parameter seeds, and its Schwartz–Zippel bound by m·d/q
(generalizeBPointwiseSchwartzZippel, generalizeBFromSchwartzZippel).
opTensor is strategy.state.opTensor, ev ψ is V.ev or strategy.state.ev, and the
vendored second state ψbi is a vector state V : VecState K in the same argument position, as
in Defs/Families.lean and Theorems/Statements.lean; callers pass strategy.state. The
normalization ev 1 = 1 of the strategy's state is the keystone's hypothesis-free
ev_one_of_isNormalized, so the vendored strategy.isNormalized argument disappears.
The reparametrizations of the line-question distribution and the Schwartz–Zippel coefficient
bound are statements about distributions and polynomials alone; this file imports the vendored
file for them and names them through an explicit open list.
Not ported #
axisParallelLineQuestionParameterEquiv: classical, imported.avgOver_axisParallelLineQuestionDistribution: classical, imported.axisParallelLinePointParamEquiv: classical, imported.avgOver_axisParallelLinePointParam: classical, imported.avgOver_axisParallelLineQuestionDistribution_to_axisParallelTestSample: classical, imported.generalizeBLineCollisionCoefficient_le: classical, imported.
References #
In LionSR/MIPStarRE at commit 507e8122, not in this repository:
references/ldt-paper/expansion.texblueprint/src/chapter/ch06_variance.tex
lem:generalize-b from its pointwise deviation bound: the aggregated families are close in
SDDRel, and the polynomial average of the deviations obeys the same bound.
lem:generalize-b.
Expanding the postprocessed collision event at the seeded question
(ℓ, ℓ(t)) gives the line-answer sum from expansion.tex, lines 283--286.
Positivity of the tensor mass appearing in the line-collision expansion.
The total tensor mass left after summing over line answers is at most one.
This is the normalization half of expansion.tex, lines 286--288: the
left-register line measurement sums to its total operator, the right-register
operator is the single submeasurement outcome G_g ≤ 1, and the strategy state
is normalized.
Commuting the uniform parameter average past the finite sum over line answers.
This is the purely finite-sum bookkeeping between the paper's seed average over
(ℓ,t) and the coefficient-weighted display in expansion.tex, lines 286--288.
The incident-question collision residual is exactly the uniform line/parameter
seed expansion from expansion.tex, lines 286--288.
The proof reindexes the axis-parallel line-test distribution by (ℓ,t) with
sampled point u = ℓ(t), then expands the ProjMeas.postprocess fiber for the
collision event f(t) = g|_ℓ(t) and f ≠ g|_ℓ.
The explicit line/parameter collision expansion is bounded by m*d/q.
This proves the Schwartz--Zippel and normalization parts of the residual estimate
from expansion.tex, lines 286--288. The preceding
generalizeBCollisionResidual_eq_seedCollisionExpansion theorem supplies the
incident-question/postprocess identity needed to apply this bound to the original
collision residual.
The uniform line/parameter seed collision expansion is bounded by m*d/q.
The proof first commutes the finite seed average into the coefficient-weighted line expansion, then applies the Schwartz--Zippel coefficient bound and tensor normalization estimate above.
The pointwise collision residual in lem:generalize-b is bounded by m*d/q.
This combines the incident-question reindexing with the seed/line expansion,
Schwartz--Zippel coefficient bound, and submeasurement-normalization estimate
from expansion.tex, lines 281--288.
Pointwise Schwartz--Zippel bound for the strategy-state form of
lem:generalize-b.
This is the paper's estimate at expansion.tex, lines 281--288, after the
projective expansion converts the squared norm into the collision residual.
lem:generalize-b for the strategy state, with the pointwise
Schwartz--Zippel estimate discharged internally. The good-strategy hypothesis is
kept in the statement to match the paper context of expansion.tex,
lines 271--288, although the algebraic Schwartz--Zippel proof itself does not
use ε, δ, or γ.