eml_keeps_oriented_channels
plain-language theorem explainer
The declaration shows that the EML operator applied to a real number x and 1 recovers the oriented exponential map, while the oriented projection from ratio is the natural logarithm. Researchers formalizing the Recognition Science to EML bridge would cite this result to confirm preservation of oriented channels before symmetrization. The proof is a direct algebraic simplification using the definitions of the EML gate and the oriented maps.
Claim. For any real number $x$, the EML operator satisfies $eml(x,1)=e^x$ and the oriented map from positive ratio to additive coordinate is the natural logarithm, $orientedFromRatio(x)=log x$.
background
This module formalizes the RS/EML bridge at the compiler layer. It emphasizes that the reciprocal cost J alone cannot derive the EML gate because J(x)=J(x^{-1}) forgets orientation. Instead, before reciprocal quotienting, the oriented recognition ledger carries an additive log coordinate. The multiplicative-ratio charts are the exponential and logarithm maps, the ledger combiner is subtraction, and the induced gate is eml(x,y):=exp(x)-log(y). After symmetrization this yields J(exp(u))=cosh(u)-1. The key definitions are eml(x,y)=Real.exp(x)-Real.log(y), orientedToRatio(u)=Real.exp(u), and orientedFromRatio(x)=Real.log(x).
proof idea
The proof applies constructor to split the conjunction into two goals. The first goal simplifies immediately using the definitions of eml and orientedToRatio. The second goal holds by reflexivity because orientedFromRatio is defined to be the natural logarithm.
why it matters
This theorem anchors the compiler-layer claim in the EMLFromRecognition module that the oriented ledger induces the EML gate eml(x,y)=exp(x)-log(y). It supports the distinction between oriented and reciprocal costs central to the Recognition Science framework, particularly the J-uniqueness property where J(x)=J(x^{-1}). No parent theorems are listed in the used-by graph, but it underpins sibling results such as eml_recovers_exp and eml_recovers_log within the same module. It touches the open question of how the oriented coordinates interface with the full forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.