deferredTests
plain-language theorem explainer
deferredTests supplies the concrete list of two CombinationIDs marked for deferred empirical testing in the Option A protocol. Researchers validating the Recognition Science cross-domain theorems would reference this list when prioritizing experiments on quantum molecular depth and Erikson reverse. The definition is a direct enumeration of the two items.
Claim. The deferred empirical tests are the list consisting of the quantum-molecular-depth combination and the Erikson-reverse combination, where each is an element of the inductive type of implemented Option A combinations.
background
The module maintains a priority queue for empirical tests attached to the C1-C9 cross-domain theorems. CombinationID is the inductive type enumerating the implemented combinations (c1CognitiveTensor through c9, with c10 left as commentary). empiricalPriority is the sibling function that assigns each CombinationID one of four priorities, including the defer case used by downstream theorems.
proof idea
Direct definition that constructs the list literal containing c4QuantumMolecularDepth and c6EriksonReverse. No lemmas or tactics are invoked; the body is a single list expression.
why it matters
This definition populates the deferred bucket that feeds deferredTests_length (asserting length 2), deferredTests_nodup, deferredTests_exact (characterizing membership via empiricalPriority), and priorityBucketTotal (summing all four priority buckets to 9). It supports the module claim that every queued item is already covered by the formal empirical protocol, without supplying evidence for the underlying theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.