firstPassSchedule_length
plain-language theorem explainer
The first-pass empirical test schedule for Option A has length exactly five. Researchers building empirical validation pipelines cite this to fix the size of the initial test sequence before mapping to pipelines or programs. The proof evaluates the explicit list definition via a single decision procedure.
Claim. Let $S$ be the ordered list of the first five empirical tests in Option A. Then $|S| = 5$.
background
The module fixes an explicit execution order for the first five empirical tests attached to Option A after the queue module assigns priorities. The upstream definition firstPassSchedule supplies the concrete list [c3OncologyTensor, c8MillerSpan, c5AttentionTensor, c9RegulatoryCeiling, c2PlanetStrata]. This establishes a deterministic schedule whose length is then certified for downstream use.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the equality between the length of the explicitly defined list and five.
why it matters
This length fact is invoked by firstPassPipelines_length, firstPassProgram_length, and empiricalScheduleCert to establish fixed sizes and construct the schedule certificate. It anchors the initial empirical sequence in the foundation layer before further composition steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.