Phase 2 stability defect infrastructure #
Internal helper definitions and lemmas for the Phase 2 scalar bridge in ProcessedG: the
counterpart of Commutativity/ScalarApproximation/ProcessedG/PhaseTwo.lean under
MIPRE/Background/LIDT/MIPStarRE/LDT/ in the port of planning/c6b-plan.md (milestone M7,
section "Port conventions"). These definitions extract and bound the one-dimensional stability
defect controlled by gCommStability_scalar (the paper's clm:g-comm-stability), reindex the
question-level defect into the stability defect via finite marginalization, and perform the
subtraction algebra that rewrites the phase-2 insertion/removal difference as the negative
defect.
The defects are real expectations strategy.state.ev (strategy.state.L β¦ * strategy.state.R β¦)
on the symmetric model of the strategy, with the vendored arguments unchanged.
avgOver_avgOver_phaseTwo_linear takes the symmetric model S where the vendored lemma takes
the state Ο, in the same position, with F, P and R in the local algebra π.
postprocess_sandwichByOuter_prod_snd_outcome is state-free and holds in π.
The vendored hypothesis hnorm : strategy.state.IsNormalized of
evaluatedSlice_phaseTwo_stability_defect_bound is dropped, as the port conventions drop
hΟ : Ο.IsNormalized: the ported gCommStability_scalar takes none. Callers omit that argument,
which stood between zeta and family.
The proofs are shorter than the vendored ones. The pointwise subtraction of
evaluatedSlice_phaseTwo_term_diff is mul_sub, the keystone's leftTensor_mul_leftTensor,
leftTensor_sub and ev_sub, and ring on the scalars, in place of the Kronecker calc with
Matrix.smul_kronecker. avgOver_avgOver_phaseTwo_linear pulls the two averages through the
placements with ev_opTensor_averageOperatorOverDistribution_left/_right. The fiber collapse is
Finset.sum_fiberwise after ev_leftTensor_mul_middle_finset_sum, and the question average is
split by avgOver_uniform_prod_swap directly, without the vendored Equiv.prodComm reindex.
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/commutativity-G.texblueprint/src/chapter/ch08_commutativity.tex
The scalar defect controlled by gCommStability_scalar after averaging out
all evaluated-slice variables except the second slice height y.
This is the paper's boundedness witness term for clm:g-comm-stability: for a
fixed y, gCommStabilityR params family y averages the left-register sandwich
G^{u,x}_a G^y_g G^{u,x}_a, while
IdxPolyFamily.averagedSlicePointEvaluationOperator strategy y g averages the
right-register point answer A^{v,y}_{g(v)} over the tail point v.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Direct βΞΆ control of the phase-2 stability defect.
The remaining bridge from the explicit evaluated-slice difference to this
one-dimensional defect is pure finite reindexing and averaging: expand
totalSandwichFamily, decompose the sampled second point as (v,y), collect the
postprocessing fiber β_b β_{g : g(v)=b} into β_g, and average the first
sampled point into gCommStabilityR. The vendored lemma asks for a normalized state.
The still-unmarginalized phase-2 defect at a sampled evaluated-slice question.
This is the exact question-level term obtained after expanding
totalSandwichFamily and using
S * G^y.total - S = -S * (1 - G^y.total) for the left-register sandwich S.
The remaining reindexing residual averages this term to
evaluatedSlicePhaseTwoStabilityDefect.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Postprocessing a sandwiched product by its second coordinate sums over the outer outcome.
For the sandwiched submeasurement with outcomes (a, b) and effect
A_a B_b A_a, the Prod.snd postprocessing has outcome b equal to
β a, A_a B_b A_a. This is the finite-fiber identity used to recognize the
gCommStabilityR averaged sandwich.
Pull two finite averages into a bipartite expectation with averaged operators.
For a fixed polynomial outcome g, the left register is averaged over πQ
while the right register is averaged over πV. The identity rewrites the
nested scalar average of
S.ev (S.L (F q g a * R) * S.R (P g v)) into the expectation of
S.L ((E_q β_a F q g a) * R) * S.R (E_v P g v), preserving the
outer sum over g.
Reindex the pointwise phase-2 question defect by polynomial outcomes.
When the sampled second point is appendPoint v y, the postprocessed slice
outcome (evaluatedSliceSecondFactor ...).outcome b is the sum of
G^y_g over the fiber g v = b. Expanding this fiber inside the sandwiched
left-register expression and summing over b collapses the defect to a
polynomial-indexed sum whose right-register outcome is A^{v,y}_{g(v)}.
Pointwise algebra for the phase-2 subtraction.
After expanding totalSandwichFamily, the inserted summand has the extra factor
G^y.total on the left register. This lemma rewrites the difference with the
removed summand as the negative defect, using the noncommutative identity
S * T - S = -(S * (1 - T)).
Average the pointwise phase-2 algebra over evaluated-slice questions.
This proves the advertised sign rewrite
avgOver π phase1Inserted - avgOver π phase2Removed = -avgOver π questionDefect.
It leaves only the finite marginalization from the question-level defect to the
one-dimensional evaluatedSlicePhaseTwoStabilityDefect.
Exact finite reindexing identity for the phase-2 scalar bridge.
Paper origin: references/ldt-paper/commutativity-G.tex:60-83 (upstream), the finite
averaging and reindexing step leading to the scalar eq:add-an-a bridge.
This statement contains no analytic estimate. It says that the question-level
phase-2 defect averages to the one-dimensional scalar defect bounded by
gCommStability_scalar. The proof is only finite marginalization and fiber
bookkeeping: decompose the second sampled point as (v,y), collapse the
postprocessing fibers, and average the first sampled point into
gCommStabilityR.