c3_protocol_covered
plain-language theorem explainer
The C3 oncology tensor combination satisfies the protocol-falsifiability condition by possessing a registered dataset class, predicted observable, and failure mode. Researchers auditing empirical coverage for the C1-C9 cross-domain theorems cite this result to confirm that queued test items carry formal protocol assignments. The proof is a direct one-line application of the general theorem that every combination meets the falsifiability criteria.
Claim. The combination $c_3$ for the oncology tensor is protocol-falsifiable: there exist a dataset class $d$, predicted observable $o$, and failure mode $f$ such that the registry maps satisfy datasetClass$(c_3)=d$, predictedObservable$(c_3)=o$, and failureMode$(c_3)=f$.
background
The Option A Empirical Queue module maintains a priority ordering over empirical tests attached to the C1-C9 cross-domain theorems. Its stated purpose is to record testing order while proving that every queued combination is already covered by the formal empirical protocol; the module contains zero sorries or axioms. ProtocolFalsifiable is the predicate asserting that a given CombinationID possesses matching entries in the three registry functions for dataset class, predicted observable, and failure mode. The upstream theorem protocolFalsifiable_all states that this predicate holds for every combination and is proved by unfolding the definition and supplying the registry values directly.
proof idea
One-line wrapper that applies protocolFalsifiable_all to the specific combination .c3OncologyTensor.
why it matters
The result confirms that the C3 oncology tensor item in the empirical queue carries a complete protocol record, thereby discharging part of the module-level claim that all queued items are formally covered. It supports the broader Recognition Science practice of attaching falsifiable empirical protocols to cross-domain theorems without supplying actual data or validation. No downstream theorems are listed, and the declaration touches no open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.