RL-1′: the composite-arena seam of Q27 — a local record on a pure composite reads the reduced state #
Category: 7-SigmaLayer (the record layer — Q27's composite-arena form; specs/BACKLOG.md
▶ OPEN QUEUE #25, the residue RecordLayer/EntangledRecord.lean declared).
What this closes #
RL-1 answered the external reader's question at the record tier by preparing the local system
as the mixed swap preparation of the reduced state, and the honest-scope note said what that
leaves open. The ontic composite point is pure, so a sceptic can say the local system was
modelled as a classical mixture rather than measured. The corpus already has the other
construction, an apparatus coupled to one sector of the composite arena: a local measurement IS
a block-degenerate measurement (LocalBlockBridge.lean, localBlock), and the join protocol
delivers its record dynamics with the coarse Born mass join_sector_born. What nobody had
stated is that this mass is the reduced state's Born weight. This module states it, and then
puts the two constructions side by side in one equation.
Main results #
localBlock_sum_normSq— the join protocol's block sum atlocalBlockreindexes alongfinProdFinEquivto∑ₐ ‖u(a, j)‖²;rayDensity_posSemidef,rayDensityIx,reduceBDensity— the density of a composite ray as an indexed density operator, and Bob's reduced statereduceBas aDensityOperator nB(throughDensityOperatorIx.reducedLeftand RL-1'stoFin);reduceB_diag_re— its diagonal entry is∑ₐ ‖v(a, j)‖² / ‖v‖²;- ★★
composite_local_record_born— on the composite arena, the record weight of Bob's outcomejis the reduced state's Born weight: for every unit composite vectoru, the join protocol atlocalBlockgives the outcome-jsector exactlyre (reduceB [u]) j j, which isre tr(reduceB [u] · ∣j⟩⟨j∣)(composite_local_record_born_trace) andTr(ρ_B ∣j⟩⟨j∣)in the LF2 pairing (composite_local_record_born_traceForm); - ★★
composite_record_eq_mixed_record— the two lines meet at a theorem: the composite- arena record weight (a pure composite point, an apparatus on one sector, the join protocol) equals the local mixed-preparation record weight (mixedSwapPrepatreduceBDensity, the swap protocol), outcome by outcome. The classical-mixture reading and the ontic reading give the same records, and now that's a proved identity rather than two numbers that happen to agree.
CSD reading #
Bob's apparatus couples to his sector of a pure composite point and the dynamics sorts the
composite into blocks. The block a run lands in is his record, and the weights of the blocks
are exactly the diagonal of his reduced state, so his records carry the entanglement's local
effect and nothing else. Alice's labels never enter (reduceA_blockLuders_mixture is the
dynamical no-signalling half of the same construction). The mixed swap preparation of RL-1 is
the epistemic description of the same records, and the two agree because both are the reduced
state's Born weights.
⚠️ Honest scope #
- Bob's outcomes are the computational basis of his factor, the block structure
localBlockfixes. A rotated local context isbasisContexton the swap side and the corresponding block structure on the join side, and isn't restated here. - The
Fin nA × Fin nBindex of the no-signalling line, not the field-configuration index of the CV composite arena. RL-1'sreducedDensityand this module'sreduceBDensityare the same construction on two index conventions, and a bridge between them is index plumbing nobody has needed. - The follow-up after Bob's record is
joinWitness_blockLudersatlocalBlock(the composite collapses to[Πⱼ u]); that its reduced state is Bob's Lüders-updated state is not stated.
References #
specs/BACKLOG.md (▶ OPEN QUEUE #25; Q27); RecordLayer/EntangledRecord.lean (RL-1, the
honest-scope note this discharges; DensityOperatorIx.toFin, trace_mul_single');
RecordLayer/LocalBlockBridge.lean (localBlock, toComposite, norm_blockProj_localBlock);
RecordLayer/LocalLuders.lean (localProjB); RecordLayer/OnticMarginals.lean (rayDensity,
reduceB, normSq_eq_sum_mul_star); RecordLayer/JoinClosure.lean (join_sector_born);
RecordLayer/MixedSwap.lean (mixed_swap_sector_born); LF2/ReducedDensity.lean
(DensityOperatorIx.reducedLeft); specs/future-work.md.
The block sum at localBlock is Bob's diagonal weight #
The join protocol's block sum at localBlock, reindexed along finProdFinEquiv: the
outcome-j block carries ∑ₐ ‖u(a, j)‖².
Bob's reduced state as a density operator #
The ray density is a nonnegative multiple of ∣v⟩⟨v∣.
The ray density is positive semidefinite.
The density of a composite ray as an indexed density operator.
Equations
- CSD.RecordLayer.rayDensityIx p = { M := CSD.RecordLayer.rayDensity p, isHermitian := ⋯, nonneg := ⋯, trace_one := ⋯ }
Instances For
Bob's reduced state as a Fin-indexed density operator: reduceB, through
DensityOperatorIx.reducedLeft and the identity labelling.
Equations
Instances For
The Born pairing of Bob's reduced state at outcome j is its diagonal entry.
★★ The composite-arena record weight is the reduced state's Born weight #
★★ On the composite arena, Bob's record weight is his reduced state's Born weight. For
a unit composite vector u, the join protocol with the local block structure localBlock
gives the outcome-j sector exactly re (reduceB [u]) j j, for every composite point, entangled
included, and independently of the ancilla calibration α.
The same, in the trace form re tr(reduceB [u] · ∣j⟩⟨j∣) RL-1's bridge reads.
The same, as the LF2 Born pairing Tr(ρ_B ∣j⟩⟨j∣) of Bob's reduced density operator.
★★ The two lines meet #
★★ The composite-arena record and the mixed-preparation record agree, outcome by outcome. The join protocol on the pure composite point (an apparatus coupled to Bob's sector) and the swap protocol on the mixed preparation of Bob's reduced state (RL-1's local witness) give every outcome the same weight. The ontic reading and the classical-mixture reading of "measure Bob's subsystem" are the same records.