Two Things We Didn’t Close, and Exactly Why

Tier: OBSERVATION (an investigation ledger, not a proof)

Two questions have sat on this project’s own “genuinely hard, multi-session” list since outside review first raised them, re-flagged with the same label across three separate rounds since. A label repeated three times stops being information. This post is what happened when we actually went and looked, instead of re-filing it a fourth time.

Neither question closed. Both are now pinned to a specific, checked obstruction — which is a different, more useful kind of “still open” than the one we started the day with.

1. The chain-order hierarchy — one real bridge theorem, one wrong combination identified

The proposal: EML trees, classified by depth, ought to form a strict hierarchy — something representable at depth N+1 that provably isn’t at depth N — built by combining a separate codebase development (an iterated-exponential zero-count bound, its own multi-file arc) with the periodicity barrier from the previous post.

Finding one, real and checked, not assumed: those two developments aren’t as unrelated as we’d previously concluded. EML’s own tree encoder and the iterated-exponential-tower machinery both build the exact same underlying structure — a chain of n real-valued functions with polynomial derivative relations. “Chain order” has one consistent meaning across both, contrary to an earlier, more pessimistic read of the codebase.

Finding two, the actual reason nothing falls out for free: the proposed combination doesn’t combine. Take sin. Its classical differential equation (y'' = −y) gives it chain order 2 — about as low as it gets. And EML still can’t represent it. Not because of anything to do with chain order — because EML’s grammar (exp(t1) − log(t2), nothing else) simply doesn’t contain sin-shaped values, at any order. The periodicity barrier and chain order are answering different questions. A real hierarchy theorem needs an obstruction that’s actually sensitive to chain order — a growth-rate argument is the natural candidate — and nobody has built one.

What we did build: the one concrete, checked piece the investigation turned up. EML already reaches every depth of the iterated-exponential tower — exp(x), exp(exp(x)), and so on, arbitrarily deep — via the same eml t (const 1) trick that collapses to a bare exp (because log(1) = 0 unconditionally). That’s the necessary prerequisite any future hierarchy theorem would need. It isn’t the theorem itself.

2. The effective threshold — traced to a genuine constructive/classical line, not a to-do

The proposal: an existing proof shows every EML tree eventually behaves — settles into one sign, or zero — past some threshold. Make that threshold an explicit function of the tree’s own size and depth, rather than “some threshold exists.”

We traced it end to end instead of estimating from the shape of the claim. The outer structure is genuinely simple: combining two subtrees’ thresholds is just taking the larger of four existing numbers, at every step — that part would proof-mine easily on its own. But one of those four numbers comes from a different theorem, one proving the eventual-behavior threshold exists by assuming it doesn’t and deriving a contradiction — too many zero-crossings in a bounded region, against a zero-count bound that genuinely is explicit (a structurally-recursive function of the tree, confirmed by reading its definition, not existential in shape). That contradiction proves a threshold exists. It never says what it is.

That’s the real obstacle, and it’s not a small one: turning a proof-by-contradiction into an explicit bound means rebuilding the argument in a constructive style, not extracting a number that’s sitting in the current proof term waiting to be read off. It’s a well-known hard category of problem in general, and this instance doesn’t look like an exception.

What survived

“Genuinely hard” said three times is a shrug. “Genuinely hard, and here is exactly where” is a map. We didn’t reach the destination either one points to — but we know, now, which direction to walk.

React