`FirstPassReady`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.OptionAEmpiricalReadiness
domain: Foundation
line: 56 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.OptionAEmpiricalReadiness on GitHub at line 56.

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

  53  empiricallyReady_all .c5AttentionTensor
  54
  55/-- The first-pass schedule is ready iff every scheduled combination is ready. -/
  56def FirstPassReady : Prop :=
  57  ∀ {c : CombinationID}, c ∈ firstPassSchedule → EmpiricallyReady c
  58
  59theorem firstPassReady : FirstPassReady := by
  60  intro c h
  61  exact scheduled_empiricallyReady h
  62
  63/-- All C1-C9 implemented combinations are ready at the metadata/protocol layer. -/
  64def AllImplementedReady : Prop :=
  65  ∀ c : CombinationID, EmpiricallyReady c
  66
  67theorem allImplementedReady : AllImplementedReady :=
  68  empiricallyReady_all
  69
  70structure EmpiricalReadinessCert where
  71  all_ready : AllImplementedReady
  72  first_pass_ready : FirstPassReady
  73  c3_ready : EmpiricallyReady .c3OncologyTensor
  74  c8_ready : EmpiricallyReady .c8MillerSpan
  75  c5_ready : EmpiricallyReady .c5AttentionTensor
  76
  77def empiricalReadinessCert : EmpiricalReadinessCert where
  78  all_ready := allImplementedReady
  79  first_pass_ready := firstPassReady
  80  c3_ready := c3_ready
  81  c8_ready := c8_ready
  82  c5_ready := c5_ready
  83
  84end OptionAEmpiricalReadiness
  85end Foundation
  86end IndisputableMonolith

papers checked against this theorem

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