SigmaLayer/LocalBlockBridge: a local measurement IS a block measurement (brick 2) #
Category: dynamical measurement — dynamical no-signalling (A6, dynamical form), brick 2: the index bridge that hands brick 1's statics to the dynamical block machinery.
The composite index Fin nA × Fin nB and the flat index Fin (nA·nB) are identified by
finProdFinEquiv. Under that identification, the block structure of a local
B-measurement is the second projection (localBlock), and the degenerate-Lüders
machinery's block projector is the local projector:
toComposite (blockProj localBlock j u) = localProjB j (toComposite u)
(toComposite_blockProj),
with the transport an isometric reindexing (norm_toComposite), so the block Born weights
are the local Born weights (norm_blockProj_localBlock).
★★ Dynamical no-signalling (reduceA_blockLuders_mixture): stated in the dynamics' own
vocabulary — the post-states [blockProj localBlock j u] and the weights ‖blockProj j u‖²/‖u‖²
are exactly what the join witness delivers: joinWitness_blockLuders inhabits
BlockLudersObligation localBlock, whose conclusion says the outcome-j-conditioned
post-measurement marginal is epistemicMeasure [blockProj localBlock j u], and the sector
weights are the coarse-grained Born weights (degenerate_selector_born). The theorem: the
Born-weighted mixture of the A-marginals of those dynamically-produced post-states equals
the A-marginal of the preparation. Alice's density matrix — hence every statistic on her
side — is invariant under Bob's measurement as realised by the corpus's own
Liouville-preserving record dynamics, not merely under a Lüders map written on paper.
⚠️ Honest scope. The composition here is at the level of the states and weights the
obligation names; the full measure-level form — pushing reduceA through the join
protocol's conditioned ensemble as one integral — and the eraser process (mark, then erase,
sequentially) are brick 3, the row's remaining work. localBlock's blocks all have
dimension nA; nondegenerate B-measurements are the nA = 1 corner, as expected.
References #
specs/BACKLOG.md (the dynamical no-signalling + eraser row); specs/future-work.md;
specs/reconstruction-status.md §2 (A6). Reused corpus API: localProjB +
reduceA_localLuders_mixture (SigmaLayer/LocalLuders.lean), blockProj +
BlockLudersObligation (SigmaLayer/DegenerateLuders.lean), joinWitness_blockLuders
(SigmaLayer/JoinLuders.lean), finProdFinEquiv (Mathlib).
The index bridge #
The block structure of a local B-measurement: under finProdFinEquiv, outcome
blocks are the fibres of the second projection. Every block has dimension nA.
Equations
- CSD.RecordLayer.localBlock nA nB i = (finProdFinEquiv.symm i).2
Instances For
Transport a flat-index vector to the composite index by pulling back along
finProdFinEquiv.
Equations
- CSD.RecordLayer.toComposite u = WithLp.toLp 2 fun (ak : Fin nA × Fin nB) => u.ofLp (finProdFinEquiv ak)
Instances For
The transport is an isometric reindexing.
The bridge: block projector = local projector #
★ The degenerate-Lüders block projector of localBlock IS the local B-projector,
under the index transport. A local measurement is a block-degenerate measurement — as a
definitional identity, not an analogy.
The block Born weights are the local Born weights.
Dynamical no-signalling #
★★ Dynamical no-signalling: the Born-weighted mixture of the A-marginals of the
post-states the join witness delivers for a local B-measurement equals the A-marginal of
the preparation. The post-states [blockProj localBlock j u] and weights ‖·‖²/‖u‖² are
those of BlockLudersObligation localBlock — inhabited dynamically by
joinWitness_blockLuders — and of degenerate_selector_born; nothing here is a paper
Lüders map.