c3_protocol
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not specify concrete values for the dataset class, observable, or failure mode of C3.
- Does not establish empirical validity or success of the C3 protocol.
- Does not address combinations outside the implemented C1-C9 registry set.
Lean usage
theorem cert_c3 : ProtocolFalsifiable .c3OncologyTensor := c3_protocolformal statement (Lean)
112theorem c3_protocol :
113 ProtocolFalsifiable .c3OncologyTensor :=
proof body
One-line wrapper that applies protocolFalsifiable_all.
114 protocolFalsifiable_all .c3OncologyTensor
115