# Proof: \(\text{eml}(1, 1) = e\)

- **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 | exp(1) = e (symbolic verification) | Computed: True (exp(1) = e confirmed) |
| A2 | ln(1) = 0 (symbolic verification) | Computed: True (ln(1) = 0 confirmed) |
| A3 | eml(1, 1) - e = 0 (symbolic simplification) | Computed: True (residual identically 0) |

## Proof Logic

The claim defines eml(a, b) = exp(a) - ln(b) and asserts that eml(1, 1) equals the mathematical constant e. The proof decomposes into two elementary facts and their combination.

**exp(1) = e (A1).** The exponential function evaluated at 1 returns e by definition. SymPy confirms that exp(1) - E (where E is SymPy's exact symbolic constant for Euler's number) simplifies to 0.

**ln(1) = 0 (A2).** The natural logarithm of 1 is 0. For the principal branch of the complex logarithm: Log(z) = ln|z| + i·Arg(z). At z = 1: |1| = 1 and Arg(1) = 0, giving Log(1) = 0. SymPy confirms ln(1) = 0 symbolically.

**eml(1, 1) = e (A3).** Substituting a = 1, b = 1 into the operator definition: eml(1, 1) = exp(1) - ln(1) = e - 0 = e. SymPy confirms that exp(1) - ln(1) - E simplifies to exactly 0 (A3 depends on A1 and A2).

As an independent cross-check, the identity was verified numerically: Python's `cmath.exp(1) - cmath.log(1)` returns 2.718281828459045, which matches `math.e` to all 15 displayed digits. The absolute difference is 0.00e+00.

## What could challenge this verdict?

Three adversarial checks were investigated:

1. **Is exp(1) exactly e?** Yes — this is definitional. The exponential function is defined such that exp(1) = e. SymPy represents this as the exact symbolic constant E, not a floating-point approximation.

2. **Does ln(1) = 0 hold for the complex logarithm?** Yes. The point z = 1 lies on the positive real axis, far from the branch cut along the negative real axis. All standard branches agree: Log(1) = 0.

3. **Could the symbolic simplification miss a nonzero result?** No. SymPy evaluates exp(1) to E and ln(1) to 0 before simplify() is called. The remaining expression E - 0 - E = 0 is trivial constant arithmetic, not a complex cancellation.

## Conclusion

**Verdict: PROVED.** The expression eml(1, 1) = exp(1) - ln(1) equals the mathematical constant e. This follows from two elementary facts: exp(1) = e by definition (A1) and ln(1) = 0 in the principal branch (A2). The combined identity eml(1, 1) - e = 0 is confirmed symbolically (A3) and numerically.

---

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