eml_keeps_oriented_channels
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not derive EML solely from the reciprocal cost function J.
- Does not address physical units or constants such as alpha or G.
- Does not claim preservation of orientation after reciprocal symmetrization.
- Does not connect directly to spatial dimensions or the eight-tick octave.
formal statement (Lean)
98theorem eml_keeps_oriented_channels (x : ℝ) :
99 eml x 1 = orientedToRatio x ∧
100 orientedFromRatio x = Real.log x := by
proof body
Term-mode proof.
101 constructor
102 · simp [eml, orientedToRatio]
103 · rfl
104
105/-- A compact certificate for the theorem-grade RS/EML bridge. -/