oriented_compiler_gate_eq_eml

formal source

  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 : ℝ) :
  77    eml 1 (eml (eml 1 x) 1) = Real.log x := by
  78  unfold eml
  79  simp only [Real.log_one, sub_zero]
  80  rw [Real.log_exp]
  81  ring
  82
  83/-- Once `exp` and `log` have been recovered, EML recovers subtraction on
  84positive ratios. -/