c8_protocol
plain-language theorem explainer
The theorem establishes that the c8MillerSpan combination satisfies the ProtocolFalsifiable predicate. Researchers testing Recognition Science Option A predictions against the Miller-Span dataset would cite this to confirm a falsification protocol exists. The proof is a direct one-line application of the general protocolFalsifiable_all theorem to this specific combination identifier.
Claim. The combination identifier c8MillerSpan is protocol-falsifiable: there exist a dataset class $d$, a predicted observable $o$, and a failure mode $f$ such that datasetClass(c8MillerSpan) = $d$, predictedObservable(c8MillerSpan) = $o$, and failureMode(c8MillerSpan) = $f$.
background
This module converts the falsifier registry into Lean propositions asserting that every implemented C1-C9 combination possesses a dataset class, predicted observable, and failure mode. ProtocolFalsifiable is the predicate asserting existence of such a triple for a given CombinationID. The upstream theorem protocolFalsifiable_all establishes the predicate for every CombinationID by direct construction from the registry fields: it unfolds the definition and supplies the three registry values with reflexivity proofs.
proof idea
The proof is a one-line wrapper that applies the general theorem protocolFalsifiable_all to the specific combination .c8MillerSpan.
why it matters
This result supplies the c8_covered field of the empiricalProtocolCert certificate, which aggregates coverage assertions for all implemented Option A combinations. It contributes to the module guarantee of total coverage: no implemented Option A theorem lacks a corresponding falsifier protocol. In the Recognition framework this supports empirical testability of the Option A mass and coupling predictions via the phi-ladder and J-cost structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.