EmpiricalProtocolCert
plain-language theorem explainer
EmpiricalProtocolCert packages the assertions that every implemented Option A combination possesses a falsifier protocol, together with uniqueness and distinctness conditions on the protocol map. A researcher auditing the empirical grounding of Recognition Science derivations would cite this certificate to confirm complete coverage of the C1-C9 combinations. The structure is defined directly by listing the required properties drawn from the falsifier registry.
Claim. An empirical protocol certificate is a record asserting: every combination $c$ admits a protocol-falsifiable triple (dataset class, predicted observable, failure mode); the map sending each combination to its protocol record is unique and injective; and the protocol records for the cognitive-tensor, oncology-tensor, attention-tensor, and Miller-span combinations are pairwise distinct.
background
The module converts the falsifier registry into a formal proposition guaranteeing that every implemented combination carries an associated dataset class, predicted observable, and failure mode. EmpiricallyCovered states that ProtocolFalsifiable holds for all combinations, where ProtocolFalsifiable(c) requires the existence of matching registry entries for datasetClass, predictedObservable, and failureMode. ProtocolSpec is the record type holding one such triple, and ProtocolMatches checks that a given record agrees exactly with the registry functions for its combination.
proof idea
The declaration is a structure definition whose fields are supplied directly by the sibling coverage predicates and the protocol-specification map; no tactics or reductions are required.
why it matters
This structure supplies the type of the empiricalProtocolCert construction that instantiates the full certificate from the registry. It formalizes the module claim of total coverage, ensuring no implemented Option A theorem lacks a falsification protocol. The certificate thereby anchors the empirical side of the Recognition Science forcing chain by making the transition from derivation to testable prediction fully explicit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.