Point-event self-consistency transport #
The counterpart of
MIPRE/Background/LIDT/MIPStarRE/LDT/GlobalVariance/Theorems/SelfConsistencyTransport/Point.lean
in the port of planning/c6b-plan.md (milestone M6, section "Port conventions"): the point
self-consistency endpoints of the six-step local-variance transport chain in
lem:local-variance-of-points (expansion.tex, lines 300--311). These are the first and last
2δ moves; the point-line 2ε moves live in PointLine.lean.
The vendored proofs apply the two notions of self-consistency to a permutation-invariant state,
strategy.permInvState; here the swap symmetry is a theorem of the model and that argument
disappears (Preliminaries.twoNotionsOfSelfConsistency,
Preliminaries.twoNotionsOfSelfConsistencyAfterEvaluation). The self-consistency hypothesis
BipartiteSSCRel is the selfConsistencyTest field of IsGood itself.
The proofs are shorter than the vendored ones. The single-polynomial endpoint
pointConditionedEventSelfConsistency_weighted_point is one nonnegative summand of the grouped
endpoint pointConditionedEventSelfConsistency_weighted_point_sum, so it is derived from it
rather than from a separate application of cabApproxDelta; the grouped endpoint is
cabApproxDelta_sum_from_sdd on the lifted point measurements, with the bridges
S.rightTensor_mul_leftTensor_eq_opTensor and S.rightTensor_mul_rightTensor.
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/expansion.tex
Good-strategy interfaces for the local-variance transport chain #
The 2δ self-consistency interface for the point event A^u_{g(u)}.
This is the evaluated, two-outcome version of the first/last moves in
lem:local-variance-of-points (expansion.tex, lines 305--306 and 310--311):
postprocess the point measurement by the event a = g(u), then apply
prop:two-notions-of-self-consistency-after-evaluation to the good-strategy
self-consistency branch.
Grouped-by-evaluation-value endpoint for the first self-consistency move in
lem:local-variance-of-points.
This is the sum-level analogue of pointConditionedEventSelfConsistency_weighted_point.
It follows the transport at references/ldt-paper/expansion.tex, lines
305--306, but first groups all polynomials with the same value g(u). The
multiplier family is 0 away from the fiber a = g(u) and is
S.R ((G_g)^{1/2}) on that fiber, so the cabApproxDelta contraction is supplied
by the submeasurement inequality ∑_{g : g(u)=a} G_g ≤ I. Consequently the
bound is 2δ for the polynomial sum, with no polynomial-cardinality loss.
The first self-consistency move in lem:local-variance-of-points, after
applying prop:cab-approx-delta with the multiplier S.R ((G_g)^{1/2}) but
before pulling the point marginal to the hypercube-edge distribution.
This proves the weighted native-distribution version of expansion.tex,
lines 305--306:
A^u_{g(u)} ⊗ (G_g)^{1/2} ≈_{2δ} I ⊗ (G_g)^{1/2} A^u_{g(u)}. It is one nonnegative summand of
pointConditionedEventSelfConsistency_weighted_point_sum.
Sum-level first self-consistency endpoint on the hypercube-edge sampler.
This is the u-endpoint version of references/ldt-paper/expansion.tex, lines
305--306, after grouping polynomials by the common value g(u) before applying
cabApproxDelta. It is the edge-distribution form of
pointConditionedEventSelfConsistency_weighted_point_sum.
The final weighted self-consistency move on the target endpoint of the hypercube edge distribution.
This is the symmetric line-310 to line-311 substep of
lem:local-variance-of-points: after the second marginal reindexing,
I ⊗ (G_g)^{1/2} A^v_{g(v)} is 2δ-close to
A^v_{g(v)} ⊗ (G_g)^{1/2}.
Sum-level final self-consistency endpoint on the hypercube-edge sampler.
This is the v-endpoint version of references/ldt-paper/expansion.tex, lines
310--311. The second marginal of rerandomizeCoord is uniform, and the squared
difference is unchanged after swapping the two endpoint operators.