`orientedToRatio`

definition

show as: view math explainer →

module: IndisputableMonolith.Information.EMLFromRecognition
domain: Information
line: 38 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Information.EMLFromRecognition on GitHub at line 38.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  35  Real.exp x - Real.log y
  36
  37/-- Oriented additive ledger coordinates lift to positive ratios by exponentiation. -/
  38def orientedToRatio (u : ℝ) : ℝ :=
  39  Real.exp u
  40
  41/-- Positive ratios project back to additive ledger coordinates by logarithm. -/
  42def orientedFromRatio (x : ℝ) : ℝ :=
  43  Real.log x
  44
  45/-- The oriented ledger combiner before reciprocal symmetrization. -/
  46def orientedSub (a b : ℝ) : ℝ :=
  47  a - b
  48
  49/-- The compiler gate induced by the oriented exp/log chart and subtraction. -/
  50def orientedCompilerGate (x y : ℝ) : ℝ :=
  51  orientedSub (orientedToRatio x) (orientedFromRatio y)
  52
  53/-- The induced oriented compiler gate is exactly EML. -/
  54theorem oriented_compiler_gate_eq_eml (x y : ℝ) :
  55    orientedCompilerGate x y = eml x y := by
  56  rfl
  57
  58/-- The identity terminal kills the logarithmic channel. -/
  59theorem identity_terminal_kills_log : Real.log 1 = 0 := by
  60  simp
  61
  62/-- EML recovers exponentiation by feeding the identity terminal to the
  63logarithmic channel. -/
  64theorem eml_recovers_exp (x : ℝ) :
  65    eml x 1 = Real.exp x := by
  66  simp [eml]
  67
  68/-- EML recovers the constant `e` from the terminal `1`. -/

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.