firstPassSchedule_mem_high_or_immediate
plain-language theorem explainer
The theorem asserts that every CombinationID in the first-pass schedule satisfies the high-or-immediate empirical priority predicate. Researchers validating Option A empirical test ordering would cite it to confirm schedule integrity before running the queue. The proof reduces list membership to a five-way disjunction via simplification then verifies the priority condition by direct substitution in each case.
Claim. Let $S$ be the list $[c_3, c_8, c_5, c_9, c_2]$ of CombinationIDs. For every $c$ such that $c$ belongs to $S$, the empirical priority of $c$ equals immediate or high.
background
The module fixes an explicit first-pass schedule as the list of five CombinationIDs (c3OncologyTensor, c8MillerSpan, c5AttentionTensor, c9RegulatoryCeiling, c2PlanetStrata) drawn from the Option A falsifier registry. The predicate isHighOrImmediate holds precisely when empiricalPriority maps the CombinationID to immediate or high, with the priority assignment given by the sibling queue module: c3 and c8 receive immediate, c5 and c2 receive high. The module doc states that this schedule fixes execution order for high-value tests and proves every scheduled item is high-or-immediate.
proof idea
The term proof first simplifies the membership hypothesis against the explicit list definition of firstPassSchedule, producing a disjunction of five equalities. Case analysis on each disjunct substitutes the equality and simplifies using the definitions of isHighOrImmediate and empiricalPriority, confirming the disjunction holds for each of the five concrete CombinationIDs.
why it matters
The result supplies the priority-membership direction needed for the EmpiricalScheduleCert constructed downstream, which bundles length, head, second, third, and no-duplicates properties. It directly supports the sibling claim that the schedule contains exactly the high-or-immediate tests. Within the Recognition Science foundation layer it supplies a concrete, machine-checked fragment of the empirical protocol attached to Option A falsifier combinations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.