EmpiricallyCovered
plain-language theorem explainer
Every implemented Option A combination possesses a falsifier protocol consisting of a dataset class, predicted observable, and failure mode. Physicists auditing empirical testability of the Recognition Science monolith would cite this to confirm complete coverage across the C1-C9 cases. The definition encodes the coverage requirement as a universal statement over the finite set of implemented combinations.
Claim. The proposition that for every implemented Option A combination identifier $c$ there exist a dataset class $d$, predicted observable $o$, and failure mode $f$ such that the registry assigns $d$, $o$, and $f$ to $c$.
background
This module converts the falsifier registry into a Lean proposition asserting total empirical coverage for Option A. Every implemented C1-C9 combination has a dataset class, predicted observable, and failure mode. The data mappings remain empirical metadata; the formal content is total coverage with no implemented Option A theorem left without a falsifier protocol. A combination is protocol-falsifiable when it has a dataset class, a predicted observable, and a failure mode in the registry. The implemented combinations are enumerated by an inductive type whose constructors include cognitive tensor, planet strata, oncology tensor, quantum molecular depth, and attention tensor.
proof idea
This is a direct definition that universally quantifies the protocol-falsifiable predicate over all constructors of the combination inductive type. It functions as a one-line wrapper packaging the coverage claim for downstream use.
why it matters
This definition supplies the coverage proposition required by the theorem that empirically covered holds via the all-protocol-falsifiable result. It is also required by the EmpiricalProtocolCert structure that bundles the all-covered field with specific instances for cognitive tensor, oncology tensor, attention tensor, and Miller span. It closes the formal loop on the empirical protocol for Option A, ensuring falsifiability for each implemented combination.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.