networkCount
plain-language theorem explainer
The theorem establishes that the attention network type contains exactly five elements, one for each enumerated mode. Researchers modeling cross-domain attention in Recognition Science cite this cardinality when computing the product with the eight-phase tick cycle to reach 40 states. The proof is a direct decision on the Fintype instance automatically derived from the inductive definition.
Claim. The finite set of attention networks has cardinality five: $|$AttentionNetwork$| = 5$.
background
AttentionNetwork is the inductive type whose five constructors are alerting, orienting, executive, defaultMode, and salience; the deriving clause supplies DecidableEq, Repr, BEq, and Fintype. The module states that attentional state space factors as AttentionNetwork × TickPhase = 5 × 8 = 40, with the complexity ceiling gap45 leaving exactly five overflow slots. This local setting sits inside the larger Recognition Science derivation of discrete structure from the forcing chain, where the eight-tick octave supplies the TickPhase factor.
proof idea
The proof is a one-line wrapper that applies the decide tactic to evaluate Fintype.card directly on the Fintype instance generated by the inductive definition of AttentionNetwork.
why it matters
networkCount supplies the network factor to the downstream attentionStateCount theorem, which concludes Fintype.card AttentionState = 40. It realizes the 5 × 8 factorization asserted in the C5 attention-space claim and aligns with the eight-tick octave (T7) from the unified forcing chain. The five enumerated modes account for the overflow slots under the gap45 ceiling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.