eml_recovers_sub
plain-language theorem explainer
The theorem shows that the EML compiler gate recovers ordinary subtraction once its inputs are the logarithm of a positive real and the exponential of any real. Researchers verifying the oriented-recognition bridge to EML would cite it to confirm the additive structure of the ledger combiner. The proof is a direct unfolding of the eml definition followed by cancellation with the standard exp-log identities.
Claim. Let $x > 0$ and $y$ be real. Then the EML gate applied to the logarithm of $x$ and the exponential of $y$ equals the ordinary difference $x - y$.
background
The module formalizes the RS/EML bridge from an oriented recognition ledger that carries an additive log coordinate. Multiplicative-ratio chart maps are the exponential and logarithm; the oriented ledger combiner is subtraction, so the induced compiler gate is eml x y = exp x - log y. After reciprocal symmetrization the same data yields J(exp u) = cosh u - 1. Upstream results supply the J-cost and multiplicative-recognizer cost functions that underwrite the broader recognition ledger.
proof idea
The proof unfolds the definition of eml and rewrites using the cancellation lemmas Real.exp_log (under the positivity hypothesis) and Real.log_exp.
why it matters
This supplies the sub_recovery field inside emlFromRecognitionCert, which assembles the full compiler gate together with exp recovery, log recovery, and the reciprocal-cost quotient. It completes the compiler-layer claim that the oriented ledger combiner is subtraction before reciprocal symmetrization erases orientation. In the Recognition Science setting it supports the passage from oriented coordinates to the EML gate while preserving the additive structure required by the ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.