Protocol
plain-language theorem explainer
The Protocol structure records the extraction method for an RS observable from a state or trace, including a machine-friendly name, summary, status, assumptions and falsifiers. Calibration and alignment code in the measurement layer cites this record to keep every choice explicit. It is introduced directly as a structure definition with default values for summary, status and the two lists.
Claim. A measurement protocol is a record with a short stable identifier $name$, an optional human-readable summary, a status value, a list of explicit assumptions, and a list of falsifiers.
background
The module sets up a Lean-first scaffold for Recognition Science measurement. Every protocol must carry falsifiers so that windowing, coarse-graining and basis choices stay visible rather than hidden. Upstream results include the cellular-automaton step operation that advances a tape by a local rule and the RS-native units status that fixes base units with $c=1$, $coh=phi^{-5}$ and $act=hbar=phi^{-5}$.
proof idea
The declaration is the structure definition itself that introduces the four fields together with their default values.
why it matters
This record is extended by AlignmentProtocol and supplies the protocol field inside CalibrationCert for single-anchor SI reporting. It directly implements the module design goal that every measurement protocol must list falsifiers. It anchors the RS-native measurement layer before any external calibration step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.