Information Emlfrom Recognition Eml Recovers Log

The exp-log gate

The exponential and logarithmic functions are normally introduced as inverses of each other, but they can also be recovered from a single two-input operation. The operation is exp(x) − log(y), where exp is the natural exponential function and log is the natural logarithm. This expression is known in some physics literature as the EML operator, named after the physicist Andrzej Odrzywolek. The framework's machine-checked library of formal theorems proves that this operator contains enough structure to reproduce both functions on its own.

The recovery works by feeding the number 1 into one channel. Setting y to 1 makes the logarithm term vanish, since log(1) = 0, leaving exp(x). Setting x to 1 and then nesting the operation twice produces log(x). The exact nesting is eml 1 (eml (eml 1 x) 1) = log(x). The framework also proves that the same operator recovers subtraction on positive numbers, and that it can produce the constant e by feeding 1 into both channels.

In Recognition Science, this result connects the framework's central object, the recognition ledger (a discrete record of events with a forced cost structure), to standard exponential and logarithmic coordinates. The framework models an oriented ledger, one that tracks direction, as having an additive coordinate. Exponentiation maps that coordinate to positive ratios, and logarithms map ratios back. The two-input compiler gate that arises from this chart is exactly the EML operator. The theorem eml_recovers_log is the formal statement that this gate can reconstruct the logarithm.

The framework is explicit about a limit of this result. The reciprocal cost function J(x) = (x + 1/x)/2 − 1, which is central elsewhere in the framework, satisfies J(x) = J(1/x) and therefore forgets orientation. The EML operator does not have this symmetry; it keeps the two channels separate. The theorem does not claim that the cost function J alone derives the EML gate. That would be false, since J cannot distinguish a ratio from its reciprocal. The recovery of log requires the oriented, pre-quotient structure.

What this means in practice is that the framework's recognition ledger, before any symmetrization, already contains the raw material for classical transcendental functions. The exponential and logarithm are not imported from outside; they emerge from the ledger's additive coordinate structure. The result is a compiler-layer bridge, not a claim about the physical origin of logarithms. It shows that a discrete record of events, when oriented and exponentiated, carries the full exp-log structure inside it.

/-- EML recovers exponentiation by feeding the identity terminal to the
logarithmic channel. -/
theorem eml_recovers_exp (x : ℝ) :
    eml x 1 = Real.exp x := by
  simp [eml]

/-- The cancellation loop that recovers logarithm from EML.  Over real Lean
this statement uses Lean's total `Real.log`; analytically it is the real
positive branch or the chosen complex branch in the paper. -/
theorem eml_recovers_log (x : ℝ) :
    eml 1 (eml (eml 1 x) 1) = Real.log x := by
  unfold eml
  simp only [Real.log_one, sub_zero]
  rw [Real.log_exp]
  ring

/-- Reciprocal cost forgets the orientation of the log coordinate. -/
theorem reciprocal_cost_forgets_orientation (u : ℝ) :
    Jlog u = Jlog (-u) := by
  have h := Jcost_symm (Real.exp_pos u)
  simpa [Jlog, Real.exp_neg] using h

/-- The EML compiler gate follows from oriented exp/log recognition data. -/
def emlFromRecognitionCert : EMLFromRecognitionCert where
  compiler_gate := oriented_compiler_gate_eq_eml
  exp_recovery := eml_recovers_exp
  log_recovery := eml_recovers_log
  sub_recovery := eml_recovers_sub
  reciprocal_cost_quotient := reciprocal_cost_forgets_orientation

What this page does not claim

The reciprocal cost function J alone derives the EML gate; the theorem requires the oriented, pre-quotient structure. The EML operator is physically fundamental; it is a compiler-layer bridge between recognition data and classical functions. The framework derives the existence of logarithms from nothing; it shows how they emerge from an oriented additive coordinate.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Information/EMLFromRecognition.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: