six_decomp
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.