Documentation

CsdLean4.Empirical.CSD.EraserSequential

Empirical/CSD/EraserSequential: mark, then erase — no revival (the row's residue) #

Category: empirical CSD twin, dynamical tier — the two-stroke sequential composition, closing the dynamical no-signalling + eraser row's recorded residue.

EraserDynamics proved the two single strokes: erasing the coherent Bell state restores the fringes (erased_rate), and marking kills them (marked_no_fringe). This module composes the strokes in the physically decisive order: mark first — a record exists — then erase. The mark post-state is the which-path product |j⟩⊗|j⟩ (localProjB_bellE); the ± erase stroke on that state gives marker outcomes with the same 1/2 weights (sequential_erase_weight), but the system profile stays on the ray [|j⟩] (seqProfile_eq — the erase stroke only rescales it), so the screen statistics remain flat at every phase:

★ sequential_no_revival — once a record exists, no later ±-basis marker measurement (Corrected 2026-08-04 (codebase audit). — the second stroke's basis is fixed by seqProfile; only the outcome is quantified. A general-basis version via localProjOn is mechanical and not done here) revives the fringe, whatever its outcome. Interference is recoverable only before the record (erased_rate), never after. This is the statistical face of what the corpus proves structurally elsewhere: records are relocation with storage, not erasable bookkeeping — "un-measuring" is not an operation the dynamics has.

⚠️ Honest scope. The strokes compose as state updates (the second stroke acts on the first stroke's post-state); the two-time protocol plumbing carries over verbatim from the single-stroke machinery and is not restated. The row's other recorded residue — the measure-level "ensemble integral" form of no-signalling — is hereby closed as definitional (2026-08-03): for finitely many outcomes the post ray-ensemble is the discrete mixture Σⱼ pⱼ·δ_{[Pⱼv]}, and its barycenter statement is reduceA_localLudersOn_mixture; recasting it as a Bochner integral would add a reduceA-measurability lemma and no content. Revisit only if a continuum-outcome layer ever appears.

References #

specs/BACKLOG.md (the row); Empirical/CSD/EraserDynamics.lean (the two single strokes); SigmaLayer/LocalLuders.lean + LocalLudersBasis.lean (the machinery); SigmaLayer/RecordPersistence.lean (the structural face of irreversibility).

source
noncomputable def CSD.Empirical.CSDBridge.EraserSequential.markPost (j : Fin 2) :
EuclideanSpace ℂ (Fin 2 × Fin 2)

The mark-stroke post-state for marker outcome j: the which-path product state.

Equations
Instances For
    source
    theorem CSD.Empirical.CSDBridge.EraserSequential.sliceB_markPost (j a : Fin 2) :
    RecordLayer.sliceB (markPost j) a = if a = j then EuclideanSpace.single j 1 else 0

    The B-slices of the mark post-state: the marker ray over the recorded path, zero elsewhere.

    source
    noncomputable def CSD.Empirical.CSDBridge.EraserSequential.seqProfile (j m : Fin 2) :
    EuclideanSpace ℂ (Fin 2)

    The system profile of the second (erase) stroke, acting on the mark post-state.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem CSD.Empirical.CSDBridge.EraserSequential.seqProfile_eq (j m : Fin 2) :
      seqProfile j m = (starRingEnd ℂ) ((EraserDynamics.pmVec m).ofLp j) • EuclideanSpace.single j 1

      The erase stroke cannot move the recorded path: the second-stroke system profile is a scalar multiple of the recorded ray |j⟩ — erasing after the record only rescales.

      source
      theorem CSD.Empirical.CSDBridge.EraserSequential.normSq_pmVec_component (m j : Fin 2) :
      ‖(EraserDynamics.pmVec m).ofLp j‖ ^ 2 = 1 / 2
      source
      theorem CSD.Empirical.CSDBridge.EraserSequential.sequential_erase_weight (j m : Fin 2) :
      ‖seqProfile j m‖ ^ 2 / ‖markPost j‖ ^ 2 = 1 / 2

      The second-stroke marker weights are still 1/2 — the erase stroke's outcomes stay unbiased on the marked state.

      source
      theorem CSD.Empirical.CSDBridge.EraserSequential.sequential_no_revival (φ : ℝ) {a : ℝ} (ha : a = 1 ∨ a = -1) (j m : Fin 2) :
      ‖inner ℂ (EraserDynamics.sysE φ a) (seqProfile j m)‖ ^ 2 / (‖EraserDynamics.sysE φ a‖ ^ 2 * ‖seqProfile j m‖ ^ 2) = 1 / 2

      ★ No revival: once the mark record exists, erasing cannot restore the fringe. The screen rate after mark-j-then-erase-m is 1/2 at every phase, port, and marker outcome — conditioning on the second stroke changes nothing, in exact contrast to the pre-record erase stroke (erased_rate), whose conditioned fringes have full visibility. Records are statistically irreversible.