uniqueProtocolSpec
plain-language theorem explainer
For any implemented combination identifier there exists exactly one protocol record whose dataset class, predicted observable, and failure mode agree with those of the combination. Empirical protocol work in the Recognition Science framework cites this to guarantee uniqueness across the C1-C9 set. The term proof exhibits the canonical construction and reduces any other match to fieldwise equality via simplification.
Claim. For every combination identifier $c$, there exists a unique protocol record $p$ such that the dataset class of $p$ equals the dataset class of $c$, the predicted observable of $p$ equals the predicted observable of $c$, and the failure mode of $p$ equals the failure mode of $c$.
background
ProtocolSpec is the structure that records a dataset class, a predicted observable, and a failure mode for one combination. ProtocolMatches is the predicate asserting that a protocol record agrees with a combination on all three components. The module converts the falsifier registry into propositions asserting total coverage: every implemented Option A combination has an associated empirical protocol record with no gaps.
proof idea
The proof is a term-mode construction that supplies protocolSpec c as the witness and invokes protocolSpec_matches c to confirm the match. Uniqueness follows by introducing an arbitrary matching p, destructuring it into its three fields, applying the match hypothesis, and simplifying to obtain equality of the fields.
why it matters
This result supplies the uniqueness half of the empirical protocol coverage for Option A. It is invoked directly by c3_uniqueProtocol to obtain the specific uniqueness statement for the oncology tensor combination and by empiricalProtocolCert to assemble the overall certificate. In the Recognition framework it closes the loop on falsifiability by ensuring each combination has a distinct protocol record.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.