oneTwentyFive_is_Dcubed
plain-language theorem explainer
125 equals the cube of the configuration dimension in the Recognition Science cardinality spectrum. Cross-domain researchers cite this to confirm 125 arises as 5 cubed among the structured values generated from cube-generators, config dimension 5, and gap45. The proof is a direct decision procedure that verifies the arithmetic identity.
Claim. $125 = D^3$ where the configuration dimension $D$ equals 5.
background
The module collects witnesses showing that cardinalities of canonical RS domain types form a structured spectrum: {2, 3, 4, 5, 6, 7, 8, 10, 12, 15, 16, 45, 70, 125, 216, 256, 3125, ...}. Each entry decomposes via sums, products, or powers of the cube-generators {2, 3}, the configuration dimension 5, and gap45. The local setting is the claim that RS produces this non-random numerical spectrum rather than arbitrary integers.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the numerical equality 125 = 5^3.
why it matters
This witness feeds cardinalitySpectrumCert, which assembles the full spectrum certificate via Dspatial_is_3, Dconfig_is_5, gap_as_D, eightTick_as_D, and cubeFaces_as_D. It supplies the explicit 125 = 5^3 slot required by the module's structural claim. The result aligns with the forcing chain's use of small integers and powers while keeping the spectrum closed under the listed RS primitives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.