eight_decomp
plain-language theorem explainer
Eight equals the cube of the binary-face generator two. Cross-domain recognition work cites this decomposition when confirming that spectrum cardinalities reduce to the primitive generators two, three and five. The proof applies a decision procedure to the arithmetic identity.
Claim. $8 = 2^3$, where $2$ is the binary-face generator.
background
The module proves decompositions showing every integer in the RS cardinality spectrum reduces to the generators {2, 3, 5} via addition, multiplication, exponentiation and choose. G2 is defined as the binary-face generator equal to 2. The local theoretical setting is the structural meta-claim that no spectrum member lies outside such polynomials in these generators, with examples including 8 = 2^3.
proof idea
One-line wrapper that applies the decide tactic to the arithmetic identity.
why it matters
This fills the enumerated slot for eight among the spectrum decompositions listed in the module doc-comment for C21. It supports the overall meta-claim that the RS cardinality spectrum is generated from {2, 3, 5}. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.