c3_c5_protocol_distinct
plain-language theorem explainer
The theorem establishes that the empirical protocols for the C3 oncology tensor and C5 attention tensor combinations are distinct. Researchers maintaining the Option A falsifier registry cite it to confirm separation between these two protocol implementations. The proof is a one-line wrapper that applies the general injectivity result for protocol specifications after deciding the underlying combinations differ.
Claim. Let $π$ map each combination identifier to its empirical protocol (dataset class, predicted observable, failure mode). Then $π$(C3 oncology tensor) $≠$ $π$(C5 attention tensor).
background
The Option A Empirical Protocol module converts the falsifier registry into Lean propositions, assigning every implemented C1-C9 combination a dataset class, predicted observable, and failure mode. The function protocolSpec produces the ProtocolSpec record for a given CombinationID. An upstream theorem states that distinct combinations produce distinct protocols, with the proof relying on injectivity of the mapping.
proof idea
The proof is a one-line wrapper that applies protocolSpec_ne_of_ne to the pair of combinations, using a decision procedure to establish that the identifiers are unequal.
why it matters
This result supports the empiricalProtocolCert definition, which certifies coverage for C1, C3, C5, and C8 protocols. It ensures no implemented Option A theorem lacks a falsifier protocol, as required by the module's total-coverage goal. The declaration strengthens the empirical validation layer tied to the forcing chain and phi-ladder structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.