mediumPriorityTests_exact
plain-language theorem explainer
The theorem establishes the exact membership condition for medium-priority empirical tests in the Option A queue. Researchers maintaining the formal empirical protocol would cite it to confirm queue ordering consistency. The proof is a one-line wrapper that performs exhaustive case analysis on the CombinationID inductive type followed by simplification against the list and priority definitions.
Claim. For every combination identifier $c$, $c$ belongs to the medium-priority tests list if and only if the empirical priority of $c$ equals medium.
background
The module sets up a priority queue for empirical tests attached to C1-C9 cross-domain theorems. It records test ordering and proves formal coverage by the empirical protocol without supplying evidence for the claims themselves. CombinationID is the inductive type enumerating implemented Option A combinations. The function empiricalPriority assigns each identifier a priority level (immediate, high, or medium). The constant mediumPriorityTests is the explicit list of those assigned medium priority.
proof idea
The proof is a one-line wrapper that applies case analysis to the inductive type CombinationID and then simplifies using the definitions of mediumPriorityTests and empiricalPriority.
why it matters
This result feeds the empiricalQueueCert definition, which assembles the full queue certificate including priority counts and immediate/high assignments. It verifies that the medium-priority list exactly matches the priority function, closing one consistency check in the module's formal protocol coverage. The declaration sits in the empirical validation layer of the Recognition framework and touches the scaffolding for cross-domain theorem testing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.