span_strict_mono
plain-language theorem explainer
The function assigning to each natural number d the value 2^d minus one is strictly monotonic. Cognitive scientists modeling Miller's law via finite-field cardinalities would invoke this result to confirm the ordering of reduced and super-normal spans. The short tactic proof unfolds the definition and dispatches the resulting arithmetic inequality with the omega solver.
Claim. For every natural number $d$, $2^d - 1 < 2^{d+1} - 1$.
background
In the module on working memory derived from the three-dimensional cube over the field with two elements, the span at dimension d is defined by spanAt d := 2^d - 1. This counts the non-identity elements of the d-dimensional vector space over F_2. The module establishes that Miller's 7 ± 2 arises as 2^3 - 1, with reductions to lower dimensions yielding 3 and 1, and super-normal extension to 15.
proof idea
The proof unfolds the definition of spanAt to obtain the inequality 2^d - 1 < 2^{d+1} - 1. It introduces the facts that 2^d is at least 1 and that 2^{d+1} equals twice 2^d, then applies the omega tactic to conclude the comparison.
why it matters
This result supports the workingMemoryFromCubeCert by confirming the monotonicity of the span ladder. It fills in the structural claim that spans increase with cube dimension, underpinning the predictions of span collapse under reduced bandwidth. Within the Recognition framework it aligns with the eight-tick octave structure by showing how powers of two generate the discrete memory plateaus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.