hygienic
The hygienic predicate on a Protocol record requires a non-empty name and, for hypothesis or scaffold status, non-empty assumptions and falsifiers lists. Calibration authors in the RS-native measurement framework cite it to guarantee that extraction protocols remain auditable. The definition performs a direct case analysis on the status field of the Protocol structure.
claimA protocol $p$ satisfies the hygiene predicate if $p.name$ is nonempty and, when $p.status$ is hypothesis or scaffold, both the list of assumptions and the list of falsifiers are nonempty.
background
The RS-Native Measurement Framework (Core) module supplies a Lean-first scaffold for extracting observables from states or traces. Every measurement carries an explicit Protocol record whose fields are name (stable identifier), summary, status (spec, hypothesis, scaffold, etc.), assumptions (testable premises), and falsifiers (conditions that would refute the extraction). This design keeps arbitrary choices such as windowing or coarse-graining visible rather than hidden. Upstream results include the RS Native Units status confirming base units tick and voxel with $τ_0=1$, together with structures from PhiForcingDerived and SpectralEmergence that supply the J-cost and gauge content underlying the observables.
proof idea
The definition is a direct structural predicate. It first checks that the name field is nonempty, then matches on the status field: for hypothesis or scaffold it additionally requires both assumptions and falsifiers to be nonempty lists; all other status values return true.
why it matters in Recognition Science
This definition is invoked by the calibration theorems calibration_protocol_hygienic and tau0_seconds_protocol_hygienic in SingleAnchor, which certify hygiene for the $τ_0$ seconds protocol. It supplies the explicit-protocol requirement demanded by the RS measurement scaffold and aligns with the framework's emphasis on falsifiability for phi-ladder observables. No open scaffolding remains at this node.
scope and limits
- Does not prescribe the semantic content of any assumption or falsifier string.
- Does not enforce uniqueness of protocol names across a catalog.
- Does not apply hygiene checks to fields other than name, status, assumptions, and falsifiers.
- Does not derive numerical bounds or calibration constants from the predicate.
Lean usage
theorem tau0_seconds_protocol_hygienic : Protocol.hygienic tau0_seconds_protocol := by simp [Protocol.hygienic, tau0_seconds_protocol]formal statement (Lean)
52def hygienic (p : Protocol) : Prop :=
proof body
Definition body.
53 p.name ≠ "" ∧
54 match p.status with
55 | .hypothesis | .scaffold => p.assumptions ≠ [] ∧ p.falsifiers ≠ []
56 | _ => True
57
58/-- Boolean check version of `Protocol.hygienic` (useful for audits). -/