Empirical/CSD/EraserDynamics: the eraser as two local measurements (brick 3b)

Category: empirical CSD twin, dynamical tier — the eraser process, closing the dynamical no-signalling + eraser row.

QuantumEraserVolume certifies the eraser's statistics (conditional fringes, the exact dark-fringe zero) on the conditioned states eraserOut. This module derives those conditioned states from the measurement machinery itself: the marker measurements are the local Lüders maps of LocalLuders/LocalLudersBasis applied to the Bell path–marker state, in the two bases the eraser story needs.

• The joint state: bellE, the corpus's |00⟩ + |11⟩ as a Euclidean vector; its B slices are the computational rays (sliceB_bellE).
• The mark arm (computational marker basis): the post-state of marker outcome j is the which-path product state, localProjB j bellE = |j⟩⊗|j⟩ (localProjB_bellE), and the system's screen statistics are flat at every phase (marked_no_fringe — rate 1/2, φ-independent): which-path information kills the fringe, dynamically.
• The erase arm (± marker basis, an instance of localProjOn): the ± family is a genuine OrthonormalBasis (pmBasis), the post-state factorises through the system profile eraseProfile (localProjOn_pm_bellE), and ★ the dynamical post-state's screen amplitudes are exactly √2 · eraserOut (erased_amp) — so every conditional statistic QuantumEraserVolume certifies for eraserOut is a statement about the state this measurement dynamics produces: the conditional rates (erased_rate), and the exact dark-fringe zero from the dynamics (erased_dark). The marker weights are 1/2 (erased_weight), the dynamical form of eraser_marker_marginal.

