c3_uniqueProtocol
plain-language theorem explainer
Existence and uniqueness of the empirical protocol record is asserted for the C3 oncology tensor combination. Researchers confirming falsifiability coverage for Option A would reference this result. The argument reduces directly to the general uniqueness theorem for all combinations.
Claim. There exists a unique protocol record $p$ such that the dataset class of $p$ equals the dataset class prescribed for the C3 oncology tensor, the predicted observable of $p$ equals the predicted observable for the C3 oncology tensor, and the failure mode of $p$ equals the failure mode for the C3 oncology tensor.
background
The Option A Empirical Protocol module converts the falsifier registry into propositions asserting that every implemented C1-C9 combination possesses a dataset class, predicted observable, and failure mode. A protocol record is a structure assembling these three components. ProtocolMatches is the predicate that a record agrees exactly with the values assigned to a given combination identifier.
proof idea
This is a one-line wrapper applying the general uniqueness result to the C3 oncology tensor case.
why it matters
The declaration feeds the empirical protocol certificate by confirming coverage for the C3 case. It supports the claim of total coverage for implemented Option A theorems, ensuring no combination lacks a falsifier protocol. This aligns with the framework requirement that every implemented theorem carries an associated empirical test.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.