threeOne25_is_D_fifth
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 in Recognition Science
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.
scope and limits
- Does not claim any physical interpretation for the value 3125.
- Does not prove that the decomposition into Dconfig^5 is unique.
- Does not connect 3125 to spatial dimension D=3 or the eight-tick octave.
- Does not address empirical tests of the spectrum against observations.
Lean usage
have h : (3125 : ℕ) = Dconfig ^ 5 := threeOne25_is_D_fifthformal statement (Lean)
94theorem threeOne25_is_D_fifth : (3125 : ℕ) = Dconfig^5 := by decide
proof body
Term-mode proof.
95
96/-! ## Non-primitives (integers that don't decompose cleanly) -/
97
98/-- 11 = 2³ + D − 2 is a less-clean decomposition (a prime close to cube). -/