c1_c3_protocol_distinct
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not establish distinctness for any pair of combinations other than C1 and C3.
- Does not supply the concrete dataset classes or observables attached to these protocols.
- Does not address empirical validation or experimental outcomes of the protocols.
formal statement (Lean)
88theorem c1_c3_protocol_distinct :
89 protocolSpec .c1CognitiveTensor ≠ protocolSpec .c3OncologyTensor := by
proof body
One-line wrapper that applies exact.
90 exact protocolSpec_ne_of_ne (by decide)
91