deferredTests_exact
deferredTests_exact pins down membership in the deferred empirical tests list by equating it to the defer priority under the empiricalPriority function. Researchers certifying the Option A test queue structure would cite it to confirm which combinations are queued for later validation. The argument is a one-line wrapper that splits cases on the inductive CombinationID and simplifies against the two defining functions.
claimFor every combination identifier $c$, $c$ belongs to the deferred empirical tests list if and only if the empirical priority assigned to $c$ equals defer.
background
The 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, with zero sorry or axiom in the file. deferredTests is the explicit list containing c4QuantumMolecularDepth and c6EriksonReverse. empiricalPriority is the function that maps c3OncologyTensor and c8MillerSpan to immediate, c5AttentionTensor and c2PlanetStrata to high, and c1CognitiveTensor to medium, with defer applying to the remaining defined combinations.
proof idea
The proof is a one-line wrapper that performs case analysis on the inductive CombinationID and then simplifies using the definitions of deferredTests and empiricalPriority.
why it matters in Recognition Science
This theorem supports the construction of empiricalQueueCert by confirming the deferred items in the queue. It contributes to the formalization of the empirical validation queue for Option A combinations, ensuring alignment between listed tests and assigned priorities. The result closes a coverage check within the empirical protocol layer of the Recognition Science framework.
scope and limits
- Does not verify the scientific outcomes or validity of any listed empirical test.
- Does not extend to CombinationID values outside the five constructors defined in the inductive type.
- Does not produce a total ordering or numerical ranking of the queue.
- Does not address the physical content of the underlying C1-C9 theorems.
formal statement (Lean)
139theorem deferredTests_exact (c : CombinationID) :
140 c ∈ deferredTests ↔ empiricalPriority c = .defer := by
proof body
One-line wrapper that applies cases.
141 cases c <;> simp [deferredTests, empiricalPriority]
142