EML Tree Builder

What this does

The compiler implements the seven structural macros from SI §2.1 of the paper:

exp(z)  ↦  eml(z, 1)
ln(z)   ↦  eml(1, exp(eml(1, z)))    = eml(1, eml(eml(1, z), 1))
x − y   ↦  eml(ln(x), exp(y))
−z      ↦  ln(1) − z
x + y   ↦  x − (−y)
1/z     ↦  exp(−ln(z))
x · y   ↦  exp(ln(x) + ln(y))

Plus derived macros for x², x/2, (x+y)/2, √x, x^y, log_b y, hypot(x, y), σ(x), sinh, cosh, tanh, arsinh, arcosh, artanh.

Trigonometric primitives are built from the complex EML grammar (EMLTermℂ). The closed constants i and π are shown as labelled leaves with their actual K-counts (their internal structure — the EMLRealizationℂ closure machinery — is hidden so the canvas stays legible). The result of a trig compile is read via .re or .im projection, shown above the metric tiles.

When an expression contains any trig sub-expression, the entire compile switches to the complex grammar (EMLTermℂ): all additions are routed through the 9-node mkAdd_ℂ ADDsafe pattern, and any trig call with a non-variable argument is realised via Path C′ subst0 — the witness is built with a fresh placeholder variable and the caller's compiled argument is substituted in. So log(sin(1+x²)) now compiles end-to-end. The grammar pill above the metric tiles tells you which pipeline (real or complex) was used.

How tree sizes here compare to the K_count_* theorems and the DASHBOARD. The Lean artefact uses three different witness sources mixed together, only one of which this tool reproduces:

• Direct compositional macros for log, exp, sub, mul, div, sq, sqrt, σ, sinh, cosh, tanh — the tool reproduces these exactly, so K-counts match the formalization (e.g. log(x) = K 7 on both sides).
• Verbatim Euler-bridge witnesses for the trig family (cos K 1273, tanCore K 2817, arctan K 1303, etc.) — these are copied directly from the formalization, so K-counts also match.
• Hand-tuned closed-constant packages in the formalization for π and i (EMLRealizationℂ, K 233 / K 407). The web tool uses a much shorter pedagogical placeholder (π = K 39) that doesn't actually evaluate — it requires log(0) in the real-fragment chain. This is a deliberate compromise: showing the closure machinery in the browser would dominate the canvas.
• Full structural-compiler output (F36Expr.translate? → compile) in the formalization for logb, div, mul, pow, hypot, arcsin (narrow). Those K-counts run into the millions because the compiler unrolls every operation uniformly. This tool shortcuts via direct compositional macros instead, so e.g. logb(x, y) here is K 77 whereas the dashboard reports K 9 929 087 — same function, same domain, very different syntax tree.

Bottom line: there is one mathematical artefact (the Lean proof). This tool implements a clean subset that agrees with the formal artefact for the majority of primitives, with two explicit divergence points (closed constants and the structural-compiler binaries) that are documented above.

All paper / SI / repository links are listed in the References panel at the top of the page.