Information Emlfrom Recognition Identity Terminal Kills Log

The identity terminal

The declaration identity_terminal_kills_log proves a fact so elementary that a textbook might state it without proof: the natural logarithm of 1 is 0. In the framework's own terms, it shows that feeding the identity terminal, the number 1, into the logarithmic channel of a compiler gate annihilates that channel. The proof is a single simplification step in the machine-checked library of formal theorems.

The statement matters because of what it makes possible. The framework models an oriented recognition ledger, a discrete record of events with a direction, as having an additive coordinate. Exponentiation and logarithm map between that additive coordinate and the positive ratios that describe comparisons. A compiler gate, written eml x y = exp x - log y, combines these two channels. The theorem identity_terminal_kills_log, by establishing that log 1 = 0, is the key that lets the gate recover exponentiation: feeding the identity terminal to the logarithmic channel leaves eml x 1 = exp x. A further cancellation loop recovers the logarithm itself, and from those two, subtraction on positive ratios follows.

The theorem is deliberately narrow. It does not claim that the reciprocal cost function J, which satisfies J x = J x⁻¹, derives the gate. That would be false, because the reciprocal cost forgets orientation. The theorem operates at the compiler layer, before any reciprocal symmetrization. It also does not claim that the identity terminal is a physical object or that the gate is a physical process; it is a statement about the algebraic structure of the framework's model.

What the theorem establishes, precisely, is a bridge. It shows that a specific piece of the framework, the oriented exp-log compiler gate, is consistent and self-contained: from the identity terminal alone, the gate can reconstruct the elementary functions that the framework uses to describe ratios and differences. The proof is a certificate that this reconstruction is not an accident of notation but a consequence of the definitions.

/-- The identity terminal kills the logarithmic channel. -/
theorem identity_terminal_kills_log : Real.log 1 = 0 := by
  simp

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

What this page does not claim

The identity terminal is a physical object or a measurement device. The reciprocal cost function J alone derives the EML gate; the theorem explicitly notes J forgets orientation. The theorem establishes the full physical recognition-to-linking bridge; that remains open.

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: