twelve_decomp
plain-language theorem explainer
The natural number 12 equals the square of the binary-face generator times the spatial-dimension generator. Researchers verifying the C27 meta-claim on spectrum decompositions would cite this when checking that every enumerated member reduces to a polynomial in {2, 3, 5}. The proof is a one-line decision procedure that confirms the arithmetic identity directly.
Claim. $12 = 2^2 · 3$, where 2 denotes the binary-face generator and 3 the spatial-dimension generator.
background
The module establishes that every integer in the RS cardinality spectrum reduces to a polynomial expression in the generators G = {2, 3, 5}, corresponding to binary face, spatial dimension, and configuration dimension. The referenced definitions fix G2 as the constant 2 (binary face) and G3 as the constant 3 (spatial dim). The local setting is the structural meta-claim that no spectrum member lies outside such polynomials, with explicit examples including 12 = 2² · 3.
proof idea
One-line wrapper that applies the decide tactic to the arithmetic equality.
why it matters
This declaration supplies one concrete decomposition required by the C27 meta-claim that spectrum members enumerated in C21 all reduce to polynomials in {2, 3, 5}. It directly supports the framework landmark T8 that fixes D = 3 spatial dimensions via the generator G3. No downstream theorems are recorded, so the result functions as a leaf verification inside the generator module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.