`immediateTests`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.OptionAEmpiricalQueue
domain: Foundation
line: 88 · 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 88.

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

  85  cases c <;> simp [isHighOrImmediate, empiricalPriority]
  86
  87/-- Immediate empirical tests. -/
  88def immediateTests : List CombinationID :=
  89  [.c3OncologyTensor, .c8MillerSpan]
  90
  91/-- High-priority empirical tests after the immediate pair. -/
  92def highPriorityTests : List CombinationID :=
  93  [.c2PlanetStrata, .c5AttentionTensor, .c9RegulatoryCeiling]
  94
  95/-- Medium-priority empirical tests. -/
  96def mediumPriorityTests : List CombinationID :=
  97  [.c1CognitiveTensor, .c7UniversalResponse]
  98
  99/-- Deferred empirical tests. -/
 100def deferredTests : List CombinationID :=
 101  [.c4QuantumMolecularDepth, .c6EriksonReverse]
 102
 103theorem immediateTests_length : immediateTests.length = 2 := by
 104  decide
 105
 106theorem highPriorityTests_length : highPriorityTests.length = 3 := by
 107  decide
 108
 109theorem mediumPriorityTests_length : mediumPriorityTests.length = 2 := by
 110  decide
 111
 112theorem deferredTests_length : deferredTests.length = 2 := by
 113  decide
 114
 115theorem immediateTests_nodup : immediateTests.Nodup := by
 116  decide
 117
 118theorem highPriorityTests_nodup : highPriorityTests.Nodup := by

papers checked against this theorem

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