`AttentionNetwork`

definition

show as: view math explainer →

module: IndisputableMonolith.CrossDomain.AttentionSpace
domain: CrossDomain
line: 22 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.CrossDomain.AttentionSpace on GitHub at line 22.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

used by

formal source

  19
  20namespace IndisputableMonolith.CrossDomain.AttentionSpace
  21
  22inductive AttentionNetwork where
  23  | alerting | orienting | executive | defaultMode | salience
  24  deriving DecidableEq, Repr, BEq, Fintype
  25
  26inductive TickPhase where
  27  | t0 | t1 | t2 | t3 | t4 | t5 | t6 | t7
  28  deriving DecidableEq, Repr, BEq, Fintype
  29
  30theorem networkCount : Fintype.card AttentionNetwork = 5 := by decide
  31theorem tickCount : Fintype.card TickPhase = 8 := by decide
  32theorem tick_eq_twoPowD : Fintype.card TickPhase = 2 ^ 3 := by decide
  33
  34abbrev AttentionState : Type := AttentionNetwork × TickPhase
  35
  36theorem attentionStateCount : Fintype.card AttentionState = 40 := by
  37  simp only [AttentionState, Fintype.card_prod, networkCount, tickCount]
  38
  39/-- The complexity ceiling gap45 leaves exactly 5 overflow slots. -/
  40def gap45 : ℕ := 45
  41theorem overflow_eq_D : gap45 - Fintype.card AttentionState = 5 := by
  42  rw [attentionStateCount]; decide
  43
  44theorem attention_fits_under_gap : Fintype.card AttentionState < gap45 := by
  45  rw [attentionStateCount]; decide
  46
  47theorem attention_plus_overflow_eq_gap :
  48    Fintype.card AttentionState + 5 = gap45 := by
  49  rw [attentionStateCount]; decide
  50
  51theorem network_surj :
  52    Function.Surjective (fun s : AttentionState => s.1) := by

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.