eml_recovers_log
plain-language theorem explainer
The theorem establishes that a nested application of the EML operator recovers the natural logarithm on the reals. Researchers formalizing the oriented recognition to EML compiler bridge cite it to close the log-recovery direction. The proof is a short term-mode reduction that unfolds the gate definition three times and cancels via exp-log identities.
Claim. For any real number $x$, let $eml(u,v) := e^u - log v$. Then $eml(1, eml(eml(1,x),1)) = log x$.
background
The module formalizes the RS/EML bridge at the compiler layer. An oriented recognition ledger carries an additive log coordinate; the multiplicative-ratio charts are the maps exp and log; the oriented ledger combiner is subtraction. The induced two-input gate is therefore defined by eml x y = exp x - log y. This sits before reciprocal symmetrization, which produces the J-cost satisfying J(exp u) = cosh u - 1. The upstream eml definition supplies the concrete operator used in the statement.
proof idea
The term proof unfolds eml three times, applies simp with Real.log_one and sub_zero, rewrites the inner exp-log pair via Real.log_exp, and closes with ring normalization on the resulting expression.
why it matters
This supplies the log_recovery component of the EMLFromRecognitionCert certificate, confirming that the compiler gate follows from oriented exp/log recognition data. It completes one half of the exp/log recovery loop in the module, consistent with the additive log coordinate on the oriented ledger before the reciprocal quotient that forgets orientation and yields J.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.