`programSpec`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.OptionAEmpiricalProgram
domain: Foundation
line: 39 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.OptionAEmpiricalProgram on GitHub at line 39.

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

  36  ready : EmpiricallyReady combination
  37
  38/-- Program row assigned to an implemented Option A combination. -/
  39def programSpec (c : CombinationID) : ProgramSpec where
  40  combination := c
  41  protocol := protocolSpec c
  42  priority := empiricalPriority c
  43  action := analysisAction c
  44  deliverable := deliverableFor c
  45  pipeline := pipelineSpec c
  46  ready := empiricallyReady_all c
  47
  48theorem programSpec_injective : Function.Injective programSpec := by
  49  intro a b h
  50  exact congrArg ProgramSpec.combination h
  51
  52/-- First-pass empirical program in execution order. -/
  53def firstPassProgram : List ProgramSpec :=
  54  firstPassSchedule.map programSpec
  55
  56theorem firstPassProgram_length :
  57    firstPassProgram.length = 5 := by
  58  unfold firstPassProgram
  59  rw [List.length_map, firstPassSchedule_length]
  60
  61theorem firstPassProgram_nodup :
  62    firstPassProgram.Nodup := by
  63  unfold firstPassProgram
  64  exact List.Nodup.map programSpec_injective firstPassSchedule_nodup
  65
  66/-- The first-pass program contains exactly the high-or-immediate tests. -/
  67theorem firstPassProgram_exact_top_priority (c : CombinationID) :
  68    c ∈ firstPassSchedule ↔ isHighOrImmediate c :=
  69  firstPassSchedule_mem_iff_high_or_immediate c

papers checked against this theorem

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