  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`. -/
  69theorem eml_recovers_e :
  70    eml 1 1 = Real.exp 1 := by
  71  simp [eml]
  72
  73/-- The cancellation loop that recovers logarithm from EML.  Over real Lean
  74this statement uses Lean's total `Real.log`; analytically it is the real
  75positive branch or the chosen complex branch in the paper. -/
  76theorem eml_recovers_log (x : ℝ) :

papers checked against this theorem

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