eml_recovers_e
plain-language theorem explainer
The oriented compiler gate at unit inputs recovers the base of the natural exponential. Researchers on oriented recognition ledgers cite this to confirm that the additive log coordinate reduces to the standard exponential at the terminal point. The proof is a one-line simplification that unfolds the gate definition and uses log(1) = 0.
Claim. Let the oriented compiler gate be defined by $eml(x,y) := e^x - log(y)$. Then $eml(1,1) = e$.
background
The module establishes the RS/EML bridge at the compiler layer. Before reciprocal quotienting, an oriented recognition ledger carries an additive log coordinate whose multiplicative-ratio charts are the exponential and logarithm maps. The oriented ledger combiner is subtraction, so the induced two-input gate is $eml(x,y) := exp(x) - log(y)$. After reciprocal symmetrization this yields the J-cost relation $J(exp u) = cosh u - 1$.
proof idea
The proof is a one-line wrapper that applies simplification on the gate definition, reducing $exp(1) - log(1)$ directly to $exp(1)$ via the fact that $log(1) = 0$.
why it matters
This result anchors the module claim that the multiplicative-ratio charts are exp and log before any reciprocal symmetrization. It supports the downstream recovery statements for exp, log, and subtraction in the same file and aligns with the oriented ledger construction that precedes the J-cost formula $J(exp u) = cosh u - 1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.