firstPassSchedule_mem_protocol
plain-language theorem explainer
Every CombinationID appearing in the first-pass empirical schedule list satisfies the protocol-falsifiability predicate. Researchers constructing or auditing the Option A test queue would cite this result to confirm uniform protocol coverage before running the ordered tests. The proof is a one-line wrapper that directly invokes the universal protocolFalsifiable_all theorem.
Claim. Let $c$ be a CombinationID. If $c$ belongs to the first-pass schedule list, then $c$ is protocol-falsifiable: there exist a dataset class $d$, predicted observable $o$, and failure mode $f$ such that datasetClass $c = d$, predictedObservable $c = o$, and failureMode $c = f$.
background
The module fixes an explicit ordered list of five CombinationIDs (c3OncologyTensor through c2PlanetStrata) as the first-pass empirical schedule for Option A. ProtocolFalsifiable is the predicate asserting that a given CombinationID possesses matching registry entries for dataset class, predicted observable, and failure mode. The upstream theorem protocolFalsifiable_all states that every CombinationID satisfies this predicate by direct construction from its three registry fields.
proof idea
The proof is a one-line wrapper that applies protocolFalsifiable_all to the input combination c, using the membership hypothesis only to supply the argument.
why it matters
This result is invoked by empiricalScheduleCert to certify that the schedule is fully protocol-covered. It supplies the protocol-coverage half of the module's stated goal (high-or-immediate priority plus protocol coverage) for the initial five tests. In the broader Recognition framework it anchors the empirical falsification step for Option A by guaranteeing that every scheduled combination carries an explicit failure mode.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.