MeasurementEvent
plain-language theorem explainer
A measurement event packages one variational ledger step that couples an observer subsystem to the complementary system: pre-state, post-state, the partition, and a proof that the step is a variational successor. Anyone formalizing RS measurement, Born-rule structure, or apparent randomness cites this carrier type. It is a plain structure definition with no proof obligations beyond the successor witness.
Claim. For $N\in\mathbb{N}$, a measurement event consists of a subsystem partition of the $N$ ledger entries, a pre-measurement configuration $c_{\mathrm{pre}}$, a post-measurement configuration $c_{\mathrm{post}}$, and a witness that $c_{\mathrm{post}}$ is a variational successor of $c_{\mathrm{pre}}$.
background
Module F-009 (Measurement Mechanism) supplies the missing mechanism behind the slogan that quantum randomness is projection through finite resolution. Observers are not external: they are subsets of ledger entries. A configuration of $N$ entries is a map $\mathrm{Fin},N\to\mathbb{R}_{>0}$; total defect is the sum of individual $J$-costs.
A subsystem partition splits the $N$ indices into observer indices of cardinality $K$ ($0<K<N$) and the complementary system indices. The observer sees only its own entries; many full configurations share that partial view. Measurement is the recognition step that correlates those blocks.
Upstream, variational dynamics supplies the successor relation: the post-state is the global cost-minimizing update of the pre-state. That update is non-local (conservation couples all entries), which is why the full state can fix an outcome while the observer's partial view cannot.
proof idea
No proof body: this is a structure definition. The only mathematical content is the field is_variational, which requires a term of type IsVariationalSuccessor pre post from VariationalDynamics. Constructing an instance means exhibiting the partition, the two configurations, and that successor witness; nothing else is checked at definition time.
why it matters
This is the Part-3 carrier type for the measurement story in F-009. Downstream siblings (outcome map, outcome determination, same-state-same-outcome, correlation creation, Born-rule weighting) all need a typed object that is simultaneously a recognition event and an observer/system split.
In the broader RS chain it sits after Determinism and VariationalDynamics: determinism of the full ledger trajectory is already forced; this packages the step at which an internal observer becomes correlated with the system. Apparent randomness is then ignorance of complementary entries under a global, non-local variational update, not Bell-local hidden variables. The module roadmap ties this to $J$-cost weighting for $|\psi|^2$ statistics and to the eight-tick / recognition-event picture of discrete updates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.