fifteen_decomp
The equality establishes that 15 factors directly as the product of the spatial dimension generator and the configuration dimension generator within the Recognition Science cardinality spectrum. Workers verifying the enumerated spectrum members against the primitive set G = {2, 3, 5} would cite this decomposition when checking closure under multiplication. The proof is a one-line wrapper that applies the decide tactic to the concrete numerical equality.
claim$15 = 3 × 5$, where 3 is the spatial dimension generator and 5 is the configuration dimension generator.
background
The RecognitionGenerators module states a structural meta-claim: every integer in the RS cardinality spectrum reduces to the primitive generators G = {2, 3, 5} via addition, multiplication, exponentiation or binomial coefficients. The generators are introduced as G3 := 3 (spatial dim) and G5 := 5 (configDim). The module enumerates concrete decompositions for spectrum members listed in C21, including 15 = 3 · 5, and asserts that no spectrum member lies outside such polynomials in {2, 3, 5}.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the equality (15 : ℕ) = G3 * G5 after the definitions of G3 and G5 have been unfolded.
why it matters in Recognition Science
This declaration supplies one of the enumerated factorizations required by the module-level claim that the entire RS spectrum is generated from {2, 3, 5}. It directly supports the cross-domain structural meta-claim for Wave 64 and aligns with the framework landmark that spatial dimension D = 3 appears as a primitive generator. No downstream theorems yet depend on it.
scope and limits
- Does not prove the full spectrum decomposition claim for all enumerated members.
- Does not assign physical units or interpret the generators beyond their integer definitions.
- Does not address whether the generators arise from the forcing chain T0-T8.
formal statement (Lean)
53theorem fifteen_decomp : (15 : ℕ) = G3 * G5 := by decide