Oscillation Is a Compact Torus

Here are two functions that look like siblings and behave like opposites:

y'' + y = 0   →   sin x, cos x      (infinitely many zeros)
y'' − y = 0   →   eˣ,  e⁻ˣ          (no zeros at all)

In the EML world — where a function’s complexity is the minimum depth of the tree built from the single gate eml(x, y) = exp(x) − log(y) — these two land on opposite sides of a hard line. eˣ is a finite EML tree (depth 1, in fact: exp(x) − log(1)). sin x is not a finite EML tree at any depth, because of the Infinite-Zeros Barrier: a real-analytic function with infinitely many zeros on every compact set cannot be a finite EML expression.

The two ODEs above have the same complex differential Galois group — the torus 𝔾_m. So what distinguishes them? This post is about the answer, which is cleaner than we expected:

The Infinite-Zeros Barrier is the compact (rotational) torus factor of the differential Galois group. Split torus (real ℝ*, exponential growth) → finite zeros → EML-finite. Compact torus (rotation SO(2), oscillation) → infinitely many zeros → EML-∞.

eˣ is a split torus. sin x is a compact one. Same complex group; the real form decides. Everything below follows from taking that seriously.

The discriminant is the boundary

The cleanest evidence is that you can flip a function across the line by changing a single coefficient. Take the constant-coefficient and Euler families and read off the characteristic / indicial roots:

y'' + ω²y = 0  (ω real)      complex roots → compact torus  → sin/cos          → EML-∞
y'' − k²y = 0  (k real)      real roots    → split torus    → e^{±kx}          → EML-finite

x²y'' + axy' + by = 0,  Δ ≥ 0   real exponents  → split    → x^{r}             → EML-finite
x²y'' + axy' + by = 0,  Δ < 0   complex exps    → compact  → x^α cos(β log x)  → EML-∞

The sign of the discriminant — whether the roots are real (overdamped / hyperbolic) or complex (underdamped / oscillatory) — is the EML-finite / EML-∞ boundary. The classical “is it ringing or is it decaying?” question and the “can I write this as a finite EML expression?” question turn out to be the same question.

A strict three-chain (and Airy is the punchline)

The standard one-line slogan — “EML-finite means the ODE is solvable in elementary terms” — is too coarse. There are three different finiteness notions in play, and they form a strict tower:

EML-finite (real)   ⊊   elementary / Liouvillian   ⊊   Pfaffian (finite chain order)
──────────────          ────────────────────────       ──────────────────────────────
x^r, e^{kx},            + sin/cos, half-integer         + Airy, Bessel, Mathieu
polynomials             Bessel j₀ = sin x / x           (Galois group SL₂, not even
(split / unipotent)     (compact torus, Liouvillian)     Liouvillian — but still
                                                          o-minimal, zero-counted)

First ⊊: sin x is Liouvillian — its Galois group is solvable (a torus), it has a perfectly good closed form. But it oscillates, so it is not a finite EML tree. Solvability by quadratures is necessary but not sufficient for EML-finiteness. The missing condition is “split real form.”
Second ⊊: Airy. y'' = x·y has differential Galois group SL₂(ℂ), which is not solvable — by Kovacic’s algorithm it has no Liouvillian solution at all. Yet it is a Pfaffian function of chain order 3 (the standard fewnomial zero-count bounds apply). So Pfaffian / Khovanskii finiteness does not imply EML-finiteness. Airy is the function that lives in the gap.

We keep a registry of “Pfaffian-but-not-EML” special functions in eml-cost — Bessel, Airy, Mathieu, hypergeometric, each with a chain order. The three-chain says exactly why each one is on that list, and which of two distinct reasons (compact torus, or non-solvable Galois) put it there.

From a table lookup to a computation

That registry used to be hand-curated: a human decided “Bessel is not EML-finite” and wrote down a chain order. The Galois picture lets us derive that verdict from a function’s defining differential equation instead.

Given any y'' + p(x)y' + q(x)y = 0, reduce it to the Schrödinger normal form u'' = r·u (r = p²/4 + p'/2 − q), and read the EML class off the oscillation of r — which, by Sturm’s theory, is governed by exactly the same −1/4 threshold that controls the local indicial exponents ½(1 ± √(1+4b)). (Complex exponent ⟺ b < −1/4 ⟺ oscillatory ⟺ compact torus: it is all one computation.) That is the heart of Kovacic’s Case-1 decision for the solvable cases, and it is now a function you can call:

>>> from eml_cost import classify_ode
>>> classify_ode(0,  1).eml_class      # y'' + y = 0  (harmonic)
'EML-infinity'
>>> classify_ode(0, -1).eml_class      # y'' − y = 0  (hyperbolic)
'EML-finite'
>>> classify_ode(0, '-x').eml_class    # y'' − x y = 0  (Airy)
'EML-infinity'

