protocolFalsifiable_all
plain-language theorem explainer
Every CombinationID in the implemented Option A set satisfies ProtocolFalsifiable, so each combination possesses a dataset class, predicted observable, and failure mode drawn from the registry. Empirical protocol designers cite the result to confirm that no implemented combination lacks an associated falsification protocol. The proof is a direct term that witnesses the three existentials by applying the registry accessors and reflexivity.
Claim. For every combination identifier $c$ in the inductive type of implemented Option A combinations, there exist a dataset class $d$, a predicted observable $o$, and a failure mode $f$ such that the registry satisfies datasetClass$(c)=d$, predictedObservable$(c)=o$, and failureMode$(c)=f$.
background
ProtocolFalsifiable is the existential proposition that a CombinationID is equipped with a DatasetClass, PredictedObservable, and FailureMode via the three registry functions. The module converts the falsifier registry into a total coverage statement: every implemented combination (C1–C9) receives an explicit falsification protocol. Upstream, CombinationID is the inductive enumeration of those combinations, while the registry functions datasetClass, predictedObservable, and failureMode supply the concrete metadata for each identifier.
proof idea
The term proof first unfolds the definition of ProtocolFalsifiable, exposing the three existentials and the three equality conjuncts. It then supplies the witnesses directly as the applications datasetClass c, predictedObservable c, and failureMode c, closing the equalities with three instances of reflexivity.
why it matters
The theorem supplies the uniform witness that every Option A combination is empirically falsifiable. It is invoked by the concrete protocol theorems c1_protocol, c3_protocol, c5_protocol, and c8_protocol, and by empiricallyCovered to assert complete coverage. Within the Recognition Science framework it closes the formal link between the theoretical combinations and their empirical test protocols, ensuring no implemented theorem is left without a falsifier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.