`firstPassActions`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.OptionAEmpiricalActionPlan
domain: Foundation
line: 84 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.OptionAEmpiricalActionPlan on GitHub at line 84.

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

  81  hasAnalysisAction_all c
  82
  83/-- First-pass actions in schedule order. -/
  84def firstPassActions : List AnalysisAction :=
  85  firstPassSchedule.map analysisAction
  86
  87theorem firstPassActions_eq :
  88    firstPassActions =
  89      [ .fitFactorModel
  90      , .fitDiscreteCollapse
  91      , .plateauDetection
  92      , .countRegulatoryStates
  93      , .estimatePhiPowerRatio
  94      ] := by
  95  decide
  96
  97theorem firstPassActions_length :
  98    firstPassActions.length = 5 := by
  99  rw [firstPassActions_eq]
 100  decide
 101
 102theorem firstPassActions_nodup :
 103    firstPassActions.Nodup := by
 104  rw [firstPassActions_eq]
 105  decide
 106
 107structure EmpiricalActionPlanCert where
 108  nine_actions : Fintype.card AnalysisAction = 9
 109  action_injective : Function.Injective analysisAction
 110  c3_first_action : analysisAction .c3OncologyTensor = .fitFactorModel
 111  c8_second_action : analysisAction .c8MillerSpan = .fitDiscreteCollapse
 112  c5_third_action : analysisAction .c5AttentionTensor = .plateauDetection
 113  scheduled_actions : ∀ {c : CombinationID}, c ∈ firstPassSchedule → HasAnalysisAction c
 114  first_pass_actions :

papers checked against this theorem

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