threeOne25_is_D_fifth
plain-language theorem explainer
3125 equals five to the fifth power where five is the configuration dimension in the Recognition Science cardinality spectrum. Cross-domain cardinality researchers cite this as an explicit witness that 3125 belongs to the structured set generated from config primitives and cube generators. The proof is a direct decision procedure that evaluates the numerical identity after substituting the definition of Dconfig.
Claim. $3125 = 5^5$ where $5$ is the configuration dimension $D_5$.
background
The CrossDomain.CardinalitySpectrum module collects witnesses showing that RS cardinalities form a structured spectrum reachable from the generators 2, 3 and the configuration dimension 5. Dconfig is defined as the constant 5. The module documentation states that every listed cardinality, including 3125, admits a decomposition into these RS primitives rather than appearing arbitrarily.
proof idea
The proof is a term-mode decision that substitutes Dconfig := 5 into the equality and invokes the decide tactic to confirm 3125 = 3125.
why it matters
This supplies the witness for 3125 in cardinalitySpectrumCert, which assembles the full spectrum certification including Dconfig_is_5. It directly supports the module claim that the spectrum is generated from configDim 5 and small cube factors, consistent with the eight-tick and D=3 landmarks in the forcing chain. It leaves open the mapping of these cardinalities onto physical gaps or Berry thresholds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.