MeasurementProtocol
plain-language theorem explainer
A measurement protocol packages a subsystem split (observer vs system), a finite outcome space, and a pre/post pair of N-entry ledger configurations linked by one variational successor step. Anyone formalizing RS measurement, Born-structure, or apparent randomness cites this bundle. It is a pure data structure: the only propositional field is the coupling witness.
Claim. For $N \in \mathbb{N}$, a measurement protocol is a 5-tuple $(S,\mathcal{O},c_{\mathrm{pre}},c_{\mathrm{post}},\kappa)$ where $S$ partitions the $N$ ledger indices into observer and system, $\mathcal{O}$ is a finite outcome space ($|\mathcal{O}|\ge 1$), $c_{\mathrm{pre}},c_{\mathrm{post}}$ are positive-entry configurations of size $N$, and $\kappa$ asserts that $c_{\mathrm{post}}$ is a variational successor of $c_{\mathrm{pre}}$. The observed outcome is the coarse-grained projection of $c_{\mathrm{post}}$ through the observer indices of $S$.
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: a subsystem is a partition of the $N$ ledger indices into an observer block of size $K$ ($0<K<N$) and its complement (the system). A configuration is an $N$-tuple of positive real ratios; total defect is the sum of individual $J$-costs on those ratios.
An outcome space is just a positive integer of coarse bins. The outcome map sums defect on the observer indices, scales by the number of bins, floors, and reduces mod the bin count. That projection reads only observer entries, but those values are fixed by the global variational update of the full state.
The local setting is the three-stage story in the doc-comment: uncoupled pre-state, one variational interaction that couples observer and system under the shared conservation constraint, then a read that projects the post-state. Apparent randomness is ignorance of complementary entries, not Bell-local hidden variables; non-locality of the update is upstream in VariationalDynamics.
proof idea
No proof body: this is a structure definition. Five fields are declared. Four are data (subsystem, outcome space, pre-state, post-state). The fifth is the propositional coupling field IsVariationalSuccessor pre_state post_state, imported from the variational-dynamics layer, which records that the post-configuration is one recognition step from the pre-configuration. The companion projection observed_outcome is a one-line wrapper applying the existing outcome map to the protocol's subsystem, outcome space, and post-state.
why it matters
This is the central data type of F-009. It turns the informal claim in Determinism (randomness as lossy projection) into a concrete object: measurement equals one variational coupling plus an observer-side coarse read. Downstream theorems in the same module (outcome determined by full state, same state same outcome, measurement creates correlation) are stated relative to this bundle; the correlation theorem is the encoding claim that post-measurement observer entries carry system information via the conservation constraint.
In the broader RS chain it sits after time emergence, determinism, and variational dynamics, and before Born-rule weighting by $J$-cost. Verification consumers under LedgerHum reuse the measurement-protocol vocabulary for experimental checklists (pulsar stacking, lag windows around the eight-tick period); the foundation structure is the abstract ledger-side counterpart those checks presuppose. It does not itself force $\phi$, $D=3$, or the eight-tick octave; those enter through the dynamics and cost layers it sits on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.