hygienic
plain-language theorem explainer
The hygienic predicate requires a Protocol to carry a nonempty name and, when status is hypothesis or scaffold, to list both assumptions and falsifiers. Calibration proofs in SingleAnchor invoke it to confirm protocol integrity before scalar-to-unit derivations. The definition encodes the hygiene rules directly via pattern match on the status field of the Protocol record.
Claim. A protocol $p$ is hygienic when its name is nonempty and, if its status equals hypothesis or scaffold, both its assumptions list and its falsifiers list are nonempty.
background
The RS-Native Measurement Framework isolates core observables built from ticks, voxels, and coherence quanta with $τ_0=1$, while external SI calibration remains outside this module. Protocols record how an observable is extracted from a state or trace and must carry explicit assumptions and falsifiers so that windowing or basis choices stay auditable. The Protocol structure supplies the fields name, summary, status, assumptions, and falsifiers that the predicate inspects.
proof idea
The definition is a direct structural check: it asserts name nonempty, then pattern-matches on status and requires nonempty lists precisely when the status is hypothesis or scaffold.
why it matters
Downstream theorems calibration_protocol_hygienic and tau0_seconds_protocol_hygienic apply this predicate to certify the protocol attached to a single-anchor $τ_0$ derivation. It directly implements the module design goal that every measurement protocol must expose its assumptions and falsifiers, keeping the RS measurement scaffold free of hidden choices.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.