Landau's function $g(n)$

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement below, with full knowledge of the source material and of the intended meaning. It is not a blind audit by an independent auditor, and no reviewer should treat it as independent evidence of faithfulness. It was produced at the explicit request of the proposal owner.

This file declares, inside the namespace LandauFunction, a function $g:\mathbb N\to\mathbb N$ (named landau). For each natural number $n$, $g(n)$ is the supremum, in $\mathbb N$ with its usual order (whose least element is $0$), of the orders $\operatorname{ord}(\sigma)$ taken over all permutations $\sigma$ of the $n$-element set $\{0,1,\dots,n-1\}$. Here $\operatorname{ord}(\sigma)$ is the order of $\sigma$ in the permutation group, i.e. the least $k\ge1$ with $\sigma^k=\mathrm{id}$ (every permutation of a finite set has finite order, so the library's junk value $0$ for elements of infinite order never occurs).

Since the set of permutations is finite and nonempty (it always contains the identity, also when $n=0$, where the only permutation is the empty one), the supremum is a genuine maximum: $g(n)=\max_{\sigma\in S_n}\operatorname{ord}(\sigma)$. In particular $g(0)=g(1)=1$. The function is marked noncomputable only because the library's order function is; this has no effect on its value.