priority_count
plain-language theorem explainer
The theorem establishes that the Priority inductive type for the Option A empirical queue contains exactly four elements. Researchers formalizing the C1-C9 cross-domain theorems cite this cardinality when constructing the queue certification. The proof is a one-line decision procedure that computes the result from the derived Fintype instance on the four-constructor inductive definition.
Claim. The finite type of empirical priorities, with constructors immediate, high, medium and defer, satisfies $Fintype.card(Priority) = 4$.
background
The module defines a priority queue for empirical tests attached to the C1-C9 cross-domain theorems. It records which protocols should be tested first and proves every queued item is covered by the formal empirical protocol, with Lean status 0 sorry and 0 axiom. The referenced Priority type is the inductive definition with exactly those four constructors, deriving DecidableEq, Repr and Fintype. Upstream results supply the active-edge count A from IntegrationGap (the phi-power balance identity at D=3) together with the actualization operator A from Modal.Actualization and the coherence unit A from Masses.Anchor.
proof idea
The proof is a one-line wrapper that applies the decide tactic. The tactic succeeds directly because the inductive definition of Priority derives Fintype, so the cardinality is computed automatically as four from the explicit constructors.
why it matters
This theorem supplies the four_priorities field inside the empiricalQueueCert definition that certifies the Option A queue structure. It closes a basic counting step required by the empirical protocol in the Recognition Science framework, ensuring the queue respects the eight-tick octave and phi-ladder from the T0-T8 forcing chain. No open scaffolding remains at this leaf.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.