mapWithProtocol
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not modify the time window attached to the measurement.
- Does not recompute or alter the uncertainty record.
- Does not inspect or enforce the assumptions listed inside the new protocol.
- Does not interact with ledger snapshots or time-emergence functions.
formal statement (Lean)
136def mapWithProtocol {α β : Type} (f : α → β) (p : Protocol) (m : Measurement α) : Measurement β :=
proof body
Definition body.
137 { value := f m.value
138 window := m.window
139 protocol := p
140 uncertainty := m.uncertainty
141 notes := m.notes
142 }
143
144/-- Transform the uncertainty record (when present). -/