firstPassSchedule_second
plain-language theorem explainer
The second position in the explicit first-pass empirical test list is the Miller span combination. Researchers certifying Option A test sequences reference this fact when assembling the full schedule certificate. The proof is a direct decision procedure on the concrete list definition supplied by the upstream schedule construction.
Claim. Let $S = [C_3, C_8, C_5, C_9, C_2]$ be the ordered list of CombinationID values for the first five Option A empirical tests. Then the element at 0-based index 1 equals the Miller span combination: $S[1] = C_8$.
background
The module fixes an explicit execution order for the high-value tests attached to Option A. The queue module assigns priorities while this module proves every scheduled item is high-or-immediate and protocol-covered. The local setting is the foundation layer that supplies deterministic schedule facts with zero axioms or sorrys.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the explicit list definition of firstPassSchedule.
why it matters
The result is consumed by empiricalScheduleCert, which packages length, head, second, third, and no-duplicates properties into a single certificate object. It supplies one of the five concrete facts required to certify the Option A empirical schedule in the Recognition Science foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.