isImmediate
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not assert empirical validity of any C1-C9 claim.
- Does not enumerate combinations beyond the five listed in CombinationID.
- Does not supply a falsifier or counterexample for the assigned priorities.
Lean usage
theorem c3_immediate : isImmediate .c3OncologyTensor := rflformal statement (Lean)
44def isImmediate (c : CombinationID) : Prop :=
proof body
Definition body.
45 empiricalPriority c = .immediate
46