2026-04-19 theorem 4 min read

T19: 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 the limit of how close you can get.

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. Starting from {1}, every input to every node is a positive real number (since 1 > 0, exp maps reals to positive reals, and we only pass positive inputs to ln).
  2. Under principal-branch ln, every intermediate value is a real number. exp of a real is real. Subtraction of reals is real.
  3. i is not real. ∎

There is no way around this under strict semantics: the grammar is closed over the positive reals when initialized with {1}.

Lean verification

This theorem is formalized in StrictBarrier.lean with 0 sorries. The key lemma: given initial values in ℝ+, every EML tree value stays in ℝ+. The proof proceeds by structural induction on the tree.

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 closest known approach to Im = 1 is 0.99999524 — a gap of 4.76 × 10⁻⁶. This is not a rounding error; it is a transcendental obstruction. See the near-miss post for the full analysis and the depth-6 phase transition post for the structural picture.

Reproduce

The Python package always returns a float from real inputs:

python -c "from monogate import eml; print(type(eml(1, 1)))"
# <class 'float'> — always real under strict semantics

Cite this work

Monogate Research (2026). "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

React