A Conjecture That Was False by One Exponential

Tier: THEOREM (Lean-verified: the refutation, the corrected statement, and the implication between them)

We had a result we wanted about how quickly a shallow expression in our exp–log grammar can approach zero. It fit the lower-depth results. It was reasonable enough to write down as a named proof obligation and build on.

It was false.

More interestingly, it was false at exactly one scale. Replacing a linear term in the proposed bound by an exponential one produces a statement that is not merely plausible — it is proved. And the relationship between the two statements is itself a theorem, which is what lets us say something more precise than “we adjusted it until it went through.”

The conjecture

Write a depth-3 term as exp(A x) − log(B x) with A and B of depth at most 2. When that quantity is positive it can be very small, and the question is how small: how fast can a shallow expression decay?

At depth 2 the answer was already known — the decay bound V₂ reads C + log x. Reading the progression off the levels below, log x → x looked like the obvious next rung. So we named it:

Depth3DecayHard :   −log( exp(A x) − log(B x) )  ≤  C + x

for all depth-≤2 A, B, past some ray, wherever the quantity is positive.

That is the shape of the mistake, and it is worth naming precisely: we read a progression off two data points. log x then x suggests x then — what? The tempting answer is the one that continues an arithmetic-looking sequence. But each level of this grammar costs a whole exponential, not a step along log x → x → …. The progression was never additive.

The refutation

Take A = var and B the depth-2 tree evaluating to exp(exp x) − log x. Then

node = exp x − log( exp(exp x) − log x ) = −log( 1 − log x / exp(exp x) ) ≈ log x · exp(−exp x)

This is positive, so the hypotheses of the conjecture hold. And it is super-exponentially small, giving −log node ≈ exp x − log log x. No constant C satisfies −log node ≤ C + x.

not_depth3DecayHard : ¬ Depth3DecayHard

Two things about that refutation matter more than the fact of it.

It is machine-checked, including the asymptotics. Not a numerical demonstration with a proof sketch attached — the witness (dep3CounterRight_depth, dep3CounterRight_eval) and the growth argument are both in Lean. There are no numerics inside the proof.

The witness has depth 2. The conjecture is about depth-3 terms, and it is refuted by a counterexample built from a depth-2 subtree. The failure was not hiding somewhere deep.

For illustration only — this is not the evidence, the theorem is — the excess −log node − x runs

x  =    2      3      4       5       6        7        8
       5.8   17.0   50.3   142.9   396.8   1089.0   2972.2

matching exp x − log log x to every digit computed. That is what “false by one exponential” looks like numerically. It is not close.

The correction, and why it is not arbitrary

Replace the rung:

Depth3DecayExp :   −log( exp(A x) − log(B x) )  ≤  C + exp x

This is now a theorem — depth3DecayExp_holds — proved by decomposing an arbitrary depth-≤2 A into four cells (growing, constant, var, bounded), discharging each, and then proving the dispatch that shows those four cells actually cover an arbitrary A.

Here is the part we think is worth the post. The obvious suspicion about any formalisation effort is that the statement got weakened until the prover stopped complaining. So we proved the relationship:

depth3DecayExp_of_hard :  Depth3DecayHard → Depth3DecayExp

Put the three together:

The implication runs one way, the antecedent is false, the consequent is true. That pins the pair exactly. C + x and C + exp x are one exponential apart, the stronger of the two is provably unavailable, and the weaker one holds. We did not weaken past what the counterexample forced — and that sentence is a theorem here, not a description of our intentions.

One detail we would rather state than let a reader discover: only one of the four cells actually needs the corrected rung. The growing and const cells are weakenings of results that prove the stronger C + x bound on their own territory, and remain true. A refutation invalidates a conjecture, not the lemmas proved on the way to it. The var cell is where the counterexample lives, and it is the cell that forced the change.

Why the scale is the interesting part

This is not an isolated correction. It is one instance of the pattern this project keeps finding: depth in this grammar produces sharp transitions, and the transitions are locatable exactly.

Two of them are now machine-checked in both directions:

Neither is a bracket with an unproved middle. The exclusion is proved on one side and the failure is proved on the other — value_gap_fails_at_depth_three and band_exclusion_fails_at_depth_four are theorems, not open questions politely labelled.

The decay conjecture belongs to the same picture. Depth 2 admits one asymptotic scale; depth 3 admits a strictly larger one; and the counterexample is what located the boundary rather than bracketing it.

Scope, stated plainly

These results concern this finite exp–log grammar and this syntactic depth measure. We do not claim the same thresholds hold for other grammars, and nothing here shows the phenomenon is about exp–log specifically rather than about any grammar with a comparable growth ladder.

The broader fact that exp/log-definable functions are tame is classical and not ours — o-minimality of the real exponential field, Pfaffian methods, and Khovanskii-style finiteness are the deep structural theory here. What is ours is narrower: specific finite depth thresholds in this grammar, located and machine-checked, with the failures proved rather than conjectured.

Named obligations are supposed to make it possible to build on something before it is proved, without pretending it is. This one paid that back in the least comfortable and most useful way: it turned out to be false, the ledger said so, and the correction is now pinned from both sides.

A conjecture that fails by an unknown amount is a setback. One that fails by exactly one exponential is a measurement.