`analysisAction`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.OptionAEmpiricalActionPlan on GitHub at line 40.

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

  37  decide
  38
  39/-- Action required by each implemented Option A combination. -/
  40def analysisAction : CombinationID → AnalysisAction
  41  | .c3OncologyTensor => .fitFactorModel
  42  | .c8MillerSpan => .fitDiscreteCollapse
  43  | .c5AttentionTensor => .plateauDetection
  44  | .c9RegulatoryCeiling => .countRegulatoryStates
  45  | .c2PlanetStrata => .estimatePhiPowerRatio
  46  | .c1CognitiveTensor => .trainMultiaxisDecoder
  47  | .c7UniversalResponse => .fitSharedResponseCoefficient
  48  | .c4QuantumMolecularDepth => .benchmarkCircuitAddressing
  49  | .c6EriksonReverse => .orderProgressionTest
  50
  51theorem analysisAction_injective : Function.Injective analysisAction := by
  52  intro a b h
  53  cases a <;> cases b <;> simp [analysisAction] at h ⊢
  54
  55theorem c3_action :
  56    analysisAction .c3OncologyTensor = .fitFactorModel := rfl
  57
  58theorem c8_action :
  59    analysisAction .c8MillerSpan = .fitDiscreteCollapse := rfl
  60
  61theorem c5_action :
  62    analysisAction .c5AttentionTensor = .plateauDetection := rfl
  63
  64theorem c9_action :
  65    analysisAction .c9RegulatoryCeiling = .countRegulatoryStates := rfl
  66
  67theorem c2_action :
  68    analysisAction .c2PlanetStrata = .estimatePhiPowerRatio := rfl
  69
  70/-- Every scheduled first-pass item has an analysis action. -/

papers checked against this theorem

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