mapWithProtocol
plain-language theorem explainer
This definition transforms the value of an RS-native measurement by applying a function f while substituting a new protocol record p. It supports derivation of observables in the Recognition Science measurement scaffold where extraction methods must remain explicit. The body performs a direct record update that copies window, uncertainty, and notes from the input unchanged.
Claim. Let $f : α → β$, let $p$ be a protocol, and let $m$ be a measurement of type $α$. Then mapWithProtocol$(f, p, m)$ yields the measurement whose value equals $f(m.value)$, whose window and uncertainty equal those of $m$, whose protocol equals $p$, and whose notes equal those of $m$.
background
The RS-Native Measurement Framework defines a Measurement as a record containing a value of type α, an optional time window, a required protocol, an optional uncertainty record, and a list of notes. A Protocol is a structure that records the extraction method via a stable name, optional summary, hygiene status, list of assumptions, and list of falsifiers. The module design requires every observable to carry its protocol explicitly so that windowing, coarse-graining, and basis choices remain visible rather than hidden.
proof idea
The definition is a direct record constructor. It applies f to the input value, inserts the supplied protocol p, and copies the window, uncertainty, and notes fields verbatim from the source measurement.
why it matters
The definition enforces the explicit-protocol rule that underpins the entire RS measurement scaffold. It allows new observables to be derived while preserving traceability of the extraction step, consistent with the module goal that arbitrary choices cannot be hidden. No downstream uses appear yet, but the construction is a prerequisite for catalog entries that build derived quantities from base ledger observables.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.