theorem
proved
priority_count
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.OptionAEmpiricalQueue on GitHub at line 29.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
26 | defer
27 deriving DecidableEq, Repr, Fintype
28
29theorem priority_count : Fintype.card Priority = 4 := by
30 decide
31
32/-- Empirical priority for the implemented Option A combinations. -/
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
44def isImmediate (c : CombinationID) : Prop :=
45 empiricalPriority c = .immediate
46
47def isHighOrImmediate (c : CombinationID) : Prop :=
48 empiricalPriority c = .immediate ∨ empiricalPriority c = .high
49
50theorem c3_immediate : isImmediate .c3OncologyTensor := rfl
51
52theorem c8_immediate : isImmediate .c8MillerSpan := rfl
53
54theorem c5_high : empiricalPriority .c5AttentionTensor = .high := rfl
55
56theorem c2_high : empiricalPriority .c2PlanetStrata = .high := rfl
57
58theorem c9_high : empiricalPriority .c9RegulatoryCeiling = .high := rfl
59