AnalysisAction
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.