firstPassSchedule_mem_protocol
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove that every element of the schedule is high-priority.
- Does not enumerate the concrete datasets or observables attached to each CombinationID.
- Does not address completeness of the schedule or later passes.
- Does not constrain the order beyond membership.
formal statement (Lean)
74theorem firstPassSchedule_mem_protocol
75 {c : CombinationID} (_h : c ∈ firstPassSchedule) :
76 ProtocolFalsifiable c :=
proof body
One-line wrapper that applies protocolFalsifiable_all.
77 protocolFalsifiable_all c
78