  70  protocolFalsifiable_all c
  71
  72/-- The two immediate tests are C3 and C8. -/
  73theorem immediate_iff (c : CombinationID) :
  74    isImmediate c ↔ c = .c3OncologyTensor ∨ c = .c8MillerSpan := by
  75  cases c <;> simp [isImmediate, empiricalPriority]
  76
  77/-- High-or-immediate items are the five tests that should precede the rest. -/
  78theorem high_or_immediate_iff (c : CombinationID) :
  79    isHighOrImmediate c ↔
  80      c = .c2PlanetStrata ∨
  81      c = .c3OncologyTensor ∨
  82      c = .c5AttentionTensor ∨
  83      c = .c8MillerSpan ∨
  84      c = .c9RegulatoryCeiling := by
  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

papers checked against this theorem

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