hygienicBool
plain-language theorem explainer
hygienicBool supplies a boolean predicate that verifies basic hygiene on a measurement protocol before observable extraction in the RS-native framework. Framework integrators and auditors cite it to gate protocol objects during validation passes. The definition implements the check via direct name inspection followed by a status match that adds extra nonempty-list requirements only for hypothesis and scaffold cases.
Claim. Let $p$ be a protocol with fields name (string), status, assumptions (list of strings), and falsifiers (list of strings). Then hygienicBool($p$) evaluates to true if and only if name is nonempty and, when status is hypothesis or scaffold, both assumptions and falsifiers are nonempty.
background
The RS-Native Measurement Framework (Core) supplies a Lean-first scaffold for extracting observables from ticks and voxels with base units fixed at τ₀ = ℓ₀ = 1. Protocols are the central explicit carrier: each carries a stable machine name, optional summary, a status tag, and separate lists of assumptions plus falsifiers so that windowing or coarse-graining choices remain visible. The module imports RSNativeUnits for the underlying constants (c = 1, coh = φ^{-5}, act = ħ = φ^{-5}) and the IntegrationGap and Masses.Anchor definitions of active-edge count A = 1.
proof idea
The definition is a direct one-line boolean expression. It first tests that p.name is nonempty, then performs a match on p.status; the hypothesis and scaffold arms each conjoin two nonempty-list checks while every other status arm returns true unconditionally.
why it matters
hygienicBool closes the hygiene contract required by the explicit-protocol design of the measurement scaffold. It operationalizes the rule that hypothesis and scaffold protocols must declare testable assumptions and falsifiers, supporting the framework's emphasis on falsifiability inside RS-native units. With zero listed downstream uses it functions as an audit utility rather than an internal lemma; it therefore touches the open integration question of how such checks compose with the concrete observables defined in the Catalog.* submodules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.