c1_c3_protocol_distinct
plain-language theorem explainer
The theorem establishes that the empirical protocols assigned to the C1 cognitive tensor and C3 oncology tensor combinations are unequal. Researchers verifying separation of falsification protocols within the Option A registry of Recognition Science would cite this result. The proof is a one-line wrapper that applies the general distinctness theorem for protocol specifications to these two cases and discharges the inequality by decision.
Claim. The protocol specification associated with the C1 cognitive tensor combination is not equal to the protocol specification associated with the C3 oncology tensor combination.
background
The Option A Empirical Protocol module maps each CombinationID to a ProtocolSpec that bundles a dataset class, a predicted observable, and a failure mode. The function protocolSpec performs this assignment for every implemented combination, turning the falsifier registry into a total Lean proposition with no remaining axioms or sorrys. The local setting is therefore one of complete formal coverage: every C1-C9 combination carries an explicit empirical protocol.
proof idea
The proof is a one-line wrapper that applies the upstream theorem protocolSpec_ne_of_ne to the concrete pair .c1CognitiveTensor and .c3OncologyTensor, with the required inequality discharged by a decision procedure.
why it matters
This result feeds directly into the empiricalProtocolCert definition, which records coverage for the C1, C3, C5 and C8 protocols. It thereby supports the Recognition Science requirement that distinct CombinationIDs receive distinct falsification protocols, closing one concrete instance of the total-coverage claim in the Option A registry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.