# Proof: \(\text{eml}(1, \text{eml}(\text{eml}(1, x), 1)) = \ln(x)\) for all real \(x > 0\)

- **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 | eml(1, x) = e - ln(x) (inner evaluation) | Computed: True (residual = 0) |
| A2 | eml(eml(1, x), 1) = exp(e)/x (middle evaluation) | Computed: True (residual = 0) |
| A3 | eml(1, eml(eml(1, x), 1)) - ln(x) = 0 (full identity) | Computed: True (residual = 0) |
| A4 | Numerical spot-check at 6 positive real points | Computed: True (max |diff| = 8.88e-16) |

## Proof Logic

The claim asserts that a triple nesting of the operator eml(a, b) = exp(a) - ln(b), evaluated at specific arguments, recovers the natural logarithm. The proof unwinds the nesting layer by layer.

**Inner layer (A1).** Evaluating the innermost call: eml(1, x) = exp(1) - ln(x) = e - ln(x). SymPy confirms this symbolically with zero residual.

**Middle layer (A2).** Feeding the inner result into eml as the first argument with b = 1: eml(e - ln(x), 1) = exp(e - ln(x)) - ln(1). Since ln(1) = 0, this reduces to exp(e - ln(x)). Using the exponent rule exp(a - b) = exp(a)/exp(b): exp(e - ln(x)) = exp(e) · exp(-ln(x)) = exp(e)/x. SymPy confirms this simplification exactly (A2 depends on A1).

**Outer layer and full identity (A3).** Feeding the middle result as the second argument to eml with a = 1: eml(1, exp(e)/x) = exp(1) - ln(exp(e)/x) = e - [ln(exp(e)) - ln(x)] = e - [e - ln(x)] = ln(x). The key steps: ln(exp(e)) = e (since ln and exp are inverse functions on the reals) and the logarithm of a quotient splits as a difference. SymPy verifies that the full nested expression minus ln(x) is identically 0 for symbolic positive x (A3 depends on A1 and A2).

**Numerical cross-check (A4).** The identity was evaluated numerically at six representative points spanning four orders of magnitude: x = 0.01, 0.5, 1, 2, e, and 100. At every point, the nested expression matched ln(x) to within 8.88e-16 — machine epsilon for float64 arithmetic. The symbolic result (A3) and numerical cross-check (A4) agree completely.

## What could challenge this verdict?

Four adversarial checks were investigated:

1. **Boundary behavior at x -> 0+.** As x approaches zero, intermediate expressions diverge (eml(1, x) -> +infinity, then exp of that -> +infinity). But the final cancellation e - (e - ln(x)) = ln(x) is algebraically exact regardless of the magnitude of intermediate values.

2. **Boundary behavior at x -> +infinity.** As x grows, eml(1, x) -> -infinity and exp(eml(1, x)) -> 0+. Despite intermediate values approaching 0 or -infinity, the identity holds exactly.

3. **Validity of ln(exp(y)) = y.** This step is the crux: it holds for all real y, since ln and exp are inverse functions on the reals. The claim restricts to x > 0, ensuring e - ln(x) is real. No branch cut ambiguity arises.

4. **Numerical overflow risk.** For representable positive floats, exp(e - ln(x)) stays within float64 range. Overflow would require x below the smallest positive float. The proof rests on exact symbolic algebra; numerics are supplementary.

## Conclusion

**Verdict: PROVED.** For every real x > 0, the triple nesting eml(1, eml(eml(1, x), 1)) equals ln(x). The proof unwinds the nesting layer by layer: the inner call produces e - ln(x) (A1), the middle call yields exp(e)/x (A2), and the outer call recovers ln(x) through the cancellation e - (e - ln(x)) (A3). Numerical evaluation at 6 points spanning x = 0.01 to x = 100 confirms agreement to machine epsilon (A4).

---

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