twelve_decomp
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 in Recognition Science
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.
scope and limits
- Does not prove uniqueness of the decomposition.
- Does not extend to integers outside the enumerated RS spectrum.
- Does not invoke the Recognition Composition Law or J-cost functions.
- Does not incorporate binomial-coefficient operations used for other spectrum members.
formal statement (Lean)
52theorem twelve_decomp : (12 : ℕ) = G2^2 * G3 := by decide