Information Emlfrom Recognition

The EML gate

EML is a two-input operation on real numbers defined as eml x y = exp x - log y. It combines the exponential function and the natural logarithm into one expression, so it can both create and extract information in a single step. The operation appears in the work of Andrzej Odrzywolek, where it acts as an elementary gate for processing information.

The operation has a clean algebraic structure. Feeding the number 1 into the logarithmic channel leaves only the exponential: eml x 1 = exp x. A more elaborate cancellation loop recovers the logarithm: eml 1 (eml (eml 1 x) 1) = log x. Once both functions are available, the operation also recovers subtraction on positive numbers: eml (log x) (exp y) = x - y. These identities show that EML is not an arbitrary mixture of functions but a self-contained system that can express the basic building blocks of arithmetic.

The machine-checked library of formal theorems proves a stronger claim: EML is not merely defined by hand, it is forced by the structure of an oriented recognition ledger. In this framework, a ledger is a discrete record of events, and recognition is the act of assigning a cost to an event. Before any symmetrization is applied, the ledger carries an oriented coordinate: positive ratios are represented by their logarithm, and addition in the ledger becomes exponentiation. The natural combiner for two such oriented entries is subtraction, and composing these pieces yields exactly the EML gate.

The library proves this bridge as a theorem, not a conjecture. The central certificate, EMLFromRecognitionCert, packages five facts: the compiler gate equals EML, exponentiation is recovered, logarithm is recovered, subtraction is recovered, and the reciprocal cost function J is symmetric under sign flip, meaning it forgets orientation. The last point is the key distinction: the reciprocal cost J(x) = (x + 1/x)/2 - 1 treats x and 1/x as the same, so it cannot see direction. EML keeps that directional data, which is why it can serve as a compiler gate while J cannot.

The practical consequence is that information processing, in this account, does not need to be bolted onto physics as a separate ingredient. The same structure that produces the cost function also produces a working gate for combining and separating information. The gate is not derived from the cost function alone, since J forgets orientation; it comes from the fuller oriented ledger that sits underneath. This gives the framework a concrete answer to where basic computational operations come from: they are already present in the ledger before symmetry reduction.

/-- Odrzywolek's EML operator, read as an oriented exp-log compiler gate. -/
def eml (x y : ℝ) : ℝ :=
  Real.exp x - Real.log y

/-- The induced oriented compiler gate is exactly EML. -/
theorem oriented_compiler_gate_eq_eml (x y : ℝ) :
    orientedCompilerGate x y = eml x y := by
  rfl

/-- 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

theorem eml_from_recognition_cert_holds : Nonempty EMLFromRecognitionCert :=
  ⟨emlFromRecognitionCert⟩

What this page does not claim

The reciprocal cost J alone derives the EML gate, since J forgets orientation. The EML gate is the only possible information-processing gate in the framework. The oriented ledger has a direct physical interpretation beyond its formal definition.

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: