networkCount
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not assign dynamical roles or transition rules to the five modes.
- Does not map the modes onto specific neural or experimental observables.
- Does not address interactions or superpositions among the networks.
Lean usage
theorem attentionStateCount : Fintype.card AttentionState = 40 := by simp only [AttentionState, Fintype.card_prod, networkCount, tickCount]formal statement (Lean)
30theorem networkCount : Fintype.card AttentionNetwork = 5 := by decide