attention_fits_under_gap
plain-language theorem explainer
The theorem establishes that the cardinality of attentional states, formed as the Cartesian product of attention-network configurations and tick phases, is strictly less than the gap45 complexity ceiling. Researchers modeling cross-domain saturation in Recognition Science would cite this bound when separating stable plateaus from overflow slots. The proof is a one-line wrapper that substitutes the explicit count of 40 and decides the numerical inequality.
Claim. Let AttentionState denote the Cartesian product of AttentionNetwork configurations and TickPhase elements. Then the cardinality satisfies $|$AttentionState$| < 45$, where 45 is the complexity ceiling gap45.
background
The module defines the attentional state space as the product AttentionNetwork × TickPhase, which factors as 5 × 8 = 40. The complexity ceiling gap45 is set to 45, leaving exactly five overflow slots. Upstream, the lemma attentionStateCount establishes that Fintype.card AttentionState = 40 by simplifying the product cardinality with the network and tick counts.
proof idea
The proof is a one-line wrapper that rewrites the left-hand side via the attentionStateCount lemma and then applies the decide tactic to verify the strict inequality against gap45.
why it matters
This result closes the structural bound in the C5 Attention Space claim by confirming that the 40 states lie strictly below the 45 ceiling, thereby isolating the five overflow slots predicted for attention-network singletons. It aligns with the eight-tick octave structure (TickPhase factor of 8) in the Recognition framework and precedes any dynamical analysis of transitions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.