c9_high
plain-language theorem explainer
The declaration asserts that the regulatory ceiling combination C9 receives high priority under the empiricalPriority mapping. Researchers auditing the Option A test queue would cite it to confirm C9's position after immediate items but ahead of medium ones. The proof reduces immediately to reflexivity on the explicit case in the priority definition.
Claim. The empirical priority function assigns high priority to the regulatory ceiling case: empiricalPriority(c9RegulatoryCeiling) = high.
background
The module implements a priority queue that orders empirical tests for the C1-C9 cross-domain theorems. The function empiricalPriority maps each CombinationID to one of immediate, high, or medium; its definition gives explicit cases for C1-C8 and leaves C9 to be asserted separately. The module documentation states that the queue records which protocols should be tested first while proving formal coverage by the empirical protocol, with zero sorry or axiom in the file.
proof idea
The proof is a one-line wrapper that applies reflexivity directly to the definition of empiricalPriority, which contains the clause mapping c9RegulatoryCeiling to high.
why it matters
The result feeds the empiricalQueueCert construction that assembles the four-priority certificate for the Option A queue. It completes the coverage of all C1-C9 combinations inside the Recognition Science empirical protocol layer, ensuring the test ordering is formally recorded before any physical measurements occur.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.