We then ran the whole special-function registry back through it. Of the 68 entries, 17 are solutions of a second-order linear ODE; for the 12 oscillatory ones (ordinary and spherical Bessel, Hankel, all four Airy functions) the classifier independently re-derives EML-∞ from the coefficients, agreeing with the hand-curated table on every one — and contradicting it on none. The five non-oscillatory genuine special functions (modified Bessel, erf) it honestly leaves as candidates, because confirming those needs the full Kovacic constructor, which we did not build. The table is now machine-checked where the cheap method is decisive, and the tool says exactly where it isn’t.

The same verdict drives a small product surface: an EML-readiness linter for ODE-defined functions (can I synthesize a kernel for this, or only approximate it on a bounded interval?), and an EML-finiteness penalty for EML symbolic regression that biases the learner toward representable forms.

What we machine-checked

The conceptual story is one thing; we also wanted the load-bearing analytic facts to be theorems, not heuristics. So they live in MachLib, our Mathlib-free Lean library, and the statements below are #print axioms-clean — no sorry, only the declared analytic axioms (rolle, the HasDerivAt rules, the Real foundation):

The oscillation barrier as an asymptotic-class fact. sin has zeros arbitrarily far out (k·π → ∞ by Archimedeanness), and every “eventually signed” growth class is disjoint from that. So sin lands in none of the EML asymptotic classes — the precise sense in which the compact-torus side escapes the EML-finite classification. Its mirror: eˣ = eml(var, const 1) is an EML tree and does sit in a signed class. Both sides of the dichotomy, witnessed.
Sturm non-oscillation for r ≥ 0. For u'' = r·u with r ≥ 0, there is no “positive arch” (and, by a clean reflection, no negative arch) between two zeros. Since oscillation requires such arches, r ≥ 0 ⇒ non-oscillatory ⇒ EML-finite. Proved from Rolle and the Mean Value Theorem — no completeness or first-zero machinery needed. When classify_ode returns EML-finite because r ≥ 0, it now hands back a certificate citing this theorem by name.
The Euler −1/4 keystone + Abel core. The harder case — r = c/x² with −1/4 ≤ c < 0, non-oscillatory even though r < 0 — needs an explicit positive comparison solution v = x^α. We proved that x^α solves x²v'' = (α²−α)v (the real-power second derivative, which forced us to build some field algebra MachLib was missing — (1/x)(1/x) = 1/x² and friends, from mul_inv), and then the full Abel–Wronskian core: the Wronskian of two Euler solutions is constant, and φ'·v² = W. That discharges all the algebra of the regular-singular theorem.

One small war story from the last item: the Wronskian cancellation needs full multiplicative associativity-commutativity (u·V·α·B = V·u·α·B), which our mach_ring tactic cannot canonicalise — a long-known gap. Rather than build the “ring v2” that would fix it in general, we reached for Lean’s ac_rfl against Real’s registered Std.Commutative / Std.Associative instances, and it went straight through. A reminder that the right small tool often beats the right big one.

Honest scope

Three things we are not claiming.

No new differential Galois theory. That Airy’s group is SL₂, that half-integer Bessel is Liouvillian, that the Euler indicial roots flip at the discriminant — these are textbook (van der Put–Singer; Kovacic 1986). The contribution here is the bridge to EML depth (the compact-torus reading), the formalization, and the tooling that makes the verdict computable and the table self-checking. Not a theorem in Galois theory.
The −1/4 theorem is not finished. Its keystone and its entire Abel core are machine-checked; what remains is the Mean-Value-Theorem sign-glue — pure logic, no algebra blockers, scoped in the file. Until that lands, classify_ode honestly reports the −1/4 Euler band as non-oscillatory but not yet Lean-certified. We would rather say “almost” than round up.
The dichotomy is a clean necessary condition, an iff only where we proved it. “EML-finite ⟹ solvable Galois group with a split real form” is the safe, established direction, with explicit witnesses. The converse we closed for the constant-coefficient and Euler families; the general n-th-order converse carries an extra “elementary tower” hypothesis we have not discharged.

What we do claim is the part that made the work worth doing: a single, legible idea — oscillation is the compact torus — that simultaneously explains an EML barrier, classifies a shelf of special functions from their differential equations, and reduces to a handful of Lean theorems we can point at. The line between the functions you can write down and the ones you can only approximate has a name now, and it is rotational.

Monogate Research (2026). “Oscillation Is a Compact Torus.” monogate research blog. https://monogate.org/blog/oscillation-is-a-compact-torus

React