scheduled_has_analysis_action
plain-language theorem explainer
Every combination identifier in the first-pass empirical test schedule possesses a corresponding analysis action. Workers constructing the Option A test plan cite this to confirm the initial schedule items are all actionable. The argument reduces immediately to the universal lemma that every combination identifier carries an analysis action.
Claim. For every combination identifier $c$ belonging to the first-pass schedule, there exists an analysis action $a$ such that the analysis action assigned to $c$ equals $a$.
background
The module supplies concrete analysis action classes for the scheduled Option A empirical tests. The schedule fixes the order of first-pass tests while this file assigns the required computation type to each entry. HasAnalysisAction asserts that every scheduled first-pass item possesses an analysis action, formalized as the existence of an AnalysisAction $a$ satisfying analysisAction $c = a$. The upstream result hasAnalysisAction_all establishes the property for arbitrary combination identifiers by direct construction from the analysisAction function.
proof idea
The proof is a one-line wrapper applying hasAnalysisAction_all directly to the given combination identifier $c$.
why it matters
This result confirms that every entry in the first-pass schedule is covered by an analysis action and is invoked inside the construction of empiricalActionPlanCert, which assembles the full certification of the action plan including action counts, injectivity, and per-combination assignments. It closes a basic interface requirement for the Option A empirical test framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.