# Proof: \(\text{eml}(a, b) = \exp(a) - \ln(b)\) satisfies \(\text{eml}(x, 1) = \exp(x)\)

- **Generated:** 2026-04-16
- **Verdict:** PROVED
- **Original result:** A. Odrzywołek, "All elementary functions from a single binary operator," [arXiv:2603.21852](https://arxiv.org/abs/2603.21852) (2026). This proof provides independent computational verification.
- **Audit trail:** [proof_audit.md](proof_audit.md) | [proof.py](proof.py)

## Evidence Summary

| ID | Fact | Verified |
|----|------|----------|
| A1 | ln(1) = 0 (symbolic verification) | Computed: True (ln(1) = 0 confirmed) |
| A2 | eml(x, 1) - exp(x) = 0 (symbolic simplification) | Computed: True (residual identically 0) |
| A3 | Numerical spot-check at 5 complex points | Computed: True (max residual = 0.00e+00) |

## Proof Logic

The claim defines a binary operator eml(a, b) = exp(a) - ln(b) and asserts that evaluating it at b = 1 yields exp(x) for every complex number x. The proof reduces to a single algebraic fact: ln(1) = 0.

**Key identity (A1).** The natural logarithm of 1 is 0. This holds for the principal branch of the complex logarithm: Log(z) = ln|z| + i·Arg(z), and since |1| = 1 and Arg(1) = 0, we get Log(1) = 0. SymPy confirms this symbolically.

**Symbolic simplification (A2).** Substituting b = 1 into the operator definition: eml(x, 1) = exp(x) - ln(1) = exp(x) - 0 = exp(x). The residual eml(x, 1) - exp(x) = exp(x) - ln(1) - exp(x) simplifies to exactly 0 for symbolic x (A2 depends on A1). This is an algebraic identity, not an approximation.

**Numerical cross-check (A3).** As an independent verification, the identity was evaluated numerically at five representative complex points: x = 0, 1, -3, iπ, and 2+3i. At every point, |eml(x, 1) - exp(x)| = 0.00 — exact agreement to machine precision. The symbolic result (A2) and numerical cross-check (A3) agree completely.

## What could challenge this verdict?

Three adversarial checks were investigated:

1. **Branch ambiguity of the complex logarithm.** The principal branch Log(z) = ln|z| + i·Arg(z) gives Log(1) = 0. Since z = 1 lies on the positive real axis, far from the branch cut along the negative real axis, there is no branch ambiguity. All standard branches of the logarithm agree at z = 1.

2. **Well-definedness of the operator.** The operator eml(a, b) has a singularity at b = 0 (ln(0) is undefined), but the claim fixes b = 1. The exponential function exp(x) is entire (defined for all complex x), and subtracting the constant ln(1) = 0 preserves this. The operator is well-defined for every complex x.

3. **Numerical precision.** The symbolic computation uses SymPy's exact algebra engine, not floating-point arithmetic. The residual is symbolically zero — not approximately zero. The numerical cross-check is supplementary; the proof does not depend on it.

## Conclusion

**Verdict: PROVED.** The identity eml(x, 1) = exp(x) holds for every complex number x. The proof rests on the algebraic fact that ln(1) = 0 (A1), which makes the residual eml(x, 1) - exp(x) identically zero (A2). Numerical evaluation at 5 complex points independently confirms exact agreement (A3).

---

Generated by [proof-engine](https://github.com/yaniv-golan/proof-engine) v1.18.0 on 2026-04-16.