`attentionSpaceCert`

definition

show as: view math explainer →

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

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

formal source

  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.