attentionStateCount
The theorem states that the number of distinct attentional states is exactly 40. Cross-domain modelers and experimentalists testing wave-62 predictions cite this cardinality when bounding the size of the attention space relative to the complexity ceiling. The proof is a direct simplification that unfolds the product type and substitutes the known cardinalities of its factors.
claimLet AttentionState denote the Cartesian product of the set of attention networks and the set of tick phases. Then the cardinality of AttentionState equals 40.
background
The module defines AttentionState as the product type AttentionNetwork × TickPhase. Upstream theorems establish that the cardinality of AttentionNetwork is 5 and the cardinality of TickPhase is 8. These facts appear directly in the local setting for wave 62, where the structural claim is that the attentional state space factors as 5 × 8 = 40 and the complexity ceiling gap45 leaves exactly 5 overflow slots.
proof idea
The proof is a one-line term-mode wrapper that applies simp to unfold AttentionState, invoke the product cardinality rule Fintype.card_prod, and substitute the two upstream cardinality theorems networkCount and tickCount.
why it matters in Recognition Science
This result supplies the state count used by attention_fits_under_gap, attention_plus_overflow_eq_gap, overflow_eq_D, and the attentionSpaceCert certificate. It fills the 5 × 8 = 40 step in the C5 attention space claim of the module, consistent with the eight-tick octave structure from the forcing chain.
scope and limits
- Does not establish the internal structure of AttentionNetwork or TickPhase.
- Does not address temporal dynamics or transitions between states.
- Does not connect to the spatial dimension D = 3 from the forcing chain.
- Does not prove uniqueness of the 40-state count under alternative factorizations.
Lean usage
rw [attentionStateCount]formal statement (Lean)
36theorem attentionStateCount : Fintype.card AttentionState = 40 := by
proof body
Term-mode proof.
37 simp only [AttentionState, Fintype.card_prod, networkCount, tickCount]
38
39/-- The complexity ceiling gap45 leaves exactly 5 overflow slots. -/