module module moderate

`IndisputableMonolith.CrossDomain.WorkingMemoryFromCube`

Module formalizes the canonical span of 7 as 2 cubed minus 1 inside the cross-domain working memory construction from the cube. Researchers applying the eight-tick octave to memory models would cite these span definitions. The module supplies a collection of span functions, monotonicity lemmas, and a certificate without deeper derivations.

claimThe canonical span satisfies $7 = 2^3 - 1$.

background

The module sits in the cross-domain layer and ties the eight-tick octave (period 2^3) to working-memory structures. It introduces spanAt at successive levels, strict monotonicity of the span map, the super-normal jump, the miller bracket, and the WorkingMemoryFromCubeCert. The local setting follows the forcing-chain step that fixes the octave length at eight ticks.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

Supplies the span foundation that feeds WorkingMemoryFromCubeCert and the cross-domain use of T7. It closes the geometric side of the eight-tick construction before further composition-law applications.

scope and limits

Does not derive the span value from the Recognition Composition Law.
Does not link the span to the phi-ladder or mass formula.
Does not address the alpha inverse interval.
Does not extend the construction past the cube geometry.

declarations in this module (13)

def canonicalSpan L25
theorem canonicalSpan_eq L26
def spanAt L29
theorem span_at_3 L31
theorem span_at_2 L32
theorem span_at_1 L33
theorem span_at_0 L34
theorem span_at_4 L35
theorem span_strict_mono L38
theorem super_normal_jump L47
theorem miller_bracket L50
structure WorkingMemoryFromCubeCert L53
def workingMemoryFromCubeCert L61