Lean 4 formalization of arXiv:2603.21852 — All elementary functions from a single binary operator eml(x,y) = exp(x) - ln(y) - View it on GitHub