seven_is_cube_minus_one
The equality 7 = 2^3 - 1 supplies a basic arithmetic witness inside the Recognition Science cardinality spectrum. Cross-domain modelers would cite it when anchoring the position of 7 among the numbers generated from the cube primitives 2 and 3. The proof is a single decision procedure that evaluates the identity by direct computation.
claimIn the natural numbers, seven equals two to the power three minus one: $7 = 2^3 - 1$.
background
The module assembles explicit witnesses for the RS cardinality spectrum, the set of canonical domain cardinalities {2, 3, 4, 5, 6, 7, 8, 10, 12, 15, 16, 45, 70, ...}. Each entry is required to decompose via multiplication, addition, or exponentiation from the cube-generators {2, 3}, the configuration dimension 5, and the gap parameter 45. The local theoretical setting is to demonstrate that this spectrum is structured rather than arbitrary.
proof idea
The proof is a term-mode application of the decide tactic that reduces the equality 7 = 8 - 1 to a direct numerical check with no lemmas invoked.
why it matters in Recognition Science
It supplies the concrete relation for 7 inside the spectrum, reinforcing the eight-tick octave (period 2^3) from the forcing chain. The declaration therefore contributes to the module's claim that every listed cardinality admits an RS-primitive decomposition. No open questions are addressed.
scope and limits
- Does not derive any spectrum member from the Recognition Composition Law.
- Does not connect 7 to mass formulas, constants, or physical units.
- Does not treat cardinalities beyond the listed small-cube examples.
formal statement (Lean)
52theorem seven_is_cube_minus_one : (7 : ℕ) = 2^3 - 1 := by decide
proof body
Term-mode proof.
53
54/-- 8 = 2³. -/