threeOneTwentyFive_decomp
plain-language theorem explainer
The theorem establishes that 3125 equals the fifth power of the configDim generator G5 defined as 5. Researchers verifying the RS spectrum decompositions from the set {2, 3, 5} would cite this result to confirm closure under exponentiation. The proof is a direct decision procedure that evaluates the numerical equality.
Claim. $3125 = 5^5$, where $5$ is the configuration dimension generator.
background
The module proves that every integer in the RS cardinality spectrum is generated from the primitive set G = {2, 3, 5} using addition, multiplication, exponentiation, and binomial coefficients. G5 is the sibling definition G5 := 5 corresponding to configDim. The local theoretical setting is the meta-claim that the spectrum enumerated in C21 admits no members outside such polynomial expressions in these three generators.
proof idea
The proof is a one-line wrapper that applies the decide tactic to confirm the concrete numerical identity 3125 = 5^5.
why it matters
This result fills one entry in the enumerated decompositions required by the module's structural meta-claim on spectrum generation from {2, 3, 5}. It supports downstream cardinality arguments in the Recognition Science forcing chain (T0-T8) and phi-ladder mass formulas by ensuring all listed spectrum members reduce to the three generators. No open questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.