`c3_protocol_covered`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.OptionAEmpiricalQueue on GitHub at line 60.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  57
  58theorem c9_high : empiricalPriority .c9RegulatoryCeiling = .high := rfl
  59
  60theorem c3_protocol_covered :
  61    ProtocolFalsifiable .c3OncologyTensor :=
  62  protocolFalsifiable_all .c3OncologyTensor
  63
  64theorem c8_protocol_covered :
  65    ProtocolFalsifiable .c8MillerSpan :=
  66  protocolFalsifiable_all .c8MillerSpan
  67
  68theorem every_priority_has_protocol (c : CombinationID) :
  69    ProtocolFalsifiable c :=
  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

papers checked against this theorem

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