mediumPriorityTests
plain-language theorem explainer
Medium-priority empirical tests are the cognitive tensor combination and the universal response combination. Researchers validating the C1-C9 cross-domain theorems cite this list to establish testing priorities. The definition introduces these two items explicitly as a constant list.
Claim. The list of medium-priority empirical tests is $[C_1, C_7]$, where $C_1$ denotes the cognitive tensor combination and $C_7$ the universal response combination among the implemented Option A combinations.
background
The Option A Empirical Queue module defines a priority structure for empirical tests associated with the C1-C9 cross-domain theorems. It records the order in which protocols should be tested and certifies that each queued item is covered by the formal empirical protocol, without supplying supporting evidence for the underlying claims. CombinationID is the inductive enumeration of implemented Option A combinations. The upstream result from ILG.CPMInstance defines a tests functional as the supremum over local tests, which in the gravitational setting corresponds to local curvature bounds.
proof idea
The definition is supplied directly as the explicit list of the two specified CombinationID values. No additional lemmas or proof steps are required beyond the literal construction of the list.
why it matters
This definition fills the medium priority slot in the empirical test queue. It is referenced in the EmpiricalQueueCert structure that certifies the four priority levels and in theorems confirming membership conditions, the list length, lack of duplicates, and the sum of all priority buckets equaling nine. It supports the systematic organization of empirical checks for the cross-domain theorems within the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.