RL-1: what entanglement does to the RECORDS — the reduced state at the record tier (Q27, second half)

Category: 7-SigmaLayer (the record layer — Q27's mixed-tier transport and the entangled two-time instantiation; specs/BACKLOG.md ▶ OPEN QUEUE #5, Q27's residue row, and the gated list of specs/two-time-luders-scoping.md).

The question, and where its first half stopped

The external reader's question (2026-08-20): for an ENTANGLED composite preparation, what are a local context's weights? CV/EntangledWeights.lean answered it at the arena level — ★★ arenaObs_leftOp_eq_reduced, arenaObs (leftOp A) x = re tr(reducedDM x · A) for every composite point, with the Bell ray's local weights exactly 1/2. What it did not do, and said so, is carry that form to the record tier: the dynamical measurement model (swapProtocol on SwapArena, mixedSwapPrep, the two-stage arena) is Fin-indexed and reads density operators through traceForm, while reducedDM lives on the field-configuration index. This module closes that gap, and then instantiates the two-time law on it.

Main results

A. The transport (index plumbing, delivered as API):

• DensityOperatorIx.toFin — an indexed density read on Fin d through a labelling e : ι ≃ Fin d of its index (the bridge LF2/ReducedDensity.lean said "should a bridge ever be needed"; this is the need); traceForm_toFin_single — the diagonal weights transport.
• reducedDensityIx x — the reduced state of a composite ray as a DensityOperatorIx, with traceForm_reducedDensityIx : (reducedDensityIx x).traceForm A = arenaObs (leftOp A) x; reducedDensity e x : DensityOperator d — the same, on Fin d, with traceForm_reducedDensity_single — the record tier's Born pairing at outcome i IS the composite arena's local observation of the pattern projector ∣e⁻¹ i⟩⟨e⁻¹ i∣.

B. The local record law (Q27 at the record tier):

• ★★ entangled_local_record_born — a local context's record weights on an entangled composite are the reduced state's Born weights, dynamically: the mixed swap preparation at reducedDensity e x gives the outcome-i sector exactly arenaObs (leftOp ∣e⁻¹ i⟩⟨e⁻¹ i∣) x — for EVERY composite point, entangled included.
• ★ entangled_local_followup — after recording i on the entangled composite, follow-up statistics in every local context are c'.rate [eᵢ]: the record fixes the local post-state, whatever the remote sector holds (mixed_luders_followup consumed).
• ★ bell_record_weight₀ / bell_record_weight₁ — the Bell ray's local records: exactly 1/2 each, on the swap arena.

C. The mixed two-time law (generic, new — mixedReadyPrep had no two-time consumer):

• mixedTwoPrep ρ — the two-stage preparation of a MIXED system: mixedReadyPrep ρ with a calibrated bank for the first measurement, fresh ready register and calibrated bank for the second.
• ★★ mixed_two_time_born — P(record i at t₁ ∧ record j at t₂) = Tr(ρ Πᵢ) · c₂.rate [eᵢ] j for every density operator ρ and every second context; mixed_two_time_first_record (no retro-action), ★ mixed_two_time_other_fate (conditioned on record i, the next partition carries the collapsed weights c₂.rate [eᵢ]).

D. The entangled two-time instantiation (the gated item of two-time-luders-scoping.md):

• ★★ entangled_two_time_born — P(local record i at t₁ ∧ record j at t₂) = arenaObs (leftOp Πᵢ) x · c₂.rate [eᵢ] j: measure a subsystem of an entangled composite, then follow up, as ONE number on one arena, with the first factor read off the composite point through reducedDM;
• ★ entangled_two_time_other_fate, ★ bell_two_time_born (the Bell ray: ½ · c₂.rate [eᵢ] j).

CSD reading

