firstPassSchedule_mem_iff_high_or_immediate
plain-language theorem explainer
The first-pass empirical schedule for Option A consists exactly of those combination identifiers whose empirical priority is high or immediate. Researchers auditing the empirical validation path in Recognition Science would cite this equivalence to confirm the test ordering. The proof is a one-line wrapper applying case analysis on the identifier followed by simplification with the priority definitions.
Claim. For any combination identifier $c$, $c$ belongs to the ordered first-pass empirical test schedule if and only if the empirical priority of $c$ is immediate or high.
background
The module establishes an ordered schedule for the first five empirical tests in Option A. The upstream empirical priority definition assigns immediate status to the oncology tensor and Miller span combinations, high status to the attention tensor and planet strata combinations. The high-or-immediate predicate is the disjunction of these two priority levels. This local setting verifies that the explicit schedule list matches precisely the top-priority tests, as part of the foundation for Option A empirical program.
proof idea
The proof performs case analysis on the combination identifier and simplifies the resulting membership statement against the explicit list definition of the schedule together with the definitions of the high-or-immediate predicate and the priority function.
why it matters
It is invoked in the completeness theorem for the first-pass program and in the exact top-priority statement for that program. The result verifies the schedule construction in the empirical schedule module for Option A, closing a verification step in the foundation layer of the Recognition framework with no remaining open questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.