c5_c8_protocol_distinct
plain-language theorem explainer
The declaration establishes that the empirical protocol assigned to the C5 attention tensor combination differs from the protocol for the C8 Miller span combination. Researchers verifying Option A falsification coverage cite it to confirm that distinct theorem combinations receive distinct dataset-observable-failure triples. The proof is a one-line wrapper applying the general distinctness result after deciding the combinations are unequal.
Claim. Let $π$ map each combination identifier to its empirical protocol (dataset class, predicted observable, failure mode). Then $π$(C5 attention tensor) $≠$ $π$(C8 Miller span).
background
The module converts the falsifier registry into a Lean proposition asserting that every implemented C1-C9 combination possesses a dataset class, predicted observable, and failure mode. The function protocolSpec sends a CombinationID to a ProtocolSpec record whose fields are exactly those three components. An upstream theorem states that distinct combinations have distinct complete empirical protocols, which follows from the injectivity of the assignment map.
proof idea
The proof is a one-line wrapper that applies the general distinctness theorem protocolSpec_ne_of_ne after the decide tactic confirms the two specific combinations are unequal.
why it matters
This result feeds the empiricalProtocolCert bundle that certifies coverage for the C5 and C8 protocols among others. It completes the requirement that all implemented Option A combinations receive distinct falsifier protocols. The module documentation records zero sorry and zero axiom for the entire coverage claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.