seven_decomp
plain-language theorem explainer
The equality shows that 7 equals 2 cubed minus 1 using the binary face generator. Cross-domain researchers cite it to confirm that 7 belongs to the Recognition Science spectrum generated from {2,3,5}. The proof is a direct decision procedure on the natural-number equality.
Claim. $7 = 2^3 - 1$, where 2 is the binary face generator.
background
The RecognitionGenerators module states that every integer in the RS cardinality spectrum reduces to a polynomial in the generators G = {2,3,5} via addition, multiplication, exponentiation, and binomial choose. G2 is the binary face generator fixed at value 2. The module enumerates explicit decompositions for spectrum members listed in C21, with 7 given as 2^3 - 1.
proof idea
The proof is a one-line wrapper that invokes the decide tactic to compute the natural-number equality directly.
why it matters
This declaration supplies the explicit decomposition for 7 inside the C27 structural meta-claim that no spectrum member lies outside polynomials in {2,3,5}. It completes one entry in the enumerated list that supports the overall generator thesis for the RS cardinality spectrum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.