HasAnalysisAction

formal source

  68    analysisAction .c2PlanetStrata = .estimatePhiPowerRatio := rfl
  69
  70/-- Every scheduled first-pass item has an analysis action. -/
  71def HasAnalysisAction (c : CombinationID) : Prop :=
  72  ∃ a : AnalysisAction, analysisAction c = a
  73
  74theorem hasAnalysisAction_all (c : CombinationID) :
  75    HasAnalysisAction c := by
  76  exact ⟨analysisAction c, rfl⟩
  77
  78theorem scheduled_has_analysis_action
  79    {c : CombinationID} (_h : c ∈ firstPassSchedule) :
  80    HasAnalysisAction c :=
  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