`empiricalPriority`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.OptionAEmpiricalQueue
domain: Foundation
line: 33 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.OptionAEmpiricalQueue on GitHub at line 33.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  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
  60theorem c3_protocol_covered :
  61    ProtocolFalsifiable .c3OncologyTensor :=
  62  protocolFalsifiable_all .c3OncologyTensor
  63

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.