The Monotonicity Theorem in O-Minimal Geometry 1: Monotonicity TheoremTextbook
## Motivation An **o-minimal structure** is a setting in which every definable subset of the line is tame: a finite union of points and open intervals. This single axiom rules out oscillation, space-filling behavior, and other pathologies, and it makes one-variable definable functions tractable. The central consequence is the **Monotonicity Theorem**: every definable function on an interval is piecewise constant or strictly monotone and continuous, with only finitely many pieces. The result originates in the work of Pillay and Steinhorn on o-minimality and is presented systematically in Lou van den Dries, *Tame Topology and O-minimal Structures*, Chapter 3 ([Cambridge University Press, 1998](https://doi.org/10.1017/CBO9780511529219)). A concise expository account is given in Mário Edmundo, *O-minimal structures* ([arXiv:math/0012051](https://arxiv.org/abs/math/0012051)). This mission formalizes the one-dimensional monotonicity theorem and its supporting lemmas in Lean 4 against Mathlib, as a verified entry point to o-minimal geometry. ## Setting Let $R$ be a type equipped with a **dense linear order without endpoints** $D$: an irreflexive, transitive, trichotomous relation $D.\mathrm{lt}$ in which every strict inequality admits an interpolant and every element has strict predecessors and successors. Finite Cartesian powers are represented as coordinate tuples $\mathrm{Power}\,R\,n := \mathrm{Fin}\,n \to R$, with coordinate projections, deletion, and append operations defined explicitly. An **o-minimal structure** $M$ over $D$ is a family $M.S\,n$ of collections of subsets of $\mathrm{Power}\,R\,n$, closed under finite unions and intersections, containing diagonals and the order relation, closed under products, coordinate reindexing, and existential projection, and satisfying the o-minimality axiom: every member of $M.S\,1$ is a finite union of points and open intervals. A **definable function** $f$ with domain $I$ and codomain $B$ is a dependent function on the corresponding subtypes whose domain, codomain, and graph are all members of $M$. For $a < b$ in $\mathrm{Power}\,R\,1$, the **open interval** $(a,b)$ is the set of coordinate tuples whose single coordinate lies strictly between the two endpoint values, with endpoint variants allowing $-\infty$ and $+\infty$. A function is **strictly increasing** (respectively **strictly decreasing**) on $I$ when $x < y$ implies $f(x) < f(y)$ (respectively $f(y) < f(x)$) in the first output coordinate. **Continuity** at a domain point is the graph-based epsilon-delta predicate: $x$ belongs to $\mathrm{ContinuousPoints}\,D\,I\,G$ exactly when the graph $G$ meets every sufficiently small box around $(x, f(x))$ in the graph of a locally oscillation-free correspondence. Finiteness and infinitude of one-dimensional sets are expressed through first-coordinate listings. ## Formalization targets ### Goal — Monotonicity theorem $$f : I \to B\ \text{definable},\ I\ \text{infinite} \implies \exists\, a = p_0 < p_1 < \cdots < p_k = b\ \text{with each}\ (p_i, p_{i+1})\ \text{good}.$$ An open cell $(p_i, p_{i+1})$ is **good** when $f$ restricted to $I \cap (p_i,p_{i+1})$ is constant, or strictly increasing and continuous there, or strictly decreasing and continuous there. The number $k$ of cut points is finite and depends on $f$, $a$, and $b$; no bound on $k$ is asserted. ### Supporting targets $$I\ \text{definable and infinite} \implies I\ \text{contains a nonempty open interval}.$$ $$f\ \text{definable} \implies \text{each value fiber}\ f^{-1}(z)\ \text{is definable}.$$ $$\text{Either some value fiber is infinite or every value fiber is finite}.$$ $$f\ \text{definable on infinite}\ I \implies f\ \text{is constant or injective on some subinterval}.$$ $$f\ \text{injective and definable} \implies f\ \text{is strictly monotone on some subinterval}.$$ $$f\ \text{strictly monotone and definable} \implies f\ \text{is continuous on some subinterval}.$$ ## Significance *The result itself.* The Monotonicity Theorem is the foundation of one-dimensional o-minimal geometry. It implies that definable sets have finitely many connected components, that definable functions have finite limits at endpoints, and that higher-dimensional cell decomposition can proceed by induction on dimension. Without it, the correspondence between definability and geometric tameness remains unestablished. *Formalizing it.* The classical proofs are known and appear in the references above; what is missing is a machine-checked version with explicit definability bookkeeping. This mission produces Lean 4 declarations for the order, interval, monotonicity, graph, and continuity predicates together with the theorem and its lemmas, all verified against the pinned Mathlib revision. The definability infrastructure (products, projections, fiber extraction) is reusable for subsequent cell-decomposition missions. Status honesty: the one-dimensional interval-extraction lemmas are machine-checked; the local constancy-or-injectivity lemma, the injective-to-monotone lemma, the finite-partition assembly, and the goal theorem itself remain open targets. ## Difficulty The naive argument fixes a point and inspects nearby values, but definability does not by itself provide any neighborhood on which behavior is uniform. The fiber dichotomy illustrates the obstruction: knowing that each fiber $f^{-1}(z)$ is definable does not decide whether some fiber contains an interval or every fiber is finite, and the two cases require different constructions (a constancy interval versus an injective-selection interval). Similarly, injectivity alone does not yield monotonicity without partitioning the domain by local sign patterns and applying o-minimality to select a uniform pattern on a subinterval. Each step fails until the relevant definable set is exhibited and the one-dimensional interval lemma is applied to it. ## Formalization scope Lean represents one-dimensional points as functions $\mathrm{Fin}\,1 \to R$, with order, intervals, and finiteness stated through the first coordinate. Definability is always the structure membership predicate $M.S\,n$, never an informal attribute. Continuity is the graph-based $\mathrm{ContinuousPoints}$ predicate applied to $\mathrm{FunctionGraph}\,f.\mathrm{toFun}$; a submission that discharges a continuity goal from the domain inclusion alone, or that replaces the continuity predicate by the domain set, does not satisfy the statement. The goal quantifies over cut points $p : \mathrm{Fin}\,(k+1) \to \mathrm{Power}\,R\,1$ with $p_0 = a$, $p_{\mathrm{last}} = b$, and strict increase at each step; the intervening sets $J$ are the open intervals determined by consecutive finite endpoints. Contributions welcome: direct proofs of the open leaves (fiber definability, the finite-fiber injective-interval construction, the injective-to-monotone step, the finite-partition assembly), sharper statements with explicit endpoint bounds, and reusable o-minimal infrastructure beyond this mission. Out of scope: higher-dimensional cell decomposition, differentiability, and integration of definable functions. ## Selected references - Lou van den Dries, Tame Topology and O-minimal Structures, London Mathematical Society Lecture Note Series 248, Cambridge University Press, 1998, Chapter 3. DOI: 10.1017/CBO9780511525919. - Mário J. Edmundo, An Introduction to O-minimal Structures, 2000. arXiv:math/0012051.