empiricallyCovered
The theorem asserts that every Option A combination identifier is assigned a complete falsifier protocol consisting of dataset class, predicted observable, and failure mode. Researchers validating Recognition Science predictions against data would cite it to confirm that no implemented C1-C9 theorem lacks an empirical test protocol. The proof is a direct one-line wrapper that applies the universal construction lemma protocolFalsifiable_all.
claimEvery combination identifier $c$ admits a falsifiable protocol: for all $c$, there exist a dataset class, predicted observable, and failure mode such that the protocol record matches $c$.
background
The Option A Empirical Protocol module converts the falsifier registry into a Lean proposition guaranteeing total coverage: no implemented theorem combination is left without a dataset class, predicted observable, and failure mode. EmpiricallyCovered is the proposition that for every CombinationID $c$, ProtocolFalsifiable $c$ holds, where ProtocolFalsifiable packages the three matching fields. This rests on the upstream theorem protocolFalsifiable_all, which states that for any $c$ the protocol record is constructed by direct application of datasetClass $c$, predictedObservable $c$, and failureMode $c$.
proof idea
The proof is a one-line wrapper that applies the lemma protocolFalsifiable_all to discharge the universal quantifier over CombinationID.
why it matters in Recognition Science
This supplies the all_covered field inside empiricalProtocolCert, closing the module requirement that every implemented Option A theorem carries a falsifier protocol. It supports the empirical testability of the Recognition Science forcing chain and phi-ladder mass formulas by ensuring no coverage gaps remain in the C1-C9 set. The result touches the framework's demand for concrete failure modes without addressing the numerical content of the datasets themselves.
scope and limits
- Does not specify numerical values or experimental details inside any dataset class.
- Does not verify that predicted observables match real measurements.
- Does not cover combinations outside the implemented C1-C9 registry.
- Does not supply the actual data mappings, which remain external empirical metadata.
formal statement (Lean)
105theorem empiricallyCovered : EmpiricallyCovered :=
proof body
One-line wrapper that applies protocolFalsifiable_all.
106 protocolFalsifiable_all
107