T17: Why You Can't Build i from 1

The imaginary unit is not reachable from the grammar {eml, 1} under strict real semantics. Here is the proof, and how close the complex grammar gets.

Correction (2026-09-13): this post was titled "T19: Why You Can't Build i from 1". The catalog entry is T17; T19 is only part of the Lean theorem's name. Its proof said every value in the grammar is a positive real, which is false: e − ln(e^e) = 0 at depth 3, and 1 − e is a depth-4 value. What holds, and what the proof needs, is that every defined value is real. The post also called the depth-6 gap "a transcendental obstruction", which nothing shows, and its reproduce command imported a function that this repository's package does not export.

The question

The EML grammar starts with the constant 1 and the binary operator eml(x, y) = exp(x) − ln(y). Can finite tree composition of this grammar produce the imaginary unit i = √(−1)?

The answer depends on the semantics of ln. Under the strict principal-branch convention — where ln is defined only for positive real inputs and returns a real output — the answer is provably no.

The proof (three lines)

1. eml(x, y) = exp(x) − ln(y) takes two inputs. The leaf 1 is real, exp of a real is real, and strict ln is defined only on positive reals, where its value is real. Values can be 0 or negative, and a tree that then takes ln of one is undefined, not complex.
2. A difference of reals is real, so by induction every defined tree value is a real number.
3. i is not real. ∎

There is no way around this under strict semantics: every defined value of the grammar initialized with {1} is real.

Lean verification

This theorem is formalized as T19_i_unconstructible_strict in StrictBarrier.lean (in the private monogate-research repository). Its #print axioms has no sorryAx, and it is re-checked before every deploy. The proof is short and not inductive: the strict evaluator is typed to return real numbers, and i is not real.

The extended grammar question

What if we relax the semantics and allow ln to accept negative real inputs, extending via the complex logarithm? Then complex values enter the grammar for the first time at depth 5.

All depth-5 values with nonzero imaginary parts have Im = −π exactly. The imaginary axis is approached, but from the wrong direction and pinned to a fixed value.

At depth 6, the imaginary parts diversify. The depth-6 value closest to i is 8.07×10⁻⁸ + 0.99999523722i, at distance 4.76 × 10⁻⁶. Nothing shows that the gap cannot close at greater depth, and a depth-7 tree already brings its imaginary part within 7.9 × 10⁻¹² of 1 (though that value is 1.32 from i). See the near-miss post, which prints both searches, and the depth-6 phase transition post for the structural picture.

Reproduce

The strict grammar in plain Python floats, through depth 4. math.log raises on a non-positive input and math.exp on overflow, so those trees are skipped as undefined; every value that survives is a float, and some are 0 or negative.

import itertools, math
def eml(x, y):                           # strict real semantics: ln only of positive reals
    return math.exp(x) - math.log(y)     # raises ValueError for y <= 0, OverflowError past 1e308
S = {1.0}
for depth in range(1, 5):
    new = set()
    for x, y in itertools.product(S, repeat=2):
        try:
            new.add(eml(x, y))
        except (ValueError, OverflowError):
            pass                         # undefined (or too large to hold): no value
    S |= new
    print(f"depth <= {depth}: {len(S)} defined values, all of type float: {all(isinstance(v, float) for v in S)}, "
          f"min {min(S):.4g}, nonpositive: {sum(v <= 0 for v in S)}")

Output:

depth <= 1: 2 defined values, all of type float: True, min 1, nonpositive: 0
depth <= 2: 5 defined values, all of type float: True, min 1, nonpositive: 0
depth <= 3: 26 defined values, all of type float: True, min 0, nonpositive: 1
depth <= 4: 396 defined values, all of type float: True, min -14.15, nonpositive: 70

Cite this work

Monogate Research (2026). "T17: Why You Can't Build i from 1." (First published as "T19: Why You Can't Build i from 1.") monogate research blog. https://monogate.org/blog/i-unconstructibility

License

CC BY 4.0 — free to share and adapt with attribution. · Code: pip install monogate · Paper: arXiv:2603.21852