`attentionStateCount`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.CrossDomain.AttentionSpace on GitHub at line 36.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  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
  53  intro x; exact ⟨(x, TickPhase.t0), rfl⟩
  54
  55theorem tick_surj :
  56    Function.Surjective (fun s : AttentionState => s.2) := by
  57  intro x; exact ⟨(AttentionNetwork.alerting, x), rfl⟩
  58
  59structure AttentionSpaceCert where
  60  state_count : Fintype.card AttentionState = 40
  61  overflow_D : gap45 - Fintype.card AttentionState = 5
  62  sum_is_gap : Fintype.card AttentionState + 5 = gap45
  63  tick_2cube : Fintype.card TickPhase = 2 ^ 3
  64  network_surj : Function.Surjective (fun s : AttentionState => s.1)
  65  tick_surj : Function.Surjective (fun s : AttentionState => s.2)
  66

papers checked against this theorem

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