threeOneTwentyFive_decomp
plain-language theorem explainer
The declaration establishes that 3125 equals five to the fifth power, with five identified as the configDim generator. Spectrum decomposition work in Recognition Science cites this to confirm that members like 3125 arise from the primitive set {2, 3, 5}. The proof is a one-line decision procedure that directly verifies the equality in natural numbers.
Claim. $3125 = 5^5$, where 5 is the configuration dimension generator.
background
The module states that every integer in the RS cardinality spectrum is generated by a small set of primitive operations on three integer generators G = {2, 3, 5}, corresponding to binary face, spatial dimension, and configDim. Operations include addition, multiplication, exponentiation, and choose. The local theoretical setting is the structural meta-claim that no spectrum member lies outside polynomials in these generators, with explicit examples such as 125 = 5^3 and 3125 appearing as a further case. G5 is defined as the constant 5 carrying the configDim label.
proof idea
One-line wrapper that applies the decide tactic to confirm the numerical identity between 3125 and the fifth power of the configDim generator.
why it matters
It supplies one concrete decomposition in the enumerated list of spectrum members from the module documentation, supporting the overall claim that the set {2, 3, 5} generates the entire RS cardinality spectrum. No parent theorems are recorded in the used-by edges. The result touches the cross-domain closure properties but leaves open the question of whether additional generators or operations become necessary for larger spectrum elements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.