`network_surj`

proved

show as: view math explainer →

module: IndisputableMonolith.CrossDomain.AttentionSpace
domain: CrossDomain
line: 51 · 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 51.

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

depends on

used by

formal source

  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
  67def attentionSpaceCert : AttentionSpaceCert where
  68  state_count := attentionStateCount
  69  overflow_D := overflow_eq_D
  70  sum_is_gap := attention_plus_overflow_eq_gap
  71  tick_2cube := tick_eq_twoPowD
  72  network_surj := network_surj
  73  tick_surj := tick_surj
  74
  75end IndisputableMonolith.CrossDomain.AttentionSpace

papers checked against this theorem

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