pith. machine review for the scientific record. sign in
def definition def or abbrev high

firstPassActions

show as:
view Lean formalization →

firstPassActions assembles the ordered list of computational steps for the initial Option A empirical tests. Validation teams cite this list to fix the exact analysis procedures attached to each scheduled protocol combination. The definition is a direct mapping of the first-pass schedule through the action assignment function.

claimLet $S$ be the ordered list of protocol combinations for the first empirical pass. Let $a$ be the function assigning to each combination its required coarse computational action. The first-pass actions list is then the elementwise image of $S$ under $a$.

background

The module introduces AnalysisAction as the inductive type enumerating coarse computational actions needed to test protocols. These comprise fitting factor models, detecting discrete collapse, identifying plateaus, counting regulatory states, and estimating phi power ratios. The firstPassSchedule supplies the ordered list of specific combinations for the initial tests: oncology tensor, Miller span, attention tensor, regulatory ceiling, and planet strata.

proof idea

The definition is a one-line wrapper that applies the map operation from the schedule definition using analysisAction as the transformer.

why it matters in Recognition Science

This definition supplies the concrete action sequence used by EmpiricalActionPlanCert to certify the plan and by the equality theorem that states the explicit list. It feeds into EmpiricalProgramCert and the nodup and length properties downstream. Within the Recognition framework it operationalizes the first stage of the empirical schedule that probes the phi-ladder structures before full program certification.

scope and limits

formal statement (Lean)

  84def firstPassActions : List AnalysisAction :=

proof body

Definition body.

  85  firstPassSchedule.map analysisAction
  86

used by (7)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.