firstPassActions_length
plain-language theorem explainer
The theorem states that the list of first-pass analysis actions for Option A empirical tests has length five. Researchers verifying the structure of scheduled empirical computations in Recognition Science would cite it to confirm the initial sequence size. The proof reduces the length claim to an explicit list equality and evaluates the result directly.
Claim. The length of the list obtained by mapping the analysis action constructor over the first-pass schedule equals five.
background
The Option A Empirical Action Plan module supplies concrete analysis action classes for scheduled empirical tests. The schedule determines test order while this file specifies the required computation type for each entry. The definition firstPassActions constructs the list by applying the analysisAction mapping to firstPassSchedule. The equality firstPassActions_eq then expands this list to its explicit form containing fitFactorModel, fitDiscreteCollapse, plateauDetection, countRegulatoryStates and one further action.
proof idea
The term-mode proof rewrites the length claim via the equality firstPassActions_eq to obtain the concrete list, then applies decide to confirm that the resulting list has length five.
why it matters
This result supports the empiricalActionPlanCert definition by fixing the size of the initial action segment. It supplies a basic counting step in the Option A schedule verification inside the Recognition Science framework, ensuring the first-pass sequence is fully determined before later certification properties such as action count and injectivity are applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.