firstPassProgram_exact_top_priority
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not establish the empirical priority values assigned to each combination.
- Does not address properties of the full empirical program beyond the first pass.
- Does not prove collision checks or readiness conditions.
- Does not cover lower-priority tests or later pipeline stages.
Lean usage
theorem use_in_cert (c : CombinationID) : c ∈ firstPassSchedule ↔ isHighOrImmediate c := firstPassProgram_exact_top_priority cformal statement (Lean)
67theorem firstPassProgram_exact_top_priority (c : CombinationID) :
68 c ∈ firstPassSchedule ↔ isHighOrImmediate c :=
proof body
One-line wrapper that applies firstPassSchedule_mem_iff_high_or_immediate.
69 firstPassSchedule_mem_iff_high_or_immediate c
70