firstPassSchedule
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.