threeSixty_decomp
The declaration establishes that 360 factors as 2 cubed times 3 squared times 5 using the primitive generators 2, 3, and 5. Cross-domain researchers working on Recognition Science spectrum decompositions cite it when confirming that 360 belongs to the set generated from G = {2, 3, 5}. The proof is a direct computational verification via the decide tactic after substituting the generator constants.
claim$360 = 2^3 · 3^2 · 5$, where 2 is the binary-face generator, 3 the spatial-dimension generator, and 5 the configuration-dimension generator.
background
The module proves structural decompositions for integers in the RS cardinality spectrum using the generators G = {2, 3, 5} under multiplication and exponentiation. The module documentation states that every spectrum member reduces to a polynomial in these generators, with explicit examples including 360 = 2³ · 3² · 5. The generators are defined locally as G2 := 2 (binary face), G3 := 3 (spatial dim), and G5 := 5 (configDim).
proof idea
The proof is a one-line wrapper that applies the decide tactic to confirm the numerical equality after unfolding the generator definitions.
why it matters in Recognition Science
This decomposition feeds directly into recognitionGeneratorsCert, which assembles the full certificate for the generators. It fills the C27 meta-claim that every RS spectrum integer is generated from {2, 3, 5}, supporting the enumerated decompositions listed for C21. The result aligns with the framework's use of these generators for cross-domain cardinality claims without introducing new hypotheses.
scope and limits
- Does not prove uniqueness of the factorization.
- Does not extend the decomposition method to integers outside the enumerated spectrum.
- Does not address physical interpretations or applications of the generators.
formal statement (Lean)
61theorem threeSixty_decomp : (360 : ℕ) = G2^3 * G3^2 * G5 := by decide