  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
  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

papers checked against this theorem

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