firstPassActions_eq
plain-language theorem explainer
The equality fixes the ordered list of first-pass analysis actions to the explicit sequence of fit-factor-model computation, discrete-collapse fitting, plateau detection, regulatory-state counting, and phi-power-ratio estimation. Researchers validating the Option A empirical schedule cite it to anchor the initial test sequence. The proof is a one-line decision procedure that confirms the list equality by direct computation.
Claim. The ordered list of first-pass actions equals the list whose entries are the fit-factor-model action, the discrete-collapse-fitting action, the plateau-detection action, the regulatory-states-counting action, and the phi-power-ratio-estimation action.
background
The Option A empirical action plan supplies concrete analysis action classes for the scheduled empirical tests that support the Recognition Science foundation. First-pass actions are obtained by mapping the first-pass schedule to the corresponding analysis actions, yielding an ordered list of five computational tasks. The upstream definition states that the first-pass actions list is constructed exactly as the image of the schedule under the analysis-action map.
proof idea
The proof is a one-line wrapper that invokes the decide tactic to verify the list equality by decidable computation.
why it matters
This result supplies the concrete list consumed by the empirical action plan certificate and by the length and nodup theorems that follow it. It completes the foundation enumeration of the initial actions required for Option A tests, which in turn feed verification steps for the phi-ladder and related constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.