pith. machine review for the scientific record. sign in
def definition def or abbrev high

empiricalPriority

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

Lean usage

def priorityExample : Priority := empiricalPriority .c5AttentionTensor

formal statement (Lean)

  33def empiricalPriority : CombinationID → Priority
  34  | .c3OncologyTensor => .immediate
  35  | .c8MillerSpan => .immediate
  36  | .c5AttentionTensor => .high
  37  | .c2PlanetStrata => .high
  38  | .c1CognitiveTensor => .medium
  39  | .c7UniversalResponse => .medium
  40  | .c4QuantumMolecularDepth => .defer
  41  | .c6EriksonReverse => .defer
  42  | .c9RegulatoryCeiling => .high
  43

used by (16)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.