AnalysisAction
AnalysisAction enumerates the nine computational tasks required to execute scheduled Option A empirical tests. Researchers validating phi-ladder mass formulas and J-cost protocols cite it when building the analysis pipeline for each CombinationID. The declaration is a direct inductive enumeration deriving decidable equality and finite cardinality.
claimLet $A$ be the inductive type whose constructors are: fitting a factor model, fitting a discrete collapse, detecting a plateau, counting regulatory states, estimating the phi-power ratio, training a multiaxis decoder, fitting a shared response coefficient, benchmarking circuit addressing, and ordering a progression test.
background
The module supplies concrete analysis action classes for the scheduled Option A empirical tests. The schedule fixes execution order; this declaration assigns the required computational step to each test. AnalysisAction is the codomain type for the mapping from CombinationID, carrying decidable equality and finite type structure so that downstream certification structures can perform exhaustive checks.
proof idea
The declaration is an inductive definition that introduces exactly nine constructors. No lemmas are applied and no tactics are used; it is a self-contained enumeration.
why it matters in Recognition Science
It supplies the action vocabulary consumed by the analysisAction mapping, which populates EmpiricalActionPlanCert and PipelineSpec. These structures record full empirical execution records for Option A combinations. The definition closes the interface between schedule and concrete analysis steps inside the Foundation layer without touching the forcing chain or phi-ladder results.
scope and limits
- Does not implement algorithms or data requirements for any action.
- Does not relate actions to specific physical constants or phi-ladder rungs.
- Does not prove injectivity or cardinality of the type.
- Does not reference upstream forcing-chain lemmas.
formal statement (Lean)
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