isImmediate
plain-language theorem explainer
The definition marks a CombinationID as immediate priority when its empiricalPriority equals the immediate case. Researchers formalizing the Option A empirical queue for C1-C9 theorems cite it to certify testing order. It is implemented as a direct equality to the immediate branch of the priority function.
Claim. For a combination identifier $c$, the predicate isImmediate$(c)$ holds if and only if the empirical priority of $c$ is immediate.
background
The module defines a priority queue that records the order in which empirical tests for the C1-C9 cross-domain theorems should be performed. It does not supply evidence for those theorems but proves that every queued item is already covered by the formal empirical protocol. The upstream CombinationID inductive enumerates the implemented combinations, while empiricalPriority maps c3OncologyTensor and c8MillerSpan to immediate, c5AttentionTensor and c2PlanetStrata to high, and c1CognitiveTensor to medium.
proof idea
The definition is a one-line wrapper that equates isImmediate c to the proposition empiricalPriority c = .immediate.
why it matters
The definition is used directly by the theorems c3_immediate and c8_immediate, by the structure EmpiricalQueueCert that certifies the queue, and by the theorem immediate_iff that characterizes the two immediate tests. It fills the role of identifying the first items in the empirical protocol queue inside the Option A framework, ensuring formal coverage of the priority assignments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.