module module high

`IndisputableMonolith.Information.EMLFromRecognition`

This module defines Odrzywolek's EML operator as an oriented exp-log compiler gate built from ledger coordinates in the recognition framework. Information theorists and foundations researchers cite it when linking J-cost to thermodynamic and information operators. The module supplies a set of oriented ratio functions and recovery lemmas that establish the gate without external hypotheses.

claimThe EML operator is the oriented exp-log compiler gate satisfying orientedToRatio(eml(x)) = x, eml_recovers_exp, and reciprocal_cost_forgets_orientation, all expressed via the J-cost ledger.

background

The module imports IndisputableMonolith.Cost, which supplies the J-cost function J(x) = (x + x^{-1})/2 - 1 that underpins Recognition Science. It introduces orientedToRatio, orientedFromRatio, orientedSub, and the core eml operator together with identities such as oriented_compiler_gate_eq_eml and eml_recovers_log. The local setting is the information bridge that grounds minimum-description-length and thermodynamic operators in recognition ledger coordinates, as stated in the aggregator module's documentation.

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 feeds the parent Information aggregator, which collects the information-theoretic and thermodynamic foundation of Recognition Science. It realizes the EML operator from ledger coordinates and closes the link between the recognition composition law and exp-log identities. It touches the step that converts cost-based ratios into oriented information operators.

scope and limits

Does not derive EML from first principles outside the Cost module.
Does not address quantum or relativistic extensions of the gate.
Does not supply numerical validations or simulations.
Does not claim completeness of the full information bridge.

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