hasAnalysisAction_all
plain-language theorem explainer
Every implemented Option A combination identifier possesses a concrete analysis action. Empirical readiness proofs cite this result to confirm that each scheduled test case carries a defined computational procedure. The proof is a direct one-line wrapper that supplies the witness from the action mapping and closes by reflexivity.
Claim. For every combination identifier $c$, there exists an analysis action $a$ such that the required action for $c$ equals $a$.
background
The module supplies concrete analysis action classes for the scheduled Option A empirical tests. The function analysisAction assigns to each CombinationID a specific AnalysisAction: oncology tensor maps to fit-factor model, Miller span to discrete collapse, attention tensor to plateau detection, regulatory ceiling to regulatory-state count, and planet strata to phi-power ratio estimate. HasAnalysisAction is the proposition that every such combination admits at least one such action, expressed as an existential over the image of analysisAction.
proof idea
One-line wrapper that applies exact to the pair formed by analysisAction c and reflexivity of equality.
why it matters
The theorem is invoked directly by scheduled_has_analysis_action to restrict attention to first-pass schedule items and by empiricallyReady_all to assemble the full empirical-readiness predicate. It completes the specification layer of the Option A empirical plan, ensuring every implemented combination carries an explicit analysis procedure before any falsification or readiness claim is asserted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.