`ProgramSpec`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.OptionAEmpiricalProgram on GitHub at line 29.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  26open OptionAEmpiricalReadiness
  27
  28/-- One executable row in the Option A first-pass empirical program. -/
  29structure ProgramSpec where
  30  combination : CombinationID
  31  protocol : ProtocolSpec
  32  priority : Priority
  33  action : AnalysisAction
  34  deliverable : Deliverable
  35  pipeline : PipelineSpec
  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]

papers checked against this theorem

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