firstPassProgram_exact_top_priority
plain-language theorem explainer
The equivalence asserts that a CombinationID belongs to the first-pass schedule precisely when its empirical priority is high or immediate. Developers of the Option A empirical program cite it to confirm the initial test ordering selects the correct priority tier. The proof is a one-line wrapper delegating directly to the 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 immediate or high.
background
The module supplies a single certificate for the first-pass empirical program attached to Option A, with earlier modules handling queue, schedule, actions, deliverables, pipelines, and readiness. CombinationID is the inductive type of implemented combinations (c1CognitiveTensor through c5AttentionTensor, c10 left as commentary). isHighOrImmediate holds exactly when empiricalPriority $c$ equals immediate or high. firstPassSchedule is the fixed list of five specific identifiers. The upstream theorem firstPassSchedule_mem_iff_high_or_immediate establishes the membership equivalence via exhaustive case analysis on $c$.
proof idea
One-line wrapper that applies firstPassSchedule_mem_iff_high_or_immediate.
why it matters
The result feeds empiricalProgramCert, which assembles the completeness certificate for the first-pass program. It directly supports the claim that the first-pass program contains exactly the high-or-immediate tests, closing one metadata-layer check in the Option A empirical program. No open scaffolding remains in this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.