isHighOrImmediate
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not assign priorities to combinations outside the listed Option A set.
- Does not assert validity of any empirical claim.
- Does not constrain testing order beyond first-pass selection.
formal statement (Lean)
47def isHighOrImmediate (c : CombinationID) : Prop :=
proof body
Definition body.
48 empiricalPriority c = .immediate ∨ empiricalPriority c = .high
49