c2_high
plain-language theorem explainer
The declaration shows that the C2 planet strata case receives high priority under the empirical priority function. Researchers verifying test ordering for the Option A queue in Recognition Science cross-domain theorems would cite it to confirm the assigned level. The proof is a direct reflexivity reduction on the case in the priority definition.
Claim. The empirical priority function maps the C2 planet strata combination to high priority: $empiricalPriority(C2PlanetStrata) = high$.
background
The module sets up a priority queue for empirical tests attached to the C1-C9 cross-domain theorems. The function empiricalPriority : CombinationID → Priority assigns levels explicitly, with the case for C2 planet strata returning high. The module records which protocols to test first and proves formal coverage by the empirical protocol, with zero sorry or axiom.
proof idea
The proof is a one-line wrapper that applies reflexivity to the empiricalPriority definition, which directly specifies high for this combination.
why it matters
This supplies the c2_next field inside the empiricalQueueCert definition that certifies the full queue structure. It fills a slot in the foundation layer for Option A empirical validation, ensuring every queued item is formally covered by the protocol. The result touches the C2 combination in the empirical pipeline without addressing the underlying physical claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.