fortyfive_decomp
plain-language theorem explainer
The equality establishes that 45 decomposes as the square of the spatial-dimension generator times the configuration-dimension generator. Cross-domain recognition researchers cite it when verifying that all enumerated spectrum cardinalities reduce to the primitive set {2, 3, 5}. The proof applies a decision procedure that confirms the arithmetic identity directly.
Claim. $45 = 3^{2} · 5$ where 3 denotes the spatial dimension generator and 5 the configuration dimension generator.
background
The module proves that every integer in the RS cardinality spectrum factors through the generators G = {2, 3, 5} via addition, multiplication, exponentiation and binomial coefficients. G3 is the constant 3 standing for spatial dimension; G5 is the constant 5 standing for configuration dimension. The local claim is that no spectrum member enumerated in C21 escapes such a polynomial representation in these three values.
proof idea
The proof is a one-line wrapper that invokes the decide tactic to verify the numerical equality 45 = 3² * 5.
why it matters
This decomposition feeds the certificate recognitionGeneratorsCert that aggregates all generator reductions. It directly supports the structural meta-claim that spectrum members are generated from {2, 3, 5} and aligns with the Recognition Science use of these primitives for cardinality derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.