Entanglement enters the record layer in exactly one place: the preparation weights of the local swap witness are those of the reduced state, and the reduced state is mixed precisely when the composite point is entangled (reducedDM_join). Everything downstream of the weights — record creation, exclusivity, persistence, the Lüders relocation to [eᵢ], the two-time composition — is the same protocol on the same arena, untouched. So "what entanglement does to the records" is: it supplies mixed Born weights and nothing else; the remote sector's labels never reach the local records (composite_no_signalling at the arena level, and here the weights arenaObs (leftOp ·) x are the only composite input).

⚠️ Honest scope

• The local system is prepared as mixedSwapPrep (reducedDensity e x) — the spectral two-stage sampling of the reduced state, the corpus's canonical mixed preparation (MixedSwap.lean). The theorems are identities of RECORD STATISTICS: the local witness at that preparation reads exactly the composite point's local observations. The ontic composite point is pure; an apparatus coupled to ONE SECTOR OF THE COMPOSITE ARENA is the corpus's OTHER line — a local measurement IS a block-degenerate measurement (RecordLayer/LocalBlockBridge.lean, localBlock), and the join protocol's coarse Born mass (join_sector_born) at that block map is ‖localProjB j v‖² / ‖v‖² (norm_blockProj_localBlock). What is NOT stated anywhere is the identification of that composite-arena sector weight with re tr(reduceB [v] · Πⱼ) That identification landed the same day as RL-1′ (RecordLayer/CompositeRecord.lean): ★★ composite_local_record_born reads the join-protocol weight as the reduced state's Born weight, and ★★ composite_record_eq_mixed_record equates it, outcome by outcome, with the mixed- preparation record weight of this module's construction. The two lines meet at a theorem.
• The first measurement is the local computational-basis context (momentContext d through the labelling e), the second is arbitrary — the scope of the two-stage arena (TwoTimeLuders.lean).
• Rank-one local outcomes; the labelling e : FieldConfig K₁ N ≃ Fin d is quantified, so no choice of enumeration is hidden.

References

specs/BACKLOG.md (▶ OPEN QUEUE #5 = RL-1; Q27, Q25); specs/two-time-luders-scoping.md (the gated list this executes); specs/record-layer-plan.md §4; CV/EntangledWeights.lean (reducedDM, arenaObs_leftOp_eq_reduced, reducedDM_bell, bell_local_weight₀/₁, trace_mul_single); CV/CompositeArena.lean (leftOp, bellVec); LF2/ReducedDensity.lean (DensityOperatorIx), LF2/MixedEnsembleIx.lean (DensityOperatorIx.traceForm); RecordLayer/MixedSwap.lean (mixedSwapPrep, mixed_swap_sector_born), RecordLayer/MixedLuders.lean (mixedReadyPrep, mixedSwapPrep_eq_prod, mixed_outcome_pos, mixed_luders_followup); RecordLayer/TwoTimeLuders.lean (twoStagePrep, two_stage_joint, two_stage_first_record, jointRecordSector); RecordLayer/SwapClosure.lean (swap_sector_born_ctx); specs/future-work.md.

Index plumbing: an indexed density read on Fin d

theorem CSD.LF2.trace_submatrix_equiv {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (M : Matrix ι ι ℂ) (e : κ ≃ ι) : (M.submatrix ⇑e ⇑e).trace = M.trace

Traces are invariant under a simultaneous reindex of rows and columns.

theorem CSD.LF2.trace_mul_single' {ι : Type u_1} [Fintype ι] [DecidableEq ι] (M : Matrix ι ι ℂ) (a : ι) : (M * Matrix.single a a 1).trace = M a a

tr(M · ∣a⟩⟨a∣) = M a a on an arbitrary finite index.

theorem CSD.LF2.outerProduct_single {ι : Type u_1} [DecidableEq ι] (i : ι) : outerProduct (EuclideanSpace.single i 1) = Matrix.single i i 1

The rank-one projector of a standard basis vector is the matrix unit ∣i⟩⟨i∣.

noncomputable def CSD.LF2.DensityOperatorIx.toFin {ι : Type u_1} [Fintype ι] [DecidableEq ι] {d : ℕ} (e : ι ≃ Fin d) (ρ : DensityOperatorIx ι) : DensityOperator d

An indexed density read on Fin d through a labelling e : ι ≃ Fin d of its index — the bridge between the index-parametric DensityOperatorIx ι and the Fin-indexed DensityOperator d the record tier consumes.

Equations

• CSD.LF2.DensityOperatorIx.toFin e ρ = { M := ρ.M.submatrix ⇑e.symm ⇑e.symm, isHermitian := ⋯, nonneg := ⋯, trace_one := ⋯ }

@[simp]

theorem CSD.LF2.DensityOperatorIx.toFin_M {ι : Type u_1} [Fintype ι] [DecidableEq ι] {d : ℕ} (e : ι ≃ Fin d) (ρ : DensityOperatorIx ι) : (toFin e ρ).M = ρ.M.submatrix ⇑e.symm ⇑e.symm

theorem CSD.LF2.DensityOperatorIx.traceForm_toFin_single {ι : Type u_1} [Fintype ι] [DecidableEq ι] {d : ℕ} (e : ι ≃ Fin d) (ρ : DensityOperatorIx ι) (i : Fin d) : LF2.traceForm (toFin e ρ) (rankOneEffect (EuclideanSpace.single i 1) ⋯) = ρ.traceForm (Matrix.single (e.symm i) (e.symm i) 1)

The diagonal weights transport: the Fin-tier Born pairing at the basis outcome i is the indexed density's pairing at the matrix unit of the label e⁻¹ i.

The reduced state of a composite ray, at the record tier

noncomputable def CSD.RecordLayer.reducedDensityIx {K₁ K₂ N : ℕ} (x : CV.FieldArena (K₁ + K₂) N) : LF2.DensityOperatorIx (CV.FieldConfig K₁ N)

The reduced state of a composite ray as an indexed density operator — the object CV/EntangledWeights.lean delivered (reducedDM, PSD and trace one), packaged for the LF2 mixed tier.

Equations

• CSD.RecordLayer.reducedDensityIx x = { M := CSD.CV.reducedDM x, isHermitian := ⋯, nonneg := ⋯, trace_one := ⋯ }

@[simp]

theorem CSD.RecordLayer.reducedDensityIx_M {K₁ K₂ N : ℕ} (x : CV.FieldArena (K₁ + K₂) N) : (reducedDensityIx x).M = CV.reducedDM x

theorem CSD.RecordLayer.traceForm_reducedDensityIx {K₁ K₂ N : ℕ} (x : CV.FieldArena (K₁ + K₂) N) (A : Matrix (CV.FieldConfig K₁ N) (CV.FieldConfig K₁ N) ℂ) : (reducedDensityIx x).traceForm A = CV.arenaObs (CV.leftOp A) x

The mixed-tier Born pairing of the reduced state is the composite arena's local observation — arenaObs_leftOp_eq_reduced read through DensityOperatorIx.traceForm.

noncomputable def CSD.RecordLayer.reducedDensity {K₁ K₂ N d : ℕ} (e : CV.FieldConfig K₁ N ≃ Fin d) (x : CV.FieldArena (K₁ + K₂) N) : LF2.DensityOperator d

The reduced state on Fin d, through a labelling e of the local configurations — the DensityOperator d the swap witness and the two-stage arena consume.

Equations

• CSD.RecordLayer.reducedDensity e x = CSD.LF2.DensityOperatorIx.toFin e (CSD.RecordLayer.reducedDensityIx x)

theorem CSD.RecordLayer.traceForm_reducedDensity_single {K₁ K₂ N d : ℕ} (e : CV.FieldConfig K₁ N ≃ Fin d) (x : CV.FieldArena (K₁ + K₂) N) (i : Fin d) : LF2.traceForm (reducedDensity e x) (LF2.rankOneEffect (EuclideanSpace.single i 1) ⋯) = CV.arenaObs (CV.leftOp (Matrix.single (e.symm i) (e.symm i) 1)) x

The record tier's Born pairing at outcome i is the composite arena's local observation of the pattern projector ∣e⁻¹ i⟩⟨e⁻¹ i∣ — the transport the Q27 first brick declared and did not claim.

★★ The local record law on an entangled composite

theorem CSD.RecordLayer.entangled_local_record_born {K₁ K₂ N d : ℕ} [NeZero d] (e : CV.FieldConfig K₁ N ≃ Fin d) (x : CV.FieldArena (K₁ + K₂) N) (i : Fin d) : (mixedSwapPrep (reducedDensity e x)) ((swapProtocol (basinIndex (momentContext d)) ⋯).outcomeSector i) = ENNReal.ofReal (CV.arenaObs (CV.leftOp (Matrix.single (e.symm i) (e.symm i) 1)) x)

★★ A local context's record weights on an entangled composite are the reduced state's Born weights — dynamically. The mixed swap preparation at the reduced state of the composite point x gives the outcome-i sector of the local measurement protocol exactly the composite arena's local observation arenaObs (leftOp ∣e⁻¹ i⟩⟨e⁻¹ i∣) x, for EVERY composite point, entangled included: Q27's answer, stated where the records are made.

theorem CSD.RecordLayer.entangled_local_followup {K₁ K₂ N d : ℕ} [NeZero d] (e : CV.FieldConfig K₁ N ≃ Fin d) (x : CV.FieldArena (K₁ + K₂) N) (i : Fin d) (hpos : CV.arenaObs (CV.leftOp (Matrix.single (e.symm i) (e.symm i) 1)) x ≠ 0) (c' : ContextField d) (j : Fin d) : ((swapProtocol (basinIndex (momentContext d)) ⋯).postMeasure (mixedSwapPrep (reducedDensity e x)) i) ((fun (y : SwapArena (LF4.KSigma d) d) => y.1.1) ⁻¹' globalBasin c' j) = ENNReal.ofReal (c'.rate (vertexPoint i) j)

★ The record fixes the local post-state, whatever the remote sector holds. After recording i on the entangled composite's local sector, follow-up statistics in every local context c' are the collapsed state's rates c'.rate [eᵢ] — mixed_luders_followup with the positivity hypothesis read off the composite point.

theorem CSD.RecordLayer.bell_record_weight₀ {K₁ K₂ N d : ℕ} [NeZero d] (e : CV.FieldConfig K₁ N ≃ Fin d) {x₀ x₁ : CV.FieldConfig K₁ N} (hx : x₀ ≠ x₁) {y₀ y₁ : CV.FieldConfig K₂ N} (hy : y₀ ≠ y₁) : (mixedSwapPrep (reducedDensity e (Projectivization.mk ℂ (CV.bellVec x₀ x₁ y₀ y₁) ⋯))) ((swapProtocol (basinIndex (momentContext d)) ⋯).outcomeSector (e x₀)) = ENNReal.ofReal (1 / 2)

★ The Bell ray's first local record weight, on the swap arena: exactly 1/2.

theorem CSD.RecordLayer.bell_record_weight₁ {K₁ K₂ N d : ℕ} [NeZero d] (e : CV.FieldConfig K₁ N ≃ Fin d) {x₀ x₁ : CV.FieldConfig K₁ N} (hx : x₀ ≠ x₁) {y₀ y₁ : CV.FieldConfig K₂ N} (hy : y₀ ≠ y₁) : (mixedSwapPrep (reducedDensity e (Projectivization.mk ℂ (CV.bellVec x₀ x₁ y₀ y₁) ⋯))) ((swapProtocol (basinIndex (momentContext d)) ⋯).outcomeSector (e x₁)) = ENNReal.ofReal (1 / 2)

★ The Bell ray's second local record weight, on the swap arena: exactly 1/2. With bell_record_weight₀: entanglement maximally mixes the local RECORDS across the correlated patterns, and the remote labels are gone.

★★ The two-time law for a mixed preparation

noncomputable def CSD.RecordLayer.mixedTwoPrep {N : ℕ} (ρ : LF2.DensityOperator N) : MeasureTheory.Measure (TwoStageArena (LF4.KSigma N) N)

The two-stage preparation of a mixed system: mixedReadyPrep ρ (the spectral mixture of the ready preparations) with a vertex-calibrated bank for the first measurement, and a fresh ready register with a vertex-calibrated bank for the second.

Equations

• One or more equations did not get rendered due to their size.

instance CSD.RecordLayer.instIsProbabilityMeasureTwoStageArenaKSigmaMixedTwoPrep {N : ℕ} (ρ : LF2.DensityOperator N) : MeasureTheory.IsProbabilityMeasure (mixedTwoPrep ρ)

theorem CSD.RecordLayer.mixed_two_time_born {N : ℕ} [NeZero N] (ρ : LF2.DensityOperator N) (i : Fin N) (hpos : LF2.traceForm ρ (LF2.rankOneEffect (EuclideanSpace.single i 1) ⋯) ≠ 0) (c₂ : ContextField N) (j : Fin N) : (mixedTwoPrep ρ) (jointRecordSector (basinIndex (momentContext N)) (basinIndex c₂) i j) = ENNReal.ofReal (LF2.traceForm ρ (LF2.rankOneEffect (EuclideanSpace.single i 1) ⋯)) * ENNReal.ofReal (c₂.rate (vertexPoint i) j)

★★ The two-time Born law for a mixed preparation, on one arena. For every density operator ρ, measured in the computational basis at t₁ and in an ARBITRARY context c₂ at t₂:

P(record i at t₁ ∧ record j at t₂) = Tr(ρ Πᵢ) · c₂.rate [eᵢ] j.

The first factor is the mixed dynamical Born weight (mixed_swap_sector_born); the second is the Born weight of the collapsed state [eᵢ] — the record erases the classical ignorance of the preparation (mixed_luders_followup's content), now as one number on the two-stage arena.

theorem CSD.RecordLayer.mixed_two_time_first_record {N : ℕ} [NeZero N] (ρ : LF2.DensityOperator N) (c₂ : ContextField N) (i : Fin N) : (mixedTwoPrep ρ) (twoStage (basinIndex (momentContext N)) (basinIndex c₂) ⁻¹' recordOneEvent i) = ENNReal.ofReal (LF2.traceForm ρ (LF2.rankOneEffect (EuclideanSpace.single i 1) ⋯))

The stage-1 record marginal of a mixed preparation: composing does not disturb the mixed Born law.

theorem CSD.RecordLayer.mixed_two_time_other_fate {N : ℕ} [NeZero N] (ρ : LF2.DensityOperator N) (i : Fin N) (hpos : LF2.traceForm ρ (LF2.rankOneEffect (EuclideanSpace.single i 1) ⋯) ≠ 0) (c₂ : ContextField N) (j : Fin N) : (mixedTwoPrep ρ)[twoStage (basinIndex (momentContext N)) (basinIndex c₂) ⁻¹' recordTwoEvent j | twoStage (basinIndex (momentContext N)) (basinIndex c₂) ⁻¹' recordOneEvent i] = ENNReal.ofReal (c₂.rate (vertexPoint i) j)

★ The fate of the other Ω_j for a mixed preparation. CONDITIONED on record i at t₁, the probability of record j at t₂ is the collapsed state's rate c₂.rate [eᵢ] j — independent of ρ: the record, not the pedigree, fixes the next partition.

★★ The entangled two-time instantiation

theorem CSD.RecordLayer.entangled_two_time_born {K₁ K₂ N d : ℕ} [NeZero d] (e : CV.FieldConfig K₁ N ≃ Fin d) (x : CV.FieldArena (K₁ + K₂) N) (i : Fin d) (hpos : CV.arenaObs (CV.leftOp (Matrix.single (e.symm i) (e.symm i) 1)) x ≠ 0) (c₂ : ContextField d) (j : Fin d) : (mixedTwoPrep (reducedDensity e x)) (jointRecordSector (basinIndex (momentContext d)) (basinIndex c₂) i j) = ENNReal.ofReal (CV.arenaObs (CV.leftOp (Matrix.single (e.symm i) (e.symm i) 1)) x) * ENNReal.ofReal (c₂.rate (vertexPoint i) j)

★★ Measure a subsystem of an entangled composite, then follow up — as one number on one arena. With the local system prepared at the reduced state of the composite point x, measured in the local computational basis at t₁ and in an ARBITRARY local context c₂ at t₂:

P(local record i at t₁ ∧ record j at t₂) = arenaObs (leftOp ∣e⁻¹ i⟩⟨e⁻¹ i∣) x · c₂.rate [eᵢ] j.

The first factor is the composite arena's own local observation (reducedDM read on the pattern projector); the second is the collapsed state's Born weight. The gated item of specs/two-time-luders-scoping.md, delivered.

theorem CSD.RecordLayer.entangled_two_time_first_record {K₁ K₂ N d : ℕ} [NeZero d] (e : CV.FieldConfig K₁ N ≃ Fin d) (x : CV.FieldArena (K₁ + K₂) N) (c₂ : ContextField d) (i : Fin d) : (mixedTwoPrep (reducedDensity e x)) (twoStage (basinIndex (momentContext d)) (basinIndex c₂) ⁻¹' recordOneEvent i) = ENNReal.ofReal (CV.arenaObs (CV.leftOp (Matrix.single (e.symm i) (e.symm i) 1)) x)

The stage-1 local record marginal on the entangled composite: the second apparatus cannot retro-act on the reduced state's Born law.

theorem CSD.RecordLayer.entangled_two_time_other_fate {K₁ K₂ N d : ℕ} [NeZero d] (e : CV.FieldConfig K₁ N ≃ Fin d) (x : CV.FieldArena (K₁ + K₂) N) (i : Fin d) (hpos : CV.arenaObs (CV.leftOp (Matrix.single (e.symm i) (e.symm i) 1)) x ≠ 0) (c₂ : ContextField d) (j : Fin d) : (mixedTwoPrep (reducedDensity e x))[twoStage (basinIndex (momentContext d)) (basinIndex c₂) ⁻¹' recordTwoEvent j | twoStage (basinIndex (momentContext d)) (basinIndex c₂) ⁻¹' recordOneEvent i] = ENNReal.ofReal (c₂.rate (vertexPoint i) j)

★ The fate of the other local Ω_j on an entangled composite. CONDITIONED on the local record i at t₁, the next local partition carries the collapsed weights c₂.rate [eᵢ] — the remote sector, and the entanglement, have no further say.

theorem CSD.RecordLayer.bell_two_time_born {K₁ K₂ N d : ℕ} [NeZero d] (e : CV.FieldConfig K₁ N ≃ Fin d) {x₀ x₁ : CV.FieldConfig K₁ N} (hx : x₀ ≠ x₁) {y₀ y₁ : CV.FieldConfig K₂ N} (hy : y₀ ≠ y₁) (c₂ : ContextField d) (j : Fin d) : (mixedTwoPrep (reducedDensity e (Projectivization.mk ℂ (CV.bellVec x₀ x₁ y₀ y₁) ⋯))) (jointRecordSector (basinIndex (momentContext d)) (basinIndex c₂) (e x₀) j) = ENNReal.ofReal (1 / 2) * ENNReal.ofReal (c₂.rate (vertexPoint (e x₀)) j)

★ The Bell ray's two-time law: record the first correlated pattern locally, then follow up in any local context — ½ · c₂.rate [e_{x₀}] j.