seven_decomp
plain-language theorem explainer
The natural number 7 equals the cube of the binary-face generator minus one. Cross-domain Recognition Science work on spectrum cardinality would cite this to confirm 7 reduces to the primitive set {2,3,5}. The proof is a one-line decision procedure that verifies the arithmetic identity by direct computation.
Claim. $7 = 2^3 - 1$, where 2 is the binary-face generator.
background
The module proves that every integer in the RS cardinality spectrum reduces to polynomials in the generators G = {2, 3, 5} via addition, multiplication, exponentiation and binomial coefficients. G2 is the binary-face generator, fixed at the constant 2. The local claim is that no spectrum member lies outside this generated set; the listed decompositions cover the members enumerated in C21.
proof idea
One-line wrapper that applies the decide tactic to the equality, reducing it to a decidable arithmetic proposition and confirming it by computation.
why it matters
This supplies the explicit decomposition 7 = 2^3 - 1 inside the Recognition Generators module, supporting the structural meta-claim that the entire spectrum arises from operations on {2,3,5}. It aligns with the eight-tick octave (T7) through the power of the binary generator. No downstream theorems yet reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.