protocolSpec
plain-language theorem explainer
Each implemented Option A combination receives a protocol specification assembled from its registry-assigned dataset class, predicted observable, and failure mode. Researchers auditing empirical coverage of the Recognition framework cite this construction when verifying that every C1-C9 theorem has a corresponding falsifier protocol. The definition performs a simple record construction using the three lookup functions defined in the falsifier registry.
Claim. For a combination identifier $c$, the protocol specification is the record with dataset component $datasetClass(c)$, observable component $predictedObservable(c)$, and failure component $failureMode(c)$.
background
ProtocolSpec is the structure that records the three components of an empirical falsifier protocol for one combination: a dataset class, a predicted observable, and a failure mode. CombinationID is the inductive type enumerating the implemented Option A combinations (c1CognitiveTensor through c5AttentionTensor). The module turns the falsifier registry into a Lean proposition by ensuring total coverage: every implemented combination has a dataset class, predicted observable, and failure mode. Upstream, the registry functions datasetClass, predictedObservable, and failureMode supply the concrete assignments for each combination.
proof idea
This definition is a one-line wrapper that constructs the ProtocolSpec record by applying datasetClass, predictedObservable, and failureMode to the input combination identifier.
why it matters
This definition supplies the protocol component used by pipelineSpec and programSpec to build complete empirical pipelines and programs for each combination. It directly supports the distinctness theorems c1_c3_protocol_distinct, c3_c5_protocol_distinct, and c5_c8_protocol_distinct as well as the EmpiricalProtocolCert structure that certifies coverage. In the Recognition Science framework it operationalizes the requirement that every prediction has an associated empirical test protocol, closing the loop from theoretical derivation to falsifiable observation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.