c8_immediate
plain-language theorem explainer
The theorem asserts that the C8 Miller-Span combination meets the immediate priority criterion within the empirical testing queue. Developers of the C1-C9 cross-domain theorems cite it when ordering formal empirical protocols. The proof is a direct reflexivity step on the definition of immediate priority.
Claim. The empirical priority of the Miller-Span combination equals the immediate level: $empiricalPriority(c8MillerSpan) = immediate$.
background
The module constructs a priority queue that records the order in which empirical tests for the C1-C9 cross-domain theorems should be executed. The predicate isImmediate holds precisely when a combination's empiricalPriority equals the immediate constructor. This declaration targets the specific case of the C8 Miller-Span combination.
proof idea
One-line wrapper that applies reflexivity to the definition of isImmediate for the c8MillerSpan combination.
why it matters
The result supplies the c8_now field inside the empiricalQueueCert structure, confirming that the C8 protocol is already covered by the formal empirical protocol. It directly supports the module's guarantee that every queued item satisfies the coverage requirement for the C-series theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.