`AnalysisAction`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.OptionAEmpiricalActionPlan on GitHub at line 24.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

used by

formal source

  21open OptionAEmpiricalSchedule
  22
  23/-- Coarse computational action needed to test a protocol. -/
  24inductive AnalysisAction where
  25  | fitFactorModel
  26  | fitDiscreteCollapse
  27  | plateauDetection
  28  | countRegulatoryStates
  29  | estimatePhiPowerRatio
  30  | trainMultiaxisDecoder
  31  | fitSharedResponseCoefficient
  32  | benchmarkCircuitAddressing
  33  | orderProgressionTest
  34  deriving DecidableEq, Repr, Fintype
  35
  36theorem analysisAction_count : Fintype.card AnalysisAction = 9 := by
  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

papers checked against this theorem

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