every_priority_has_protocol
plain-language theorem explainer
Every combination identifier satisfies the protocol falsifiability condition by possessing a matching dataset class, predicted observable, and failure mode. Researchers validating empirical coverage for the C1-C9 cross-domain theorems cite this result to confirm that all queued priorities are formally addressed. The proof is a one-line wrapper applying the universal protocol falsifiability theorem.
Claim. For every combination identifier $c$, there exist a dataset class $d$, a predicted observable $o$, and a failure mode $f$ such that the dataset class of $c$ equals $d$, the predicted observable of $c$ equals $o$, and the failure mode of $c$ equals $f$.
background
The Option A Empirical Queue module records priorities for empirical tests attached to the C1-C9 cross-domain theorems. It proves that every queued item is already covered by a formal empirical protocol, with zero sorry statements or axioms in the module. The protocol falsifiability condition requires that a combination has an associated dataset class, predicted observable, and failure mode in the registry.
proof idea
The proof is a one-line wrapper that applies the protocolFalsifiable_all theorem to the input combination identifier.
why it matters
This result supports the empiricalQueueCert definition, which assembles the certified priority queue with immediate tests for C3 and C8 plus high-priority items for C5 and C2. It fills the formal coverage step in the foundation layer for empirical validation of Recognition Science claims. The module doc states that this records test priorities while proving protocol coverage.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.