attention_plus_overflow_eq_gap
plain-language theorem explainer
The theorem establishes that the cardinality of attentional states plus five equals the gap45 complexity ceiling. Cross-domain attention researchers in Recognition Science cite it to confirm the five overflow slots under saturation in the 5 by 8 state space. The proof is a one-line rewrite of the state count followed by a decision tactic.
Claim. $ |AttentionState| + 5 = gap45 $, where $AttentionState$ denotes the Cartesian product of the attention network space and the tick phase space.
background
The module defines the attentional state space as the product $AttentionNetwork × TickPhase$, which factors numerically as 5 by 8. The upstream theorem attentionStateCount establishes that the cardinality of this product equals 40. The module doc-comment states that the complexity ceiling gap45 leaves exactly five overflow slots, with the prediction that attentional-blink experiments should exhibit 40 stable plateaus plus five transient ones.
proof idea
One-line wrapper that rewrites the left-hand side via the theorem attentionStateCount (which sets the cardinality to 40) and then applies the decide tactic to verify equality with gap45.
why it matters
This result supplies the sum_is_gap field inside the attentionSpaceCert definition, which aggregates state count, overflow relation, and tick relations. It directly instantiates the module's structural claim that 45 minus 40 equals five overflow slots. In the Recognition framework it fills the gap45 ceiling for cross-domain attention, consistent with the eight-tick octave and the D equals 3 spatial structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.