eml
The eml definition supplies Odrzywolek's EML operator as the oriented exp-log compiler gate. Researchers formalizing the Recognition Science to EML bridge cite this gate when recovering exponentiation, logarithm, and oriented subtraction from an additive ledger coordinate. It is introduced by a direct one-line definition that subtracts the logarithm of the second argument from the exponential of the first.
claimThe oriented compiler gate is defined by $EML(x,y) := e^x - log(y)$ for real numbers $x,y$.
background
The EMLFromRecognition module formalizes the RS/EML bridge at the compiler layer. An oriented recognition ledger carries an additive log coordinate before reciprocal quotienting. The multiplicative-ratio chart maps are exp and log, while the oriented ledger combiner is subtraction. This produces the two-input gate eml x y = exp x - log y. The module documentation states that the reciprocal cost J alone cannot derive the EML gate because J(x) = J(x^{-1}) forgets orientation; the same data after symmetrization yields J(exp u) = cosh u - 1.
proof idea
The definition is a direct one-line assignment of Real.exp x minus Real.log y.
why it matters in Recognition Science
This definition supplies the core operator for the EMLFromRecognitionCert structure, which certifies the RS/EML bridge via compiler_gate, exp_recovery, and log_recovery axioms. It fills the compiler-layer claim in the module's formalization of the honest RS/EML bridge. Downstream results such as eml_recovers_exp and eml_recovers_log recover the exponential and logarithmic functions directly from the gate, while eml_keeps_oriented_channels shows that forward and reverse channels remain separately addressable. The construction preserves orientation before the J-uniqueness step of the forcing chain.
scope and limits
- Does not derive the EML gate from the reciprocal cost J alone.
- Does not address orientation forgetting that occurs under reciprocal symmetrization.
- Does not extend the recovery statements beyond the real positive branch.
- Does not claim a direct physical derivation of EML from RS without the oriented ledger.
Lean usage
theorem eml_recovers_exp (x : ℝ) : eml x 1 = Real.exp x := by simp [eml]formal statement (Lean)
34def eml (x y : ℝ) : ℝ :=
proof body
Definition body.
35 Real.exp x - Real.log y
36
37/-- Oriented additive ledger coordinates lift to positive ratios by exponentiation. -/