firstPassProgram_exact_top_priority
plain-language theorem explainer
The equivalence asserts that any CombinationID belongs to the first-pass schedule precisely when its empirical priority is high or immediate. Researchers certifying the Option A empirical program cite this when confirming the initial test sequence is complete. The proof is a one-line wrapper that invokes the upstream schedule membership theorem.
Claim. For any combination identifier $c$, $c$ belongs to the first-pass empirical test schedule if and only if the empirical priority of $c$ is either immediate or high.
background
The module supplies a single certificate for the first-pass empirical program attached to Option A. Earlier modules establish the queue, schedule, actions, deliverables, pipelines, and readiness separately; this file assembles them to prove the program is complete and collision-free at the metadata layer, with zero sorrys and zero axioms.
proof idea
The proof is a one-line wrapper that applies the theorem firstPassSchedule_mem_iff_high_or_immediate to the input combination identifier.
why it matters
This theorem feeds the first_pass_complete field inside the empiricalProgramCert definition. It confirms the assembled first-pass program begins exactly with the high-or-immediate tests required by the Option A structure. The upstream schedule membership result, whose doc-comment states that the first-pass schedule contains exactly the high-or-immediate tests, supplies the concrete list and priority cases.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.