oneTwentyFive_decomp
plain-language theorem explainer
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
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}.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.