eight_decomp
eight_decomp establishes that eight equals the cube of the binary-face generator two. Researchers decomposing RS spectrum cardinalities from the set {2, 3, 5} cite it as a base case in the Recognition Generators module. The proof is a one-line computational check that verifies the equality directly.
claim$8 = 2^3$, where 2 is the binary-face generator.
background
The 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 defined as the constant 2, labeled the binary face. The local setting is the structural meta-claim that no spectrum member lies outside such expressions, with explicit examples including 8 = 2^3.
proof idea
The proof is a one-line wrapper that applies the decide tactic to confirm the numerical equality by direct computation.
why it matters in Recognition Science
This fills one enumerated decomposition in the C27 meta-claim that spectrum members reduce to operations on {2, 3, 5}. It aligns with the eight-tick octave (period 2^3) from the forcing chain T7. No downstream theorems are recorded.
scope and limits
- Does not prove uniqueness of the decomposition.
- Does not extend the claim to generators outside {2, 3, 5}.
- Does not supply physical or dimensional interpretations.
formal statement (Lean)
50theorem eight_decomp : (8 : ℕ) = G2^3 := by decide