A strict lower bound for the fractional part of a nonintegral cube root

Prove: $\{\sqrt[3]{n}\}>\frac{1}{3\sqrt[3]{n^2}}$ where $n$ is a positive integer not equal to a cube of any integer

Formalization Note: The source formalization omitted the fractional-part operation and used a square root with a natural-number fractional exponent. This correction represents the cube root by a nonnegative real r with r³=n and restores r−floor(r). Its denominator3r² equals3 times the cube root of n². The noncube condition is preserved for positive integers.

Source: InternLM Lean-Workbook, record lean_workbook_plus_70623 (Apache-2.0).