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

firstPassSchedule

show as:
view Lean formalization →

The definition firstPassSchedule supplies the explicit ordered list of five CombinationIDs for the initial empirical tests in Option A. Researchers sequencing validation experiments on oncology tensors, Miller spans, attention tensors, regulatory ceilings, and planet strata would cite this schedule to fix the first-pass execution order. It is realized as a direct five-element list literal with no computation or lemmas.

claimThe first-pass empirical schedule is the ordered list $ [c_3, c_8, c_5, c_9, c_2] $ where each $c_i$ denotes the corresponding CombinationID constructor for oncology tensor, Miller span, attention tensor, regulatory ceiling, and planet strata tests.

background

CombinationID is the inductive type enumerating the implemented Option A combinations (c1 through c9, with c10 left as commentary) from the FalsifierRegistry module. The Option A Empirical Schedule module fixes an explicit execution order for the five highest-priority tests, drawing on the priority assignments from the imported OptionAEmpiricalQueue. The module states that every scheduled item is high-or-immediate and protocol-covered, with the entire file carrying zero sorry statements.

proof idea

The definition is a direct list literal enumerating the five CombinationID constructors in the chosen order. No upstream lemmas are invoked; the body is a plain constructor application.

why it matters in Recognition Science

This schedule is the input to firstPassActions and firstPassDeliverables, which populate the EmpiricalActionPlanCert and EmpiricalDeliverablesCert structures (each requiring nine distinct actions or deliverables). It supplies the concrete ordering for the first five steps of Option A empirical validation, directly supporting the nine-action and nine-deliverable certificates used downstream in the pipeline module.

scope and limits

Lean usage

firstPassSchedule.map analysisAction

formal statement (Lean)

  25def firstPassSchedule : List CombinationID :=

proof body

Definition body.

  26  [ .c3OncologyTensor
  27  , .c8MillerSpan
  28  , .c5AttentionTensor
  29  , .c9RegulatoryCeiling
  30  , .c2PlanetStrata
  31  ]
  32

used by (26)

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

depends on (1)

Lean names referenced from this declaration's body.