Information Emlfrom Recognition Eml From Recognition Cert Holds

The EML bridge

The EML operator, named after its origin in Odrzywolek's work, is defined as eml x y = exp(x) - log(y). In plain terms, it takes two numbers: exponentiates the first, takes the natural logarithm of the second, and subtracts. This makes it a kind of compiler gate, a small circuit that transforms two inputs into one output.

The Recognition Science framework models reality as maintaining a ledger, a discrete record of recognition events. Before any symmetrization, this ledger has an oriented, additive coordinate: events can be assigned a real number that adds when composed. The certificate proves that this oriented structure maps directly onto the EML gate. The exponential function lifts additive coordinates to positive ratios, the logarithm projects back, and subtraction combines them. The theorem oriented_compiler_gate_eq_eml states this identity exactly.

From this foundation, the certificate shows EML can recover the basic operations of arithmetic. Feeding the identity terminal 1 to the logarithmic channel recovers exponentiation, as eml_recovers_exp proves. A cancellation loop recovers the logarithm, and with both functions in hand, EML recovers subtraction on positive ratios. The certificate packages these results into a single structure, EMLFromRecognitionCert, and the theorem eml_from_recognition_cert_holds asserts this structure exists.

The declaration is careful about what it does not claim. The reciprocal cost function J, which satisfies J(x) = J(1/x), forgets orientation: the theorem reciprocal_cost_forgets_orientation shows Jlog u = Jlog (-u). This symmetry means J alone cannot distinguish between a forward and a backward direction, so it cannot derive the oriented EML gate. The certificate explicitly builds the bridge from the oriented ledger, not from the symmetrized cost. It is a compiler-layer result, not a claim about the fundamental cost function.

What this establishes is a precise, machine-checked connection between the framework's foundational concepts and a concrete computational operator. It shows that the EML gate is not an arbitrary choice but follows from the structure of oriented recognition. This gives the operator a firm foundation within the framework, while leaving the deeper question of how the symmetrized cost relates to oriented processes as a separate matter.

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

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

/-- 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 function J alone does not derive the EML gate. The certificate does not claim that the EML gate is the only possible compiler gate. The certificate does not address the physical interpretation of the oriented ledger.

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: