c5_protocol
plain-language theorem explainer
The theorem shows that the C5 attention tensor combination is protocol-falsifiable, possessing a dataset class, predicted observable, and failure mode. Researchers confirming empirical test coverage for all implemented Option A protocols in Recognition Science cite it to verify completeness. The proof applies the general protocolFalsifiable_all result directly to this combination.
Claim. The C5 attention tensor combination satisfies the predicate that there exist a dataset class $d$, predicted observable $o$, and failure mode $f$ such that the registry assigns datasetClass$(c) = d$, predictedObservable$(c) = o$, and failureMode$(c) = f$ for this combination $c$.
background
The module converts the falsifier registry into Lean propositions, guaranteeing that each implemented C1-C9 combination has a dataset class, predicted observable, and failure mode. ProtocolFalsifiable requires the existence of matching components from the registry functions for a given CombinationID. The upstream theorem protocolFalsifiable_all proves the property for every combination by unfolding the definition and using reflexivity on the registry entries.
proof idea
This is a one-line wrapper that applies protocolFalsifiable_all to the C5 attention tensor combination.
why it matters
It populates the empiricalProtocolCert definition, which aggregates coverage for C1, C3, C5, and C8 protocols. This supports the framework requirement that no implemented Option A theorem lacks a falsifier protocol, ensuring total empirical testability.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.