c3_protocol
plain-language theorem explainer
The theorem establishes that the C3 oncology tensor combination satisfies ProtocolFalsifiable, confirming it possesses a registered dataset class, predicted observable, and failure mode. Researchers validating empirical coverage for Recognition Science Option A combinations would cite this result. The proof is a direct one-line application of the general protocolFalsifiable_all theorem to the C3 identifier.
Claim. The C3 oncology tensor combination is protocol-falsifiable: there exist a dataset class $d$, a predicted observable $o$, and a failure mode $f$ such that the registry satisfies datasetClass(C3) = $d$, predictedObservable(C3) = $o$, and failureMode(C3) = $f$.
background
This module converts the Option A falsifier registry into Lean propositions, guaranteeing that every implemented C1-C9 combination carries a dataset class, predicted observable, and failure mode. ProtocolFalsifiable(c) is the predicate asserting existence of matching registry entries for a given CombinationID. The upstream theorem protocolFalsifiable_all proves the predicate holds for arbitrary c by direct construction: unfolding yields the triple (datasetClass c, predictedObservable c, failureMode c) with reflexivity proofs.
proof idea
One-line wrapper that applies protocolFalsifiable_all to the C3 oncology tensor identifier.
why it matters
The result populates the empiricalProtocolCert record, which certifies coverage for the C1, C3, C5, and C8 cases. It closes the coverage requirement stated in the module: no implemented Option A theorem lacks an associated falsification protocol. This supports the framework's demand for total empirical testability of the implemented combinations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.