twoSixteen_decomp
The equality shows 216 equals the cube of the product of the binary-face generator and the spatial-dimension generator. Researchers enumerating RS spectrum cardinalities would cite this to confirm 216 reduces to a polynomial in {2, 3, 5}. The proof is a direct decision on the arithmetic identity after generator substitution.
claim$216 = (2 · 3)^3$, where 2 is the binary-face generator and 3 is the spatial-dimension generator.
background
Module C27 states that every integer in the RS cardinality spectrum is generated by primitive operations on G = {2, 3, 5}, with 2 as binary face, 3 as spatial dim, and 5 as configDim. Operations include addition, multiplication, exponentiation, and choose. The module documentation explicitly lists 216 = 6³ = (2·3)³ as one such reduction, part of the claim that the spectrum members enumerated in C21 all admit such decompositions. Upstream results supply the constant definitions for the binary-face generator (equal to 2) and spatial-dimension generator (equal to 3).
proof idea
The proof is a one-line wrapper that applies the decide tactic to verify the numerical equality after substituting the generator definitions.
why it matters in Recognition Science
This declaration supplies one concrete decomposition in the enumeration supporting the structural meta-claim of C27 that no RS spectrum member escapes generation as a polynomial in {2, 3, 5}. It aligns with framework landmarks T8 (D = 3 spatial dimensions) via the spatial-dimension generator. No downstream uses are recorded, and no open questions are closed here.
scope and limits
- Does not prove the general theorem that all spectrum members decompose via these generators.
- Does not link the decomposition to physical constants, mass formulas, or forcing chain steps.
- Does not invoke the Recognition Composition Law or any J-cost identities.
- Does not address wave-64 cross-domain interpretations beyond the integer equality.
formal statement (Lean)
59theorem twoSixteen_decomp : (216 : ℕ) = (G2 * G3)^3 := by decide