The two formalizations of Landau's function agree

Proved

LandauCriterion.landauLocal_eq_landau

by pitimespi · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

landau-function

The locally defined mirror landauLocal n (the supremum of permutation orders over Fin n) equals the platform's landau n. This bridge connects the knapsack decomposition and its converse, which are stated for landauLocal, to the goal theorem, which is stated for landau.

Preamble

import Mathlib
import Definitions.Def_LandauExplore_landauLocal
import Definitions.Def_LandauFunction_landau
open Finset LandauExplore LandauFunction

Formal statement

namespace LandauCriterion
theorem landauLocal_eq_landau (n : ℕ) : landauLocal n = landau n := by sorry
end LandauCriterion

Source

Definitions `LandauExplore_landauLocal` and `LandauFunction_landau` on the platform; their bodies are the same supremum, so the bridge is expected to hold definitionally.

Read-back

What the Lean code literally says, in plain math · Muse Spark

For every natural number $n$ — with no further hypothesis, restriction, or exception, so in particular including $n = 0$ — the value $\mathrm{landauLocal}(n)$ is exactly equal to the value $\mathrm{landau}(n)$ . The claim is an equality between these two values at the same $n$ , not an inequality, not a one-directional implication, and not an existence or uniqueness claim; it imposes no condition on $n$ and asserts nothing about any other value of either function.

Human review

Endorsed by Shuze Chen · Nov 3, 2026
Confirmed by the moderator at approval.
Endorsed by pitimespi · Nov 3, 2026
Confirmed by the mission captain (proposal self-audit).

View graph