analysisAction_injective
plain-language theorem explainer
The assignment of analysis actions to Option A combination identifiers is injective. Certificate builders for empirical Option A tests cite this to guarantee distinct identifiers produce distinct actions. The proof uses case analysis on the pair of identifiers followed by simplification against the action assignment definition.
Claim. The function mapping each combination identifier to its assigned analysis action is injective.
background
This module supplies the concrete analysis actions needed for each scheduled Option A empirical test. The schedule determines execution order while this file determines the computational type of each test. The key definition maps the five implemented combinations to distinct actions: fit factor model, discrete collapse, plateau detection, regulatory state counting, and phi power ratio estimation.
proof idea
The proof begins by introducing two identifiers a and b along with the equality of their images. Exhaustive case splitting on the constructors of a and b produces a finite collection of subgoals. Each subgoal is resolved by rewriting with the definition of the assignment function.
why it matters
This injectivity is a required field in the empirical action plan certificate. The certificate also records the total number of actions and the specific actions for the first three scheduled combinations. It thereby provides a verified foundation for running the Option A tests in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.