module module

`IndisputableMonolith.Information.EMLFromRecognition`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

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