immediate_iff
plain-language theorem explainer
The equivalence states that a combination identifier is immediate precisely when it is the oncology tensor or Miller span case. Researchers maintaining the Option A empirical test queue would cite this to fix the leading positions for C3 and C8. The proof runs by exhaustive case analysis on the identifier followed by simplification against the priority assignment.
Claim. Let $c$ be a combination identifier. Then $c$ is immediate if and only if $c$ is the oncology tensor combination or the Miller span combination.
background
CombinationID is the inductive type enumerating the implemented Option A combinations. The definition empiricalPriority maps c3OncologyTensor and c8MillerSpan to the immediate priority, c5AttentionTensor and c2PlanetStrata to high, and c1CognitiveTensor to medium. isImmediate is the predicate that holds exactly when empiricalPriority returns immediate. The module maintains a priority queue for empirical tests attached to the C1-C9 cross-domain theorems and proves that every queued item is already covered by the formal empirical protocol; it records ordering but supplies no evidence for the claims themselves.
proof idea
The proof performs case analysis on the combination identifier c. Each case is discharged by simplification using the definitions of isImmediate and empiricalPriority, which directly produces the required disjunction for the two immediate constructors and falsehood for the rest.
why it matters
The result feeds empiricalQueueCert, which assembles the certified four-priority queue with explicit markers for c3 and c8 immediate. It identifies the two leading tests inside the Option A protocol, consistent with the eight-tick geometry and the cross-domain theorem coverage. The declaration touches no open analytic questions such as the phi-ladder Poisson summation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.