HasAnalysisAction
plain-language theorem explainer
HasAnalysisAction asserts that every Option A combination identifier is assigned a concrete computational action by the analysisAction map. Empirical test schedulers cite it to confirm that all first-pass protocols have designated analysis steps before execution. The definition is a direct existential wrapper over the pre-defined analysisAction function.
Claim. For every Option A combination identifier $c$, there exists a computational action $a$ such that the action required by $c$ equals $a$.
background
The Option A Empirical Action Plan module supplies concrete analysis action classes for the scheduled empirical tests. The schedule determines execution order while this file assigns the required computation type to each test. AnalysisAction is the inductive type listing the five tasks: fitFactorModel, fitDiscreteCollapse, plateauDetection, countRegulatoryStates, and estimatePhiPowerRatio. The function analysisAction maps each implemented CombinationID to its assigned task, for example sending c3OncologyTensor to fitFactorModel.
proof idea
The definition is a one-line wrapper that asserts existence of an AnalysisAction witness equal to the value returned by analysisAction on the input CombinationID.
why it matters
This definition feeds EmpiricalActionPlanCert, hasAnalysisAction_all, scheduled_has_analysis_action, and the EmpiricallyReady predicate. It ensures every first-pass scheduled item carries a defined computational task, closing the link between the Option A schedule and executable analysis steps in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.