highPriorityTests
plain-language theorem explainer
This definition supplies the explicit list of three high-priority empirical tests in the Option A queue: c2PlanetStrata, c5AttentionTensor, and c9RegulatoryCeiling. Researchers certifying priority orderings or aggregating test buckets would cite it when verifying coverage of cross-domain claims. The declaration is a direct constant list with no computation or lemmas.
Claim. Let $H$ be the list of high-priority tests. Then $H = [c2PlanetStrata, c5AttentionTensor, c9RegulatoryCeiling]$, where each entry belongs to the CombinationID inductive type of implemented Option A combinations.
background
The Option A Empirical Queue module organizes empirical tests attached to the C1-C9 cross-domain theorems into four priority buckets. It records which protocols to test first while proving every queued item is already covered by the formal empirical protocol. Local setting: zero sorry, zero axiom in the module.
proof idea
Direct definition that assigns the three-element list to highPriorityTests. No lemmas or tactics are invoked; it is a constant declaration.
why it matters
This supplies the concrete high-priority list consumed by EmpiricalQueueCert (which checks four priorities and specific immediate/high assignments) and by priorityBucketTotal (which sums lengths across all buckets to nine). It fills the high-priority slot after the immediate pair in the empirical queue for Option A, supporting systematic validation of cross-domain theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.