c5_c8_protocol_distinct
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.
claimLet $π$ 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 in Recognition Science
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.
scope and limits
- Does not specify the concrete dataset classes or observables attached to these combinations.
- Does not address any combinations outside C5 and C8.
- Does not prove existence or correctness of the underlying data mappings.
- Does not connect to the forcing chain, phi-ladder, or mass formulas.
Lean usage
theorem c5_c8_distinct_example : protocolSpec .c5AttentionTensor ≠ protocolSpec .c8MillerSpan := c5_c8_protocol_distinctformal statement (Lean)
96theorem c5_c8_protocol_distinct :
97 protocolSpec .c5AttentionTensor ≠ protocolSpec .c8MillerSpan := by
proof body
Term-mode proof.
98 exact protocolSpec_ne_of_ne (by decide)
99
100/-- A theorem bundle is empirically covered if every combination has a falsifier
101protocol. -/