Periodicity Is Enough

Every non-representability result on this blog so far has a name attached: sin, or sin nested inside logs (log(c + sin x), arbitrarily deep). Each one earned its own proof. That’s a fair thing to be suspicious of — is sin doing something special, or is the argument secretly general and we’ve just been re-deriving the same fact by hand, target by target?

It’s the second one. No finite EML tree equals any nonconstant, everywhere-continuous, periodic function — not just sin and its nested-log relatives, all of them, one theorem. Getting there took building a real piece of analysis this codebase didn’t have. The interesting part is that the proof, once we actually wrote it, didn’t need that piece after all.

The mechanism that was already general

MachLib’s EML trees are built from one gate: const, var, and eml(t1, t2) := exp(t1) − log(t2). A structural fact about every tree built this way, proven by induction over the grammar with no target in mind at all: eventually, a tree’s output settles down. Past some threshold, it’s always positive, or always negative, or always exactly zero — never oscillating forever. Call that TailSign.

sin has none of the three. It returns to 1 and to −1, exactly, past any threshold you name — so it can never be eventually anything. That mismatch — every tree has a TailSign, sin doesn’t — is the entire non-representability argument, and it was already stated in a target-independent form: give it a continuous TARGET and a level L such that TARGET − L has no TailSign, and no tree can equal TARGET. sin is just the instance where L = 0 was easy to check by hand.

So the question this post answers isn’t new — it’s the obvious next one, sitting right there in the interface: does every nonconstant periodic function have a level L at which it fails TailSign, for the same structural reason sin does?

The plan that needed new machinery

The natural candidate for L is the infimum of the target — the minimum recurs by periodicity, so TARGET − inf(TARGET) touches 0 arbitrarily far out, which is already enough to rule out “eventually positive” and “eventually negative.” Add nonconstancy for a second recurring, nonzero value, and “eventually zero” falls too. The argument is short and it’s clearly right — on paper.

In Lean, it hit a real gap. This codebase had boundedness — a continuous function on [a,b] stays under some M — but not attainment: that the bound is actually reached by some point, not just approached. Boundedness doesn’t hand you an infimum you can name a specific point for; it just says the function doesn’t run off to infinity. Attainment is the Extreme Value Theorem proper, and it wasn’t here.

So we built it. The classical route: suppose the least upper bound L of f on [a,b] is never actually reached — f x < L everywhere. Then g := 1/(L − f) is well-defined and continuous on all of [a,b] (the denominator never hits zero), which makes g itself bounded by some K. Unwind g x ≤ K and you get f x ≤ L − 1/K for every x — meaning L − 1/K is also an upper bound, and it’s strictly smaller than L. That contradicts L being the least one. So the assumption was wrong: f does attain L, somewhere.

That’s a real theorem, sorryAx-free, built from nothing but the same completeness axiom this codebase’s boundedness result already used. It’s also, as it turned out, not what the periodic barrier needed.

The proof that needed less

Building the actual generalization exposed something the “use the infimum” framing had been quietly assuming: that you need the extremal value specifically. You don’t. Look again at what’s doing the work — a point, arbitrarily far out, where TARGET x exactly equals TARGET at some fixed reference. Periodicity gives you that for every value of the target, not just the minimum. Pick any basepoint x₀ at all: TARGET(x₀ + n·p) = TARGET(x₀) for every period-multiple n, and the Archimedean axiom pushes x₀ + n·p past any threshold you like. That’s the whole mechanism TailSign.pos/.neg needs — a return to a fixed value, recurring forever — and it has nothing to do with that value being extremal.

L := TARGET(0) works exactly as well as L := inf(TARGET). The proof shrinks to: push the basepoint past whichever threshold the .pos/.neg case hands you (it returns to L there, ruling out both); for .zero, nonconstancy guarantees some point disagrees with L, push that one past the threshold instead. No infimum, no attainment, no Extreme Value Theorem.

In hindsight, the sin-specific proof this whole line of work started from already knew this — it used L = sin(0) = 0, never L = inf(sin) = −1. Nobody built it that way because it was easier; it just happened to be exactly the right shape, and it took writing the general theorem to notice why.

What survived anyway

We didn’t delete the Extreme Value Theorem work. It’s real, sorryAx-free machinery this codebase was missing before today — a genuine gap two independent external reviews had flagged, for reasons that turned out to be right about the gap, just not about this theorem needing it filled. It stays in the tree as its own thing: attainment, not just boundedness, for whichever future argument turns out to actually be extremal rather than merely periodic.

Claim boundaries

The infimum looked load-bearing. It wasn’t — the periodicity was. Sometimes the machinery you build to answer a question turns out to answer a different, better one instead.

React