AttentionNetwork
plain-language theorem explainer
AttentionNetwork enumerates the five attention networks that factor the attentional state space in the Recognition Science cross-domain model. Researchers modeling attentional dynamics or the predicted 40-state plateaus would cite this enumeration to anchor the product structure with TickPhase. The declaration is a direct inductive definition with five named constructors and automatic derivation of decidable equality plus finite type structure.
Claim. Let $A$ be the inductive type whose elements are the five attention networks: alerting, orienting, executive, default mode, and salience, equipped with decidable equality, representation, Boolean equality, and finite cardinality.
background
The module establishes the structural claim that the attentional state space factors as AttentionNetwork × TickPhase = 5 × 8 = 40, with the complexity ceiling gap45 = 45 leaving exactly five overflow slots. These slots correspond to the five attention-network singletons under saturation. The local setting predicts that attentional-blink experiments should exhibit 40 stable plateaus plus 5 transient ones. The module imports only Mathlib and introduces the product abbrev AttentionState together with cardinality and surjectivity results.
proof idea
The declaration is an inductive definition that introduces five constructors and derives DecidableEq, Repr, BEq, and Fintype in a single line.
why it matters
This definition supplies the five-element factor required for the 40-state attention space and directly enables the downstream results networkCount (Fintype.card = 5), tick_surj (surjectivity onto TickPhase), and the abbrev AttentionState. It fills the C5 structural claim in the module documentation, linking to the eight-tick octave from the forcing chain and the gap45 overflow structure. The five networks account for the predicted transient states under the 45 ceiling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.