theorem
proved
analysisAction_count
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.OptionAEmpiricalActionPlan on GitHub at line 36.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
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