AttentionState
plain-language theorem explainer
AttentionState is the Cartesian product of the five-element AttentionNetwork type and the eight-element TickPhase type. Researchers modeling cross-domain attention in Recognition Science cite this abbreviation to fix the 40-state space that sits under the gap45 ceiling. The declaration is a direct type abbreviation whose finite cardinality follows immediately from the product rule.
Claim. Let $N$ be the inductive type whose constructors are alerting, orienting, executive, defaultMode, salience. Let $P$ be the inductive type whose constructors are $t_0, t_1, t_2, t_3, t_4, t_5, t_6, t_7$. The attentional state space is the product type $N × P$.
background
The module states that attentional state space factors as AttentionNetwork × TickPhase = 5 × 8 = 40, leaving exactly five overflow slots under the complexity ceiling gap45. AttentionNetwork is the inductive type with five constructors that enumerate the alerting, orienting, executive, defaultMode, and salience networks. TickPhase is the inductive type with eight constructors t0 through t7; an identical TickPhase appears upstream in TwoCubeUniversality, confirming the eight-tick octave structure.
proof idea
The declaration is a one-line type abbreviation that directly equates AttentionState to the product AttentionNetwork × TickPhase. No lemmas or tactics are invoked; the equality is definitional and immediately supplies the inputs to Fintype.card_prod used in downstream cardinality theorems.
why it matters
This definition supplies the 40-element state space whose cardinality is proved equal to 40 in attentionStateCount and shown to fit under gap45 with five overflow slots in overflow_eq_D and attention_plus_overflow_eq_gap. It realizes the module's structural claim 5 × 8 = 40 and feeds the AttentionSpaceCert structure that records the overflow and the surjectivity of the network projection. The eight phases align with the eight-tick octave (T7) of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.