highPriorityTests_exact
Researchers confirming the structure of the Option A empirical priority queue cite this result to verify that the high-priority test list matches exactly the combinations assigned high priority by the empiricalPriority function. The equivalence holds for all CombinationID values. The proof is a one-line case analysis on the inductive type followed by definitional simplification.
claimFor every combination identifier $c$, $c$ belongs to the high-priority test list if and only if the empirical priority function assigns $c$ the value high.
background
The OptionAEmpiricalQueue 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. CombinationID is the inductive type enumerating the implemented combinations. The function empiricalPriority maps each such identifier to a Priority value (immediate, high, or medium). The constant highPriorityTests is the list containing c2PlanetStrata, c5AttentionTensor, and c9RegulatoryCeiling, the high-priority items after the immediate pair.
proof idea
The proof is a one-line wrapper that applies case analysis to the inductive type CombinationID. Simplification then unfolds the definitions of highPriorityTests and empiricalPriority to establish the biconditional for each constructor.
why it matters in Recognition Science
This result supports the empiricalQueueCert definition, which assembles the certified queue using priority counts and specific high-priority items such as c5 and c2. It fills the formal step ensuring the queued tests align with their assigned priorities in the Option A empirical protocol. In the Recognition framework it contributes to coverage of the cross-domain theorems without supplying empirical evidence.
scope and limits
- Does not prove the physical validity of any test protocol.
- Does not enumerate combinations outside the inductive CombinationID type.
- Does not include immediate-priority or medium-priority items.
- Does not address the full empirical protocol coverage beyond the queue.
formal statement (Lean)
131theorem highPriorityTests_exact (c : CombinationID) :
132 c ∈ highPriorityTests ↔ empiricalPriority c = .high := by
proof body
One-line wrapper that applies cases.
133 cases c <;> simp [highPriorityTests, empiricalPriority]
134