ProtocolSpec
plain-language theorem explainer
The protocol specification record assembles a dataset class, predicted observable, and failure mode into one structure for falsifying an Option A combination. Empirical researchers validating Recognition Science claims would cite this record when defining test protocols. The definition is a direct structure introduction that bundles three inductive enumerations and derives equality and representation.
Claim. A protocol specification is a record $(D, O, F)$ where $D$ is a dataset class, $O$ is a predicted observable, and $F$ is a failure mode, with each component taken from the inductive types defined in the Option A falsifier registry.
background
In the Option A empirical protocol module, the falsifier registry is formalized to guarantee that every implemented combination from C1 to C9 possesses a corresponding dataset class, predicted observable, and failure mode. The mappings themselves are treated as empirical metadata, while the formal content enforces total coverage without leaving any theorem without a falsification protocol.
proof idea
The declaration introduces the structure by listing its three fields and automatically deriving decidable equality and representation from the underlying inductive types. No tactics or lemmas are applied; it is a pure record definition.
why it matters
This record type anchors the empirical layer of Option A by providing the common structure for protocol specifications. It is referenced in the definitions of pipeline and program specifications, and in theorems certifying unique protocols and empirical coverage for combinations such as c3 oncology tensor. It directly implements the module's goal of total falsifier coverage, aligning with the Recognition Science requirement that all claims be empirically testable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.