protocolSpec_matches
plain-language theorem explainer
protocolSpec_matches asserts that the protocol record generated for any CombinationID satisfies the three-field agreement condition in ProtocolMatches. Physicists auditing empirical falsification protocols cite this to confirm every implemented Option A combination carries a dataset class, predicted observable, and failure mode. The proof is a one-line simplification that unfolds the definitions of ProtocolMatches and protocolSpec.
Claim. For every combination identifier $c$, the protocol specification record for $c$ satisfies the matching predicate: its dataset class equals the dataset class of $c$, its predicted observable equals the predicted observable of $c$, and its failure mode equals the failure mode of $c$.
background
CombinationID is the inductive type enumerating implemented Option A combinations (C1 cognitive tensor through C5 attention tensor). ProtocolSpec is the record type with three fields: dataset class, predicted observable, and failure mode. ProtocolMatches is the predicate requiring exact agreement between these fields of a ProtocolSpec and the corresponding functions of a given CombinationID.
proof idea
The proof is a one-line term-mode simplification. It unfolds ProtocolMatches (the conjunction of three field equalities) and protocolSpec (the constructor that sets each field to the matching function of $c$), after which the equalities hold by reflexivity.
why it matters
This result supplies the existence witness for the uniqueness theorem uniqueProtocolSpec, which states that each CombinationID possesses a unique empirical protocol record. It realizes the module's coverage claim that no implemented Option A theorem lacks a falsifier protocol, supporting the empirical layer that accompanies the forcing chain and mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.