isHighOrImmediate
plain-language theorem explainer
The predicate selects combinations whose empirical priority is immediate or high. Scheduling proofs for the Option A first-pass program cite it to isolate the initial five tests. It is realized as a direct disjunction on the output of the empiricalPriority assignment function.
Claim. A combination $c$ satisfies the predicate when its empirical priority equals immediate or equals high.
background
The module records a priority queue for empirical tests attached to the C1-C9 cross-domain theorems. CombinationID enumerates the implemented Option A combinations. The empiricalPriority function maps c3OncologyTensor and c8MillerSpan to immediate, c5AttentionTensor and c2PlanetStrata to high, and c1CognitiveTensor to medium.
proof idea
One-line definition that applies the disjunction to the two priority cases returned by empiricalPriority.
why it matters
It is referenced by EmpiricalQueueCert to certify the immediate and high items and by firstPassProgram_exact_top_priority to equate first-pass schedule membership with this predicate. The definition closes the interface between priority assignment and program completeness in the empirical testing queue for Option A.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.