tick_surj
plain-language theorem explainer
The projection from attentional states onto their tick-phase component is surjective. Researchers modeling cross-domain attention within Recognition Science would cite this to confirm every tick phase is attained. The proof is a one-line wrapper that builds an explicit preimage by pairing the target phase with the alerting network.
Claim. The map sending each pair $(N, P)$ in AttentionNetwork × TickPhase to the phase $P$ is surjective.
background
AttentionState is the product type AttentionNetwork × TickPhase. AttentionNetwork is the inductive type whose five constructors are alerting, orienting, executive, defaultMode and salience. The module documentation states that this product yields a state space of cardinality 40, with the remaining five slots under the gap45 ceiling reserved for overflow singletons.
proof idea
The proof is a one-line wrapper around the intro tactic. It supplies the concrete preimage (alerting, x) and closes the equality by reflexivity.
why it matters
The result supplies the tick-phase half of the surjectivity data required by the AttentionSpaceCert structure. That structure aggregates the 40-state count, the overflow of 5, the relation Fintype.card TickPhase = 2^3, and the network surjectivity; together they certify the factorization 5 × 8 = 40 inside the gap45 ceiling. In the Recognition framework the theorem confirms that the eight-tick octave is realized across all five networks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.