high_or_immediate_iff
plain-language theorem explainer
The theorem states that a CombinationID has high or immediate empirical priority exactly when it matches one of five specific combinations: c2PlanetStrata, c3OncologyTensor, c5AttentionTensor, c8MillerSpan, or c9RegulatoryCeiling. Researchers sequencing Option A empirical tests would cite this equivalence to determine which protocols must be run first. The proof is a one-line term-mode case split on the inductive CombinationID followed by simplification with the priority definitions.
Claim. Let $c$ be a CombinationID. The empirical priority of $c$ is immediate or high if and only if $c$ equals c2PlanetStrata, c3OncologyTensor, c5AttentionTensor, c8MillerSpan, or c9RegulatoryCeiling.
background
The module implements a priority queue for empirical tests attached to the C1-C9 cross-domain theorems. It records which protocols should be tested first and proves that every queued item is already covered by the formal empirical protocol. The empiricalPriority definition maps each CombinationID to a priority level, sending c3OncologyTensor and c8MillerSpan to immediate, c5AttentionTensor and c2PlanetStrata to high, and the remainder to medium. The isHighOrImmediate predicate is defined as the disjunction of those two priority cases.
proof idea
The proof performs exhaustive case analysis on the inductive CombinationID and then simplifies using the definitions of isHighOrImmediate and empiricalPriority. This directly verifies the listed constructors match the high-or-immediate cases while all others do not.
why it matters
The result feeds the empiricalQueueCert construction that assembles the certified priority counts and immediate/high flags. It supplies the explicit list of the five tests that should precede the rest, as stated in the module documentation, within the Option A empirical protocol. The declaration is fully proved with no open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.