module module moderate

`IndisputableMonolith.Information.EMLFromRecognition`

This module introduces Odrzywolek's EML operator as an oriented exp-log compiler gate built from ledger coordinates in the Cost framework. Information theorists and physicists deriving thermodynamic relations from recognition cost functions would cite these definitions when connecting J-cost to exponential and logarithmic maps. The module supplies a collection of oriented ratio conversions and recovery lemmas that establish the gate without external proof obligations beyond the imported Cost primitives.

claimThe EML operator is the oriented exp-log compiler gate $E$ satisfying $E(xy) + E(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$ together with the oriented ratio maps that recover $\exp$ and $\log$ from ledger coordinates.

background

The module sits inside the Information domain and imports the Cost module to access J-cost and related ledger operations. Its sibling definitions implement orientedToRatio, orientedFromRatio, orientedSub, and the compiler gate itself, all expressed in terms of the Recognition Composition Law. The downstream Information aggregator describes the module as supplying the oriented exp-log compiler gate from ledger coordinates that supports the minimum-description-length grounding in J-cost.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the oriented exp-log compiler gate that the parent Information aggregator uses to connect ledger coordinates to information-theoretic and thermodynamic foundations. It directly populates the EMLFromRecognition component listed in the aggregator's module inventory, enabling downstream use of oriented recovery lemmas such as eml_recovers_exp and reciprocal_cost_forgets_orientation.

scope and limits

Does not derive numerical values for physical constants.
Does not extend the gate to quantum or relativistic regimes.
Does not prove uniqueness of the EML representation.
Does not supply executable code or simulation routines.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Information module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import

declarations in this module (16)

def eml L34
def orientedToRatio L38
def orientedFromRatio L42
def orientedSub L46
def orientedCompilerGate L50
theorem oriented_compiler_gate_eq_eml L54
theorem identity_terminal_kills_log L59
theorem eml_recovers_exp L64
theorem eml_recovers_e L69
theorem eml_recovers_log L76
theorem eml_recovers_sub L85
theorem reciprocal_cost_forgets_orientation L91
theorem eml_keeps_oriented_channels L98
structure EMLFromRecognitionCert L106
def emlFromRecognitionCert L119
theorem eml_from_recognition_cert_holds L126