addNote
plain-language theorem explainer
addNote augments an RS-native measurement by appending a string note to its notes list while copying all other fields unchanged. Researchers documenting protocol steps or calibration details in the RS scaffold would invoke it to maintain explicit audit trails. The definition reduces to a direct record update that concatenates the note onto the existing list.
Claim. For a measurement $m$ of type Measurement $α$ carrying value, optional window, protocol, optional uncertainty, and notes list, addNote(note, $m$) returns the measurement identical to $m$ except that its notes field becomes $m$.notes concatenated with the singleton list containing note.
background
The RS-Native Measurement Framework supplies a Lean-first scaffold for Recognition Science observables built from ticks, voxels, and ledger entries with $τ₀ = 1$. Its central structure Measurement $α$ packages a value of type $α$, an optional Window, a required Protocol, optional Uncertainty, and a list of String notes. The module documentation states that every measurement must carry protocol plus falsifiers so that arbitrary choices cannot be hidden. Upstream structures supply related but distinct records: a simple name-value-error triple in Data.Import and an axis-outcome-time triple in Quantum.NonlocalityNoSignaling.
proof idea
The definition is a one-line wrapper that performs a record update on the input measurement, replacing only the notes field by list concatenation of the existing notes with the singleton list containing the supplied note.
why it matters
addNote implements the explicit-notes requirement of the RS measurement scaffold, allowing protocol annotations without touching value or uncertainty. It directly supports the module design goal that protocols remain visible and that SI calibration stays outside core. With zero recorded downstream uses, its role in Catalog observables remains open for later integration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.