addNotes
plain-language theorem explainer
This definition appends a list of annotation strings to an existing measurement record while preserving its value, window, protocol, and uncertainty. Workers on protocol-aware observables in the RS-native framework would invoke it to attach context without mutating core fields. The implementation performs a direct record update that concatenates the supplied notes onto the measurement's existing list.
Claim. Let $m$ be a measurement of type $α$ carrying a value, optional window, protocol, optional uncertainty, and list of notes. For any list of strings $n$, the operation returns the measurement identical to $m$ except that its notes field equals the concatenation of $m$'s notes with $n$.
background
The RS-Native Measurement Framework supplies a Measurement structure that packages a value of arbitrary type $α$ together with an explicit protocol, optional time window, optional uncertainty interval, and a list of string notes. This design keeps every observable tied to its protocol and allows annotations while leaving SI calibration outside the core. The module imports the general Measurement structure from Data.Import and the PrimitiveDistinction axioms, plus related measurement records from the Quantum and Relativity sectors.
proof idea
The definition is realized by a one-line record update that replaces the notes field of the input measurement with the concatenation of its current notes and the supplied list.
why it matters
The definition belongs to the Measurement namespace inside the RS-native core and supports the framework's requirement that every measurement carry an explicit protocol plus optional notes. It directly implements the design goal stated in the module documentation that protocols remain visible so that windowing and coarse-graining choices cannot be hidden. No downstream theorems are recorded yet, but the operation underpins the catalog of concrete observables built on this scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.