c8_action
plain-language theorem explainer
The analysis action mapping sends the Miller Span combination to the discrete collapse fitting procedure. Researchers certifying the Option A empirical action plan cite this equality to confirm the computation type for the second scheduled test. The proof is immediate reflexivity from the case definition of the action assignment function.
Claim. The function assigning analysis actions maps the Miller Span combination identifier to the discrete collapse fitting action: analysisAction(Miller Span) = fitDiscreteCollapse.
background
The Option A Empirical Action Plan module supplies concrete computation classes for each scheduled empirical test. The analysisAction function is defined by pattern matching on CombinationID and assigns to each identifier a specific AnalysisAction such as fitFactorModel for oncology tensor or plateauDetection for attention tensor. The local setting is the concrete specification of actions needed to execute the Option A schedule, with zero axioms or sorrys in the module.
proof idea
The proof is a one-line wrapper that applies reflexivity to the case clause for the Miller Span combination in the definition of analysisAction.
why it matters
It supplies the second action entry in the empiricalActionPlanCert structure that assembles the full certified action plan. This feeds into empiricalPipelineCert to ensure each scheduled combination carries the correct analysis type. In the Recognition framework it supports the empirical validation step by linking specific tests to their required analysis methods.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.