Priority
The Priority inductive type introduces four ordered levels for empirical test scheduling in the Option A queue: immediate, high, medium, and defer. Researchers building the C1-C9 empirical program cite it when constructing pipeline and program specifications that attach priorities to protocol combinations. The declaration is a direct inductive definition that derives decidable equality, representation, and finite type instances in one clause.
claimLet $P$ be the inductive type whose constructors are immediate, high, medium, and defer; $P$ is equipped with decidable equality, a representation instance, and a finite type structure.
background
This definition lives in the Option A Empirical Queue module, whose purpose is to supply a priority queue for empirical tests attached to the C1-C9 cross-domain theorems. The module records which protocols should be tested first and proves that every queued item is already covered by the formal empirical protocol. No upstream lemmas are required; the type is introduced as a primitive building block for the queue.
proof idea
The declaration is an inductive definition with four constructors followed by a deriving clause that installs the DecidableEq, Repr, and Fintype instances automatically.
why it matters in Recognition Science
Priority is referenced by PipelineSpec and ProgramSpec to annotate empirical rows, by empiricalPriority to map specific combinations (c3OncologyTensor and c8MillerSpan to immediate; c5AttentionTensor and c2PlanetStrata to high), and by EmpiricalQueueCert to certify the four-level structure. It supplies the ordering mechanism for the first-pass empirical program inside the Recognition Science Option A framework.
scope and limits
- Does not assign numerical weights or comparison functions to the levels.
- Does not prove that any particular protocol combination satisfies a given priority.
- Does not define queue insertion or removal operations.
- Does not encode the empiricalPriority mapping itself.
formal statement (Lean)
22inductive Priority where
23 | immediate
24 | high
25 | medium
26 | defer
27 deriving DecidableEq, Repr, Fintype
28