threeSixty_decomp
plain-language theorem explainer
360 factors as the cube of the binary-face generator times the square of the spatial-dimension generator times the configuration-dimension generator. Researchers enumerating the Recognition Science cardinality spectrum cite this decomposition. The proof is a one-line computational check that unfolds the generator definitions and verifies the arithmetic equality.
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 that every integer in the RS cardinality spectrum reduces to a polynomial in the generators G = {2, 3, 5}, which stand for binary face, spatial dimension, and configuration dimension. The module document states that the claim is there is no member of the RS spectrum that cannot be written as such a polynomial in {2, 3, 5}, with explicit examples including 360 = 2³ · 3² · 5. The three generator definitions supply the constants 2, 3, and 5 used in the equality.
proof idea
One-line wrapper that applies the decide tactic to the numerical equality after the definitions of the three generators are substituted.
why it matters
This decomposition supports the structural meta-claim that the RS spectrum is generated from the set {2, 3, 5}. It is referenced by the certificate that records the generators and related properties. It fills the enumerated case for 360 among the spectrum decompositions listed in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.