Minimal period

Remarks

Let $p$ be the minimal period of $x$. Then $f^m(x) = x$ holds exactly when $p$ divides $m$: write $m = qp + r$ with $0 \le r < p$; then $x = f^m(x) = f^r(x)$, so $r = 0$ by minimality. The points $x, f(x), \dots, f^{p-1}(x)$ are distinct, so the orbit of $x$ has exactly $p$ points. A point has minimal period $1$ exactly when it is a fixed point.

Example: for $f(x) = -x$ on $\R$ and $x = 1$, one has $f(1) = -1 \ne 1$ and $f^2(1) = 1$, so the minimal period is $2$.

Non-example: for the same map, $2$ is not the minimal period of $0$. It is a period, since $f^2(0) = 0$, but already $f(0) = 0$, so the minimal period of $0$ is $1$.

In Lean's Mathlib, Function.minimalPeriod f x is defined for all $x$ and takes the value $0$ when $x$ is not periodic.