`workingMemoryFromCubeCert`

definition

show as: view math explainer →

module: IndisputableMonolith.CrossDomain.WorkingMemoryFromCube
domain: CrossDomain
line: 61 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.CrossDomain.WorkingMemoryFromCube on GitHub at line 61.

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

  58  miller_bracket : 5 ≤ canonicalSpan ∧ canonicalSpan ≤ 9
  59  monotone : ∀ d, spanAt d < spanAt (d + 1)
  60
  61def workingMemoryFromCubeCert : WorkingMemoryFromCubeCert where
  62  canonical := canonicalSpan_eq
  63  reduced_to_5 := span_at_2
  64  reduced_to_3 := span_at_1
  65  super_normal := span_at_4
  66  miller_bracket := miller_bracket
  67  monotone := span_strict_mono
  68
  69end IndisputableMonolith.CrossDomain.WorkingMemoryFromCube

papers checked against this theorem

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