Together with reduceA_localLudersOn_mixture (Alice's marginal is invariant under either arm — erasing is Bob-side conditioning, never Alice-side signalling), this is the dynamical eraser: mark kills the fringe, erase restores it in the conditioned records, and nothing propagates to the unconditioned marginal.

⚠️ Honest scope. The two arms are single measurement strokes on the composite; the sequential mark-then-erase composition as one protocol run (two successive strokes on one arena, csd_sequential_born-style) is bookkeeping over these states and remains recorded on the BACKLOG row with the measure-level ensemble integral. The dynamical supplier of the post-states is, as throughout the route, BlockLudersObligation inhabited by joinWitness_blockLuders (through the brick-2 index bridge for the computational arm, and its local-unitary rotation for the ± arm).

References

specs/BACKLOG.md (the row); specs/future-work.md; Empirical/CSD/QuantumEraserVolume.lean (the statistics this module grounds dynamically); Empirical/QM/QuantumEraser.lean (bellVec, sysBra, markBra); SigmaLayer/LocalLuders.lean + LocalLudersBasis.lean (the machinery).

The joint state

noncomputable def CSD.Empirical.CSDBridge.EraserDynamics.bellE : EuclideanSpace ℂ (Fin 2 × Fin 2)

The Bell path–marker state as a Euclidean vector.

Equations

• CSD.Empirical.CSDBridge.EraserDynamics.bellE = WithLp.toLp 2 CSD.Empirical.QM.QuantumEraser.bellVec

@[simp]

theorem CSD.Empirical.CSDBridge.EraserDynamics.bellE_apply (p : Fin 2 × Fin 2) : bellE.ofLp p = QM.QuantumEraser.bellVec p

theorem CSD.Empirical.CSDBridge.EraserDynamics.bellVec_eq (p : Fin 2 × Fin 2) : QM.QuantumEraser.bellVec p = if p.1 = p.2 then 1 else 0

theorem CSD.Empirical.CSDBridge.EraserDynamics.bellE_ne_zero : bellE ≠ 0

theorem CSD.Empirical.CSDBridge.EraserDynamics.sliceB_bellE (a : Fin 2) : RecordLayer.sliceB bellE a = EuclideanSpace.single a 1

The B-slices of the Bell state are the computational rays.

The mark arm: which-path, no fringe

theorem CSD.Empirical.CSDBridge.EraserDynamics.localProjB_bellE (j : Fin 2) : RecordLayer.localProjB j bellE = EuclideanSpace.single (j, j) 1

The computational marker measurement leaves the which-path product state: Pⱼ |Φ⟩ = |j⟩ ⊗ |j⟩.

noncomputable def CSD.Empirical.CSDBridge.EraserDynamics.sysE (φ a : ℝ) : EuclideanSpace ℂ (Fin 2)

The screen-basis state, as a Euclidean vector.

Equations

• CSD.Empirical.CSDBridge.EraserDynamics.sysE φ a = WithLp.toLp 2 (CSD.Empirical.QM.QuantumEraser.sysBra φ a)

@[simp]

theorem CSD.Empirical.CSDBridge.EraserDynamics.sysE_apply (φ a : ℝ) (i : Fin 2) : (sysE φ a).ofLp i = QM.QuantumEraser.sysBra φ a i

theorem CSD.Empirical.CSDBridge.EraserDynamics.sysE_one_eq (φ a : ℝ) : (sysE φ a).ofLp 1 = ↑(a * Real.cos φ) + ↑(a * Real.sin φ) * Complex.I

theorem CSD.Empirical.CSDBridge.EraserDynamics.normSq_sysE_one (φ : ℝ) {a : ℝ} (ha : a = 1 ∨ a = -1) : ‖(sysE φ a).ofLp 1‖ ^ 2 = 1

theorem CSD.Empirical.CSDBridge.EraserDynamics.normSq_sysE (φ : ℝ) {a : ℝ} (ha : a = 1 ∨ a = -1) : ‖sysE φ a‖ ^ 2 = 2

theorem CSD.Empirical.CSDBridge.EraserDynamics.marked_no_fringe (φ : ℝ) {a : ℝ} (ha : a = 1 ∨ a = -1) (j : Fin 2) : ‖inner ℂ (sysE φ a) (EuclideanSpace.single j 1)‖ ^ 2 / ‖sysE φ a‖ ^ 2 = 1 / 2

The which-path state shows no fringe: the screen rate is 1/2 at every phase and screen port — the flat statistics of a marked path, produced by the mark stroke itself.

The ± marker basis

def CSD.Empirical.CSDBridge.EraserDynamics.pmSign (m : Fin 2) : ℝ

The ± sign of a marker index: +1 for 0, −1 for 1.

Equations

• CSD.Empirical.CSDBridge.EraserDynamics.pmSign m = if m = 0 then 1 else -1

theorem CSD.Empirical.CSDBridge.EraserDynamics.pmSign_cases (m : Fin 2) : pmSign m = 1 ∨ pmSign m = -1

noncomputable def CSD.Empirical.CSDBridge.EraserDynamics.pmVec (m : Fin 2) : EuclideanSpace ℂ (Fin 2)

The normalised ± marker vectors (|0⟩ ± |1⟩)/√2.

Equations

• CSD.Empirical.CSDBridge.EraserDynamics.pmVec m = !₂[↑(√2)⁻¹, ↑(CSD.Empirical.CSDBridge.EraserDynamics.pmSign m) * ↑(√2)⁻¹]

@[simp]

theorem CSD.Empirical.CSDBridge.EraserDynamics.pmVec_zero (m : Fin 2) : (pmVec m).ofLp 0 = ↑(√2)⁻¹

@[simp]

theorem CSD.Empirical.CSDBridge.EraserDynamics.pmVec_one (m : Fin 2) : (pmVec m).ofLp 1 = ↑(pmSign m) * ↑(√2)⁻¹

theorem CSD.Empirical.CSDBridge.EraserDynamics.invSqrtTwo_mul_self : (√2)⁻¹ * (√2)⁻¹ = 1 / 2

theorem CSD.Empirical.CSDBridge.EraserDynamics.invSqrtTwo_eq : (√2)⁻¹ = √2 / 2

theorem CSD.Empirical.CSDBridge.EraserDynamics.invSqrtTwoC_mul_self : ↑(√2)⁻¹ * ↑(√2)⁻¹ = ↑(1 / 2)

theorem CSD.Empirical.CSDBridge.EraserDynamics.inner_pmVec (i j : Fin 2) : inner ℂ (pmVec i) (pmVec j) = ↑((1 + pmSign i * pmSign j) / 2)

theorem CSD.Empirical.CSDBridge.EraserDynamics.orthonormal_pmVec : Orthonormal ℂ pmVec

The ± family is orthonormal.

noncomputable def CSD.Empirical.CSDBridge.EraserDynamics.pmBasis : OrthonormalBasis (Fin 2) ℂ (EuclideanSpace ℂ (Fin 2))

The ± marker basis, as a genuine orthonormal basis — the erase arm is an instance of localProjOn, not a hand-built pair of projectors.

Equations

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

theorem CSD.Empirical.CSDBridge.EraserDynamics.pmBasis_coe : ⇑pmBasis = pmVec

The erase arm: the conditioned states, from the dynamics

noncomputable def CSD.Empirical.CSDBridge.EraserDynamics.eraseProfile (m : Fin 2) : EuclideanSpace ℂ (Fin 2)

The system profile of the ±-conditioned post-state: the coefficient family of localProjOn pmBasis m bellE (see localProjOn_pm_bellE).

Equations

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

theorem CSD.Empirical.CSDBridge.EraserDynamics.localProjOn_pm_bellE (m : Fin 2) (ak : Fin 2 × Fin 2) : (RecordLayer.localProjOn pmBasis m bellE).ofLp ak = (eraseProfile m).ofLp ak.1 * (pmVec m).ofLp ak.2

The erase-arm post-state factorises: system profile ⊗ marker vector.

theorem CSD.Empirical.CSDBridge.EraserDynamics.eraseProfile_apply (m a : Fin 2) : (eraseProfile m).ofLp a = (starRingEnd ℂ) ((pmVec m).ofLp a)

theorem CSD.Empirical.CSDBridge.EraserDynamics.normSq_eraseProfile (m : Fin 2) : ‖eraseProfile m‖ ^ 2 = 1

theorem CSD.Empirical.CSDBridge.EraserDynamics.erased_amp (φ : ℝ) (i m : Fin 2) : inner ℂ (sysE φ (pmSign i)) (eraseProfile m) = ↑√2 * (QuantumEraserVolume.eraserOut φ (pmSign m)).ofLp i

★ The dynamical post-state's screen amplitudes are exactly √2 · eraserOut: the states the erase stroke produces are the states whose statistics QuantumEraserVolume certifies — conditional fringes, dark zero, and all.

theorem CSD.Empirical.CSDBridge.EraserDynamics.erased_dark : inner ℂ (sysE Real.pi (pmSign 0)) (eraseProfile 0) = 0

★ The dark fringe from the dynamics: at φ = π, the +-conditioned post-state has exactly zero amplitude at the bright port — the eraser's exact ontic zero, produced by the erase stroke.

theorem CSD.Empirical.CSDBridge.EraserDynamics.erased_rate (φ : ℝ) (i m : Fin 2) : ‖inner ℂ (sysE φ (pmSign i)) (eraseProfile m)‖ ^ 2 / (‖sysE φ (pmSign i)‖ ^ 2 * ‖eraseProfile m‖ ^ 2) = ‖(QuantumEraserVolume.eraserOut φ (pmSign m)).ofLp i‖ ^ 2

The conditional screen rates of the dynamical post-state are the eraserOut rates — the fringes QuantumEraserVolume certifies, now as statistics of the measurement dynamics' own output.

theorem CSD.Empirical.CSDBridge.EraserDynamics.erased_weight (m : Fin 2) : ‖RecordLayer.localProjOn pmBasis m bellE‖ ^ 2 / ‖bellE‖ ^ 2 = 1 / 2

The marker weights are 1/2 — the dynamical form of eraser_marker_marginal.