Information Emlfrom Recognition Oriented Compiler Gate Eq Eml

The oriented gate

The EML operator, written eml and defined as exp(x) − log(y), is a two-input real-valued function. It appears in the work of Odrzywolek as a candidate information-processing gate. The Recognition Science library contains a theorem, oriented_compiler_gate_eq_eml, that establishes a precise identity: when an oriented recognition ledger (a discrete record of events with a direction) is given additive coordinates, and those coordinates are converted to positive ratios by exponentiation and back by logarithm, then the natural combiner, subtraction, induces exactly the EML operation. The proof is a direct computation, a reflexivity step in the machine-checked library of formal theorems.

The theorem is a compiler-layer claim, not a physical derivation. It does not say that the framework's reciprocal cost function J, which satisfies J(x) = (x + 1/x)/2 − 1, produces EML. That would be false, because J is symmetric under x ↦ 1/x and therefore forgets orientation. The theorem instead starts from an oriented ledger, before any reciprocal symmetrization, and shows that its natural arithmetic yields EML. The library also proves supporting facts: feeding the identity terminal 1 to the logarithmic channel recovers exponentiation, a cancellation loop recovers logarithm, and the gate keeps the forward exp channel and the log channel separately addressable.

What the declaration does not claim is as important as what it proves. It does not claim that EML is the unique gate forced by the framework's axioms, nor that the reciprocal cost function alone can derive it. It does not claim any empirical or physical status for EML beyond its algebraic identity. The theorem is a statement about a specific construction: given oriented exp/log data and subtraction, the induced two-input gate is EML. That is the full scope of the result.

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

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

What this page does not claim

The reciprocal cost function J alone derives the EML gate. The EML operator is the unique gate forced by the framework's axioms. The theorem assigns any empirical or physical status to EML beyond its algebraic identity.

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: