HasAnalysisAction
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not enumerate the concrete steps inside any analysis action.
- Does not verify that the assigned action suffices to falsify the protocol.
- Does not cover combinations outside the implemented set.
formal statement (Lean)
71def HasAnalysisAction (c : CombinationID) : Prop :=
proof body
Definition body.
72 ∃ a : AnalysisAction, analysisAction c = a
73