immediateTests
plain-language theorem explainer
immediateTests enumerates the two highest-priority empirical tests in the Option A queue as the oncology tensor and Miller span combinations. Researchers validating the C1-C9 cross-domain theorems would cite this list when ordering experimental protocols. The definition is a direct literal construction of the list of CombinationID values.
Claim. The list of immediate empirical tests is $[c_3, c_8]$ where $c_3$ denotes the oncology tensor combination and $c_8$ the Miller span combination, both drawn from the inductive type of implemented Option A combinations.
background
The Option A Empirical Queue module records a priority ordering for empirical tests attached to the C1-C9 cross-domain theorems. It ensures every queued item is already covered by the formal empirical protocol and maintains zero sorry or axiom in Lean. CombinationID is the inductive type that enumerates the implemented Option A combinations (c1 through c9, with c10 left as commentary). The upstream tests definition supplies a supremum over local tests that, in the gravitational setting, represents local curvature bounds derived from eight-tick geometry.
proof idea
This is a direct definition that returns the literal list [.c3OncologyTensor, .c8MillerSpan]. No lemmas or tactics are invoked; the construction is a one-line enumeration of the two immediate CombinationID constructors.
why it matters
The definition supplies the concrete contents of the immediate bucket that is referenced by EmpiricalQueueCert and by the supporting theorems immediateTests_exact, immediateTests_length, immediateTests_nodup, and priorityBucketTotal. It therefore fixes the first rung of the empirical priority ladder for the C1-C9 theorems. The surrounding queue structure aligns with the eight-tick octave and the requirement that every test be formally protocol-covered.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.