theorem
proved
miller_bracket
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.CrossDomain.WorkingMemoryFromCube on GitHub at line 50.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
47theorem super_normal_jump : spanAt 4 - spanAt 3 = 2 ^ 3 := by decide
48
49/-- The Miller 7 ± 2 corridor (5 to 9) brackets canonicalSpan. -/
50theorem miller_bracket : 5 ≤ canonicalSpan ∧ canonicalSpan ≤ 9 := by
51 unfold canonicalSpan; decide
52
53structure WorkingMemoryFromCubeCert where
54 canonical : canonicalSpan = 2 ^ 3 - 1
55 reduced_to_5 : spanAt 2 = 3 -- collapse one dimension
56 reduced_to_3 : spanAt 1 = 1 -- collapse two
57 super_normal : spanAt 4 = 15 -- add one dimension
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