fortyfive_decomp
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 in Recognition Science
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.
scope and limits
- Does not prove uniqueness of the factorization among possible expressions.
- Does not extend the decomposition to integers outside the enumerated spectrum.
- Does not link the result to physical constants or forcing-chain steps T0-T8.
formal statement (Lean)
56theorem fortyfive_decomp : (45 : ℕ) = G3^2 * G5 := by decide