immediateTests_exact
The equivalence states that an Option A combination identifier belongs to the immediate empirical tests list exactly when its priority assignment is immediate. Researchers verifying queue ordering for the C1-C9 cross-domain theorems would cite it to confirm protocol sequencing. The proof is a one-line wrapper that performs exhaustive case analysis on the inductive constructors followed by simplification against the defining equations.
claimFor any implemented Option A combination identifier $c$, $c$ belongs to the list of immediate empirical tests if and only if the empirical priority function assigns $c$ the immediate priority level.
background
The module implements a priority queue for empirical tests attached to the C1-C9 cross-domain theorems. It records which protocols to test first and proves that every queued item is already covered by the formal empirical protocol. The empirical priority function is defined by cases on CombinationID, sending the oncology tensor and Miller span combinations to immediate priority, the attention tensor and planet strata combinations to high priority, and the cognitive tensor to medium. The immediate tests list is defined explicitly as the two combinations that receive immediate priority.
proof idea
The proof is a one-line wrapper that applies case analysis to the CombinationID inductive type and then simplifies using the definitions of the immediate tests list and the empirical priority function.
why it matters in Recognition Science
This theorem supports the empiricalQueueCert definition by confirming that the immediate priority assignments match the explicit list. It fills the formal guarantee that queued items align with the priority protocol inside the Option A empirical framework. The result sits inside the foundation layer that attaches empirical tests to the cross-domain theorems without introducing axioms or sorrys.
scope and limits
- Does not establish empirical validity or outcomes of any test.
- Does not cover combinations outside the five implemented Option A cases.
- Does not address scheduling, execution, or resource allocation for the tests.
- Does not prove coverage by the formal empirical protocol beyond queue membership.
formal statement (Lean)
127theorem immediateTests_exact (c : CombinationID) :
128 c ∈ immediateTests ↔ empiricalPriority c = .immediate := by
proof body
One-line wrapper that applies cases.
129 cases c <;> simp [immediateTests, empiricalPriority]
130