empiricalPriority
plain-language theorem explainer
This definition assigns testing priorities to each implemented Option A combination. Researchers specifying the empirical validation pipeline cite it to fix the order of C1-C9 tests. It is realized as an exhaustive pattern match on the combination constructors that returns one of the four priority levels.
Claim. The priority mapping from cross-domain theorem labels to urgency categories is given by the cases: oncology tensor and miller span map to immediate; attention tensor, planet strata, and regulatory ceiling map to high; cognitive tensor and universal response map to medium; quantum molecular depth and erikson reverse map to defer.
background
The module defines a priority queue for empirical tests attached to the C1-C9 cross-domain theorems. The Priority type is an inductive classification with four constructors: immediate, high, medium, and defer. The CombinationID type enumerates the implemented Option A combinations, with C10 left as commentary only.
proof idea
The definition is realized by direct pattern matching on each CombinationID constructor, returning the corresponding Priority value in every case. No lemmas or tactics are invoked; it is an exhaustive case split.
why it matters
This definition supplies the priority field used by pipelineSpec and programSpec to organize empirical validation records for the Option A theorems. It ensures every queued item is formally covered by the empirical protocol and supports the downstream theorems that verify exact priority assignments such as c2_high and deferredTests_exact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.