tickCount
plain-language theorem explainer
The theorem establishes that the TickPhase inductive type with eight constructors t0 through t7 has cardinality exactly eight. Researchers modeling cross-domain attention in Recognition Science cite it to fix the second factor in the 5 by 8 state-space product. The proof is a direct decision computation on the automatically derived Fintype instance.
Claim. Let TickPhase be the inductive type with constructors $t_0, t_1, t_2, t_3, t_4, t_5, t_6, t_7$. Then the cardinality of TickPhase is eight: $|$TickPhase$| = 8$.
background
The CrossDomain.AttentionSpace module defines the attentional state space as the product AttentionNetwork × TickPhase. TickPhase is the inductive enumeration with eight constructors t0 to t7 that derives DecidableEq, Repr, BEq and Fintype. This supplies the eight-tick structure required for the 5 × 8 = 40 factorization under the gap45 ceiling.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the Fintype.card expression for the eight-constructor inductive type.
why it matters
tickCount supplies the factor of eight used by the downstream theorem attentionStateCount to obtain Fintype.card AttentionState = 40 and to confirm the five overflow slots under gap45. It realizes the eight-tick octave (T7) of the UnifiedForcingChain inside the attention model. The module predicts that attentional-blink experiments will exhibit 40 stable plateaus plus five transient singletons.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.