Empirical/CSD/SequentialMeasurement: repeatability and sequential Born, from the dynamics #
Category: 3-Local (CSD-ontic empirical; the first entry consuming the v0.7.0–v1.0.0 dynamical measurement layer).
What this tests #
Every other entry in the empirical suite exercises the kinematic Born machinery — volumes,
partitions, bridge transports. This one exercises the measurement dynamics: the calibrated-swap
witness, in which a record is created by an explicit measure-preserving propagator and the
post-measurement state is a pushforward theorem (swap_luders_born). Two textbook empirical facts
fall out, now as consequences of the dynamics rather than as separate posits:
- Repeatability (
csd_repeatability): measure in the computational basis, obtain outcomei, measure again in the same basis — the same outcome recurs with probability1, any other with probability0. Von Neumann's "a repeated measurement gives the same result", derived from the swap dynamics plusmomentMap_vertex(the moment map at a vertex is its indicator). - Sequential Born (
csd_sequential_born): after outcomei, the follow-up statistics for any context fieldc'are the collapsed state's Born weightsc'.rate [eᵢ]— not the preparation's. This is the empirically loaded content of the Lüders update: the second measurement sees[eᵢ], and the originalψis gone from the statistics.
The chain, and its exact status #
The chain is: a record fixes the state (the collapse — the post-measurement marginal is the
slot-i calibration), Born gives the next volume fractions at that state, and repeat. Each
repetition consumes a fresh bank.
⚠️ Status, and it changed on 2026-09-05 — do not repeat the older wording. Iteration beyond two
steps used to be an argument from self-similarity. It is now a theorem: csd_nstep_born
(RecordLayer/NStepChain.lean) proves the depth-n law for every sequence of contexts and
outcomes, by induction, with csd_nstep_repeatable for non-vacuity. What is still an argument is
one level up: that an n-stage arena assembles to give it. two_stage_joint builds that arena
for n = 2; the general construction is not done. So the honest split is — the chain law is
proved to arbitrary depth given n banks; the chain arena is built for two.
⚠️ Honest scope #
- The calibration is a named posit —
specs/POSITS.mdPosit 5,calibratedBank(RecordLayer/SwapClosure.lean) — and costs one bank per measurement. - Rank-one, computational-basis first measurement — the scope of the swap witness
(
SwapLuders.lean); degenerate first measurements are the recorded open construction (DegenerateLuders.lean). hpos(the first outcome has nonzero probability) is carried as a hypothesis: conditioning on a null outcome is undefined, as it should be. (Upgrade 2026-08-02:) for the canonical ready preparationreadyPrep p = epistemicMeasure p ⊗ readyMeasure N,prep_outcome_posproveshposoutright whenever the Born weightmomentMap p iis nonzero — the preparation itself licenses the conditioning. (Moved 2026-08-02, same day:)readyPrepandprep_outcome_posnow live inRecordLayer/SwapClosure.lean— they areSigmaLayermachinery, born one layer too high here; re-exported through this module's imports, so consumers are unchanged.- These are theorems about the witness dynamics, inheriting the witness's own scope notes (calibration is a context-fixed posit; Hamiltonian origin of the propagator is §2a-scoped).
- (Upgrade 2026-08-21, Q25:) these are CONDITIONAL statements — probabilities of the second
outcome given the first, read off the post-measurement ensemble. The composed two-time joint
law on one arena (both records on a single composite space, the first persisting) is
RecordLayer/TwoTimeLuders.lean(two_time_born,two_time_repeat,two_time_other_fate).
References #
RecordLayer/SwapLuders.lean (swap_luders_born — the engine);
RecordLayer/DegenerateLuders.lean (momentMap_vertex);
RecordLayer/RecordPersistence.lean (readout_persists_on_interval — the pointer-level
repeatability this complements at the state level); EMPIRICAL.md.
The post-measurement ensemble of the calibrated-swap witness, given outcome i from a
computational-basis measurement on system-and-register state μ12 with vertex-calibrated bank.
Equations
- One or more equations did not get rendered due to their size.
Instances For
★ Sequential Born: the second measurement sees the collapsed state. After outcome i, the
follow-up outcome-j probability for any context field c' is the Born weight of [eᵢ] — the
preparation ψ has left the statistics entirely. The Lüders update as an empirical prediction,
derived from the swap dynamics.
★★ Repeatability: a repeated measurement gives the same result. Measure in the
computational basis, record outcome i, measure again in the same basis: outcome i recurs with
probability 1 and any other outcome has probability 0. Derived — the follow-up context's rate
at the collapsed vertex is the vertex's indicator (momentMap_vertex).
The two halves of repeatability, spelled out: certainty on the recorded outcome…
…and impossibility of every other outcome.