Main scalar chain assembly #
The core lemma evaluatedSlice_scalar_chain_bound that assembles the ten-step scalar
approximation chain for lem:comm-data-processed-g: the counterpart of
Commutativity/ScalarApproximation/ProcessedG/MainChain.lean under
MIPRE/Background/LIDT/MIPStarRE/LDT/ in the port of planning/c6b-plan.md (milestone M7,
section "Port conventions"). Phases 1, 3, 4, 6–7 and 8–9 are supplied by the reverse and tail
parts of the paper chain; Phase 2 uses the reindexing of ProcessedG/PhaseTwo.
The endpoints are real expectations strategy.state.ev (strategy.state.L … * strategy.state.R …)
on the symmetric model of the strategy, and the families C of the point-swap lemmas are joint
operators K →L[ℂ] K, with star for the vendored ᴴ. The vendored
evaluatedSlicePointSwapRightPrefix places its prefix with leftTensor (ι₂ := ι), which needs no
state; here the placement is S.L, so it and
evaluatedSlice_pointSwap_right_prefix_normalization take the symmetric model S as an explicit
first argument, as M1's placement helpers do (planning/c6b-plan.md, "Departures in M1").
The vendored hypothesis hnorm : strategy.state.IsNormalized is dropped from
evaluatedSlice_pointSwap_right_bound_of_norms (where it stood between gamma and hcomm) and
from evaluatedSlice_scalar_chain_bound (between gamma zeta and hcomm), as the port
conventions drop hψ : ψ.IsNormalized; no lemma the chain calls takes it. The unused hypothesis
_hself of evaluatedSlice_scalar_chain_bound is kept, so that callers pass the vendored
argument list without hnorm.
The proofs are shorter than the vendored ones. The point measurement is
evaluatedSlicePointMeas itself, not a cast of strategy.pointMeasurement; the transfer of
prop:cons-sub-meas to the two question coordinates is avgOver_uniform_fst/_snd, as in
EvaluatedSliceCommutation/Consequences. The placement algebra of phases 3–4 is the keystone's
opTensor_mul_leftTensor and opTensor_mul, in place of the vendored simp calls with
opTensor_mul and mul_assoc, and the final assembly reads each phase bound through
abs_sub_le_iff and closes by linarith.
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 phase-four endpoint before the right-register point swap:
∑_{ab} ⟨ψ, C_{ab} (I ⊗ A^{q₂}_b A^{q₁}_a) ψ⟩.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The phase-four endpoint after the right-register point swap:
∑_{ab} ⟨ψ, C_{ab} (I ⊗ A^{q₁}_a A^{q₂}_b) ψ⟩.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Shared left-register prefix for the ProcessedG right-register point-swap bounds:
(G^{u,x}_a G^{v,y}_b T_q) ⊗ I, placed by S.L.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Normalization for the shared ProcessedG right-register point-swap prefix.
The right-register point swap, for any two endpoints whose averages are those of
evaluatedSlicePhaseFourInserted and evaluatedSlicePhaseFourSwapped.
Scalar approximation chain for the evaluated-slice commutation.
This is the core of the paper's proof of lem:comm-data-processed-g
(references/ldt-paper/commutativity-G.tex, lines 72–131, upstream).
Starting from E[∑ ABAB], the proof applies ten approximation steps:
≈_{2√ζ}: insert Bob's measurement viaclosenessOfIP+eq:add-an-a≈_{√ζ}: remove trailingG^y(clm:g-comm-stability)≈_{2√ζ}: insert Bob's second measurement viaclosenessOfIP+eq:add-an-a≈_{6√(γ(m+1))}: swap Bob's measurements viaclosenessOfIP+commutativityPoints5a.≈_{6√(γ(m+1))}: the point-measurement swap contribution internal to the paper'sclm:g-comm-stability2accounting 5b.≈_{√ζ}: remove trailingG^xby the boundedness part ofgCommStabilityTwo_raw_scalar6–7.≈_{2√ζ + 2√ζ}: reverse theeq:add-an-ainsertions 8–9.≈_{√ζ + √ζ}: apply postprocessed self-consistency twice
Summing: Σεᵢ = 12√ζ + 12√(γ(m+1)), so 2 * Σεᵢ ≤ 48m(√γ + √ζ). The chain ends at BAB,
whose average is that of ABA by the swap of the question coordinates
(evaluatedSliceCommutation_avg_swap_terms).