module module high

`IndisputableMonolith.Information.EMLFromRecognition`

The EMLFromRecognition module introduces Odrzywolek's EML operator as an oriented exp-log compiler gate built from ledger coordinates. It extends the Cost module with definitions for oriented ratios, subtractions, and recovery identities. Information theorists studying thermodynamic foundations cite this for bridging J-cost to exp-log operations. The module contains a collection of definitions and equalities without a single central theorem.

claimThe EML operator is realized as the oriented exp-log compiler gate from ledger coordinates, satisfying recovery of the exponential map, base $e$, logarithm, and subtraction via oriented ratios and costs.

background

Recognition Science derives physics from a functional equation involving the J-cost function. This module sits in the Information domain and imports the Cost module to access those cost definitions. It provides the EML operator, read as an oriented exp-log compiler gate from ledger coordinates, as described in the module documentation.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

This module feeds the IndisputableMonolith.Information aggregator, which collects the information-theoretic and thermodynamic foundation of Recognition Science. It fills the role of providing the oriented exp-log compiler gate, enabling connections between cost structures and classical exp-log operations. The module touches the information bridge in the Recognition framework.

scope and limits

Does not claim independence from the Cost module import.
Does not address the forcing chain T0 to T8 or spatial dimensions.
Does not compute numerical constants such as the fine structure constant.
Does not include mass formulas or phi-ladder constructions.

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