AttentionSpaceCert in module IndisputableMonolith.CrossDomain.AttentionSpace.
(1) In plain English: AttentionSpaceCert is a structure that bundles six proved facts into one certificate object. It asserts the attention state space (product of 5 networks and 8 phases) has cardinality 40, that gap45 minus 40 equals 5, that 40 plus 5 equals gap45, that the 8 phases equal 2^3, and that the two projections from states onto networks and onto phases are surjective.
(2) In Recognition Science this matters because the module states the structural claim that attentional state space factors as 5 × 8 = 40 with gap45 leaving exactly 5 overflow slots (the five attention-network singletons under saturation). The module notes the prediction that attentional-blink experiments should show 40 stable plateaus plus 5 transient ones.
(3) How to read the formal statement: The structure is
structure AttentionSpaceCert where
state_count : Fintype.card AttentionState = 40
overflow_D : gap45 - Fintype.card AttentionState = 5
sum_is_gap : Fintype.card AttentionState + 5 = gap45
tick_2cube : Fintype.card TickPhase = 2 ^ 3
network_surj : Function.Surjective (fun s : AttentionState => s.1)
tick_surj : Function.Surjective (fun s : AttentionState => s.2)
Each field is an equality or surjectivity proposition. The term attentionSpaceCert supplies concrete proofs for all fields.
(4) Visible dependencies in the supplied source: The structure depends on the inductive definitions of AttentionNetwork (5 constructors) and TickPhase (8 constructors), the cardinality theorems networkCount, tickCount, tick_eq_twoPowD, the product cardinality attentionStateCount, the gap theorems overflow_eq_D, attention_plus_overflow_eq_gap, attention_fits_under_gap, and the surjectivity theorems network_surj, tick_surj. The concrete certificate is attentionSpaceCert.
(5) What this declaration does not prove: It does not prove any empirical outcome or experimental result. It does not derive physical constants, link to the forcing chain, or establish that the 5 networks model actual neural mechanisms. The attentional-blink prediction appears only in the module docstring and is not a theorem.