priority_count
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not establish empirical validity of any C1-C9 theorem.
- Does not depend on numerical values of alpha, G or other constants.
- Does not constrain the ordering or selection logic among the four priorities.
- Does not address actualization or forcing beyond module imports.
Lean usage
def exampleCert : EmpiricalQueueCert := { four_priorities := priority_count, c3_now := c3_immediate, c8_now := c8_immediate, c5_next := c5_high, c2_next := c2_high }formal statement (Lean)
29theorem priority_count : Fintype.card Priority = 4 := by
proof body
Decided by rfl or decide.
30 decide
31
32/-- Empirical priority for the implemented Option A combinations. -/