eight_decomp
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.