ProtocolMatches
plain-language theorem explainer
ProtocolMatches(c, p) asserts that protocol record p agrees with combination c on its dataset class, predicted observable, and failure mode. Researchers certifying empirical coverage for Option A combinations cite this predicate to link registry assignments to concrete falsification protocols. The definition is realized as the direct conjunction of three field equalities drawn from the registry functions.
Claim. ProtocolMatches(c, p) holds if and only if the dataset class of p equals datasetClass(c), the observable of p equals predictedObservable(c), and the failure mode of p equals failureMode(c).
background
ProtocolSpec is the structure with three fields: dataset of type DatasetClass, observable of type PredictedObservable, and failure of type FailureMode. CombinationID is the inductive type enumerating implemented Option A combinations (c1CognitiveTensor through c5AttentionTensor). The functions datasetClass, predictedObservable, and failureMode map each combination to its assigned empirical metadata, as recorded in the falsifier registry.
proof idea
The definition is a direct conjunction of the three field projections of p against the registry functions applied to c. It functions as a one-line abbreviation with no tactics or lemmas required.
why it matters
ProtocolMatches supplies the core matching condition used by uniqueProtocolSpec and protocolSpec_matches to prove each combination possesses a unique protocol record. It also appears in the EmpiricalProtocolCert structure that certifies coverage for c1, c3, c5, and c8. Within the Recognition framework this predicate completes the empirical layer that turns the falsifier registry into propositions, guaranteeing total coverage for Option A without leaving any implemented combination without a falsification protocol.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.