The asymptotic diameter of the n x n x n Rubik's Cube in the slice-turn and outer-block-turn metrics

We determine the leading constant of the arbitrary-pair graph diameter of the coloured-sticker n x n x n Rubik cube in both the slice-turn and outer-block-turn metrics: D(n) log(n) / n² tends to (1/4) log(24!/(4!)⁶). A slice-turn move turns one slice by 90, 180 or 270 degrees; an outer-block-turn move turns the outermost w layers at one of the six sides by such an angle, with 1 ≤ w ≤ n−1. Equal-coloured centre stickers are indistinguishable; the spatial frame is fixed and whole-cube rotations are not identified. The counting lower bound is standard; the contribution is the matching upper bounds. The paper contains proofs for the two diameters and solved-state radii, and discusses related metric conventions. The included Lean 4 formalization verifies the two fixed-frame arbitrary-pair diameter limits, with only the three standard axioms. It does not formalize the solved-state radius claims, Corollary 1.2 on other conventions, or the explicit-construction appendix. The earliest conjecture located in the sources is H. Kociemba's SpeedSolving forum post of 4 August 2011; OEIS A257401 is defined in a half-turn metric of sides, not STM. Assisted by AI.