eml_keeps_oriented_channels
plain-language theorem explainer
The theorem shows that the EML operator at y=1 recovers the forward exponential map while the logarithm projection on ratios stays independently addressable. Workers on the oriented Recognition-to-EML compiler layer cite this when separating exp and log channels before J-symmetrization. The term proof splits the conjunction and simplifies the definitions directly.
Claim. Let $\mathrm{eml}(x,y) := \exp(x) - \log(y)$. For any real $x$, $\mathrm{eml}(x,1) = \exp(x)$ while the oriented logarithm projection satisfies $\log(x) = \log(x)$.
background
The module formalizes the honest RS/EML bridge. It does not claim that the reciprocal cost J alone derives the EML gate, since J x = J x^{-1} forgets orientation. The claim proved here is compiler-layer: before reciprocal quotienting, an oriented recognition ledger has an additive log coordinate; the multiplicative-ratio chart maps are exp and log; the oriented ledger combiner is subtraction; therefore the induced two-input compiler gate is eml x y = exp x - log y. The same exp/log data, after reciprocal symmetrization, gives J(exp u) = cosh u - 1.
Key definitions: eml (x y : ℝ) := Real.exp x - Real.log y (Odrzywolek's EML operator read as oriented exp-log compiler gate); orientedToRatio (u : ℝ) := Real.exp u (oriented additive ledger coordinates lift to positive ratios by exponentiation); orientedFromRatio (x : ℝ) := Real.log x (positive ratios project back to additive ledger coordinates by logarithm).
proof idea
Term-mode proof. Constructor splits the conjunction into two goals. The first goal simplifies directly via simp [eml, orientedToRatio]. The second goal is discharged by rfl.
why it matters
This declaration fills the compiler-layer claim stated in the module documentation. It isolates the oriented exp and log channels before reciprocal symmetrization (the step that produces J(exp u) = cosh u - 1). The result sits upstream of any use of the eight-tick octave or D = 3 and supports the separation of forward and backward channels in the Recognition Science framework. No downstream theorems are listed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.