six_decomp
The equality 6 = 2 × 3 holds where 2 and 3 are the binary-face and spatial-dimension generators of the Recognition Science spectrum. Cross-domain researchers cite this when confirming that spectrum cardinalities factor through the primitive set {2, 3, 5}. The proof is a one-line decision procedure that confirms the arithmetic identity from the generator definitions.
claim$6 = 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 in the generators G = {2, 3, 5} via addition, multiplication, exponentiation, and binomial coefficients. Explicit examples include 6 = 2 · 3, 4 = 2², 8 = 2³, 10 = 2 · 5, and 12 = 2² · 3. The binary-face generator is defined as 2 and the spatial-dimension generator as 3.
proof idea
The proof is a one-line wrapper that applies the decide tactic to verify the equality directly from the generator definitions.
why it matters in Recognition Science
This supplies a base case for the recognitionGeneratorsCert that certifies all spectrum members reduce to operations on {2, 3, 5}. It fills the C27 structural meta-claim for the integer 6 and supports the forcing chain step where spatial dimension D = 3 appears as a generator.
scope and limits
- Does not prove uniqueness of the factorization.
- Does not extend the decomposition beyond the enumerated spectrum members.
- Does not invoke exponentiation or binomial operations for this case.
formal statement (Lean)
48theorem six_decomp : (6 : ℕ) = G2 * G3 := by decide