twelve_decomp
plain-language theorem explainer
The decomposition establishes that twelve factors as the square of the binary generator times the spatial dimension generator. Researchers working on the Recognition Science spectrum would reference this when enumerating cardinalities from the primitive set {2,3,5}. The proof reduces immediately via the decide tactic on the concrete arithmetic equality.
Claim. $12 = 2^2 · 3$ where $2$ is the binary face generator and $3$ is the spatial dimension generator.
background
The module proves that every integer in the RS cardinality spectrum reduces to a polynomial expression in the generators G = {2, 3, 5} via addition, multiplication, exponentiation and binomial coefficients. The listed spectrum members include the explicit case 12 = 2² · 3. Local notation fixes G2 as the binary-face constant and G3 as the spatial-dimension constant.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the concrete numerical identity.
why it matters
This result instantiates the structural meta-claim that every spectrum member arises from the primitive set {2, 3, 5}. It directly matches the enumerated example in the module documentation for C27 and aligns with the forcing-chain step that fixes spatial dimensions at three.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.