analysisAction_injective
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove surjectivity of the mapping onto all analysis actions.
- Does not detail the internal algorithms of the individual analysis actions.
- Does not relate the actions to the eight-tick octave or spatial dimension results.
- Does not guarantee uniqueness under extensions of the combination identifier type.
Lean usage
def empiricalActionPlanCert : EmpiricalActionPlanCert where nine_actions := analysisAction_count action_injective := analysisAction_injective c3_first_action := c3_action c8_second_action := c8_action c5_third_action := c5_actionformal statement (Lean)
51theorem analysisAction_injective : Function.Injective analysisAction := by
proof body
Term-mode proof.
52 intro a b h
53 cases a <;> cases b <;> simp [analysisAction] at h ⊢
54