twentyfive_decomp
plain-language theorem explainer
The equality 25 = 5² holds in the natural numbers, where 5 is the configDim generator. Researchers verifying the Recognition Science cardinality spectrum decompositions would cite this instance to confirm that 25 reduces to a polynomial in the primitive set {2, 3, 5}. The proof is a direct numerical check via the decide tactic.
Claim. $25 = 5^2$, where 5 is the configDim generator.
background
The module proves that every integer in the RS cardinality spectrum reduces to a polynomial in the generators G = {2, 3, 5} via addition, multiplication, exponentiation, and choose. The listed examples include 25 = 5² along with 4 = 2², 6 = 2·3, 8 = 2³ and 16 = 2⁴. This local setting is the structural meta-claim of C27 that no spectrum member lies outside such polynomials, with the upstream definition fixing G5 as the constant 5.
proof idea
One-line wrapper that applies the decide tactic to the numerical equality.
why it matters
This instance supplies one of the enumerated decompositions required by the C27 meta-claim that the entire RS spectrum is generated from {2, 3, 5}. It directly supports the module's goal of showing every spectrum member enumerated in C21 factors as a polynomial in the generators tied to binary face, spatial dimension D = 3, and configDim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.