oneTwentyFive_decomp
The decomposition establishes that 125 equals the cube of the configuration dimension generator. Cross-domain recognition researchers cite it when confirming that enumerated spectrum cardinalities reduce to operations on the set {2, 3, 5}. The proof proceeds by a single decision procedure that evaluates the numerical identity directly.
claim$125 = 5^3$ where 5 is the configuration dimension generator.
background
The RecognitionGenerators module proves decompositions of RS spectrum members into polynomials over the generators G = {2, 3, 5}, which stand for binary face, spatial dimension, and configuration dimension. The local setting is the structural meta-claim of C27 that every integer in the spectrum arises from addition, multiplication, exponentiation, or choose applied to these three values. The upstream definition supplies G5 as the constant 5.
proof idea
The proof is a one-line wrapper that invokes the decide tactic to verify the equality 125 = 5^3 by direct numerical computation.
why it matters in Recognition Science
This decomposition contributes to the certificate recognitionGeneratorsCert that validates the full set of generators and their operations. It fills the explicit case 125 = 5^3 in the C27 enumeration of spectrum reductions. The result supports the claim that the RS cardinality spectrum is closed under the primitive operations on {2, 3, 5}.
scope and limits
- Does not establish uniqueness of the decomposition among possible expressions in the generators.
- Does not extend the reduction to integers outside the enumerated RS spectrum.
- Does not connect the cardinality result to dynamical or physical interpretations.
formal statement (Lean)
58theorem oneTwentyFive_decomp : (125 : ℕ) = G5^3 := by decide