c9_action
plain-language theorem explainer
The mapping assigns the count-regulatory-states action to the regulatory ceiling test case by definition. Empirical researchers validating Option A schedules reference this to fix the computational task for that combination. The proof reduces immediately by reflexivity to the case clause in the action assignment function.
Claim. The analysis action required for the regulatory ceiling combination is the count of regulatory states: $analysisAction(c9RegulatoryCeiling) = countRegulatoryStates$.
background
The module supplies concrete analysis action classes for the scheduled Option A empirical tests. The schedule fixes execution order while this file fixes the computation type each test demands. The upstream definition analysisAction : CombinationID → AnalysisAction enumerates the mapping, with the c9RegulatoryCeiling case returning countRegulatoryStates.
proof idea
One-line wrapper that applies reflexivity to the defining equation of analysisAction at the c9 case.
why it matters
This declaration completes the action specification for the c9 regulatory ceiling entry in the Option A empirical plan. It ensures the computational requirement is fixed before any schedule execution. No parent theorems or chain steps depend on it in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.