RequestProject_Identities.lean

import RequestProject.Defs

/-!
# EML Identities: Proving the core argument

This file proves that the EML operator `eml(x, y) = exp(x) - log(y)` together with the
constant `1` generates all standard elementary functions, following the constructive
proof from the paper "All elementary functions from a single operator" by
Andrzej Odrzywolek (arXiv:2603.21852v2).

## Proof structure

The proof proceeds in stages, mirroring the paper's "bootstrapping phylogenetic tree" (Fig. 1):

1. **exp** and **e** from `eml` (trivial)
2. **ln** from `eml` (main technical lemma)
3. **Subtraction** from `{eml, exp, ln}`
4. **Negation** and **addition** from subtraction
5. **Multiplication** and **division** from `exp` and `ln`
6. **Constants** (0, π, i) and **trigonometric functions** via Euler's formula
-/

open Complex

set_option maxHeartbeats 800000

noncomputable section

/-! ### Stage 1: exp and e from EML -/

/-- **Core identity**: `eml(x, 1) = exp(x)`.
    The logarithm term vanishes since `log(1) = 0`. -/
theorem eml_one_right (x : ℂ) : eml x 1 = Complex.exp x := by
  simp [eml, Complex.log_one]

/-- The EML tree for `exp` evaluates correctly. -/
theorem EMLTree.expTree_correct (x : ℂ) :
    EMLTree.expTree.eval (fun _ => x) = Complex.exp x := by
  simp [EMLTree.expTree, EMLTree.eval, eml_one_right]

/-- The EML tree for `e` evaluates correctly: `eml(1, 1) = exp(1)`. -/
theorem EMLTree.constE_correct :
    EMLTree.constE.eval Fin.elim0 = Complex.exp 1 := by
  simp [EMLTree.constE, EMLTree.eval, eml_one_right]

/-- The exp tree has depth 1 (matching Table 4 of the paper). -/
theorem EMLTree.expTree_depth : EMLTree.expTree.depth = 1 := by rfl

/-- The exp tree has size K = 3 (matching Table 4 of the paper). -/
theorem EMLTree.expTree_size : EMLTree.expTree.size = 3 := by rfl

/-- The ln tree has depth 3 (matching Table 4 of the paper). -/
theorem EMLTree.lnTree_depth : EMLTree.lnTree.depth = 3 := by rfl

/-- The ln tree has size K = 7 (matching Table 4 of the paper). -/
theorem EMLTree.lnTree_size : EMLTree.lnTree.size = 7 := by rfl

/-! ### Stage 2: ln from EML

The key identity is: `ln(x) = eml(1, eml(eml(1, x), 1))`.

The proof proceeds in three steps:
- Step A: `eml(1, x) = e - log(x)` (inner application)
- Step B: `eml(e - log(x), 1) = exp(e - log(x)) = exp(e) / x` (middle)
- Step C: `eml(1, exp(e)/x) = e - log(exp(e)/x) = e - (e - log(x)) = log(x)` (outer)
-/

/-
Step A: `eml(1, ↑x) = exp(1) - log(↑x)` for positive real x.
    When x > 0, we have `log(↑x) = ↑(Real.log x)`.
-/
theorem eml_one_ofReal_pos (x : ℝ) (hx : 0 < x) :
    eml 1 (↑x : ℂ) = ↑(Real.exp 1) - ↑(Real.log x) := by
  norm_num [ eml ];
  rw [ Complex.ofReal_log hx.le ]

/-
The intermediate value `exp(1) - log(↑x)` is real for positive real x,
    hence its imaginary part is 0.
-/
lemma eml_one_ofReal_im_eq_zero (x : ℝ) (hx : 0 < x) :
    (eml 1 (↑x : ℂ)).im = 0 := by
  unfold eml; norm_num;
  norm_num [ Real.exp_ne_zero, Complex.log_im ];
  norm_num [ Complex.exp_im, Complex.arg ];
  positivity

/-
Step B: The middle application gives `exp(e) / x`.
-/
theorem eml_middle_step (x : ℝ) (hx : 0 < x) :
    eml (eml 1 (↑x : ℂ)) 1 = ↑(Real.exp (Real.exp 1) / x) := by
  unfold eml; norm_num [ Complex.ext_iff, Real.exp_pos ];
  norm_num [ Complex.exp_re, Complex.exp_im, Complex.log_re, Complex.log_im, Real.exp_sub, Real.exp_log hx ];
  norm_num [ Complex.arg_ofReal_of_nonneg hx.le ]

/-
Key fact: `exp(e)/x > 0` for `x > 0`.
-/
lemma exp_exp_one_div_pos (x : ℝ) (hx : 0 < x) :
    0 < Real.exp (Real.exp 1) / x := by
  positivity

/-
**Main Theorem (ln from EML)**: For real `x > 0`,
    `eml(1, eml(eml(1, x), 1)) = log(x)`.

    This is the key technical result: the natural logarithm can be
    expressed as a depth-3 EML tree. Together with `eml(x, 1) = exp(x)`,
    this establishes that `{eml, 1}` generates the exp-log pair.
-/
theorem eml_ln (x : ℝ) (hx : 0 < x) :
    eml 1 (eml (eml 1 (↑x : ℂ)) 1) = ↑(Real.log x) := by
  -- Substitute the result of the middle application into the outer eml operation.
  have h_outer : eml 1 (↑(Real.exp (Real.exp 1) / x)) = ↑(Real.exp 1) - ↑(Real.log (Real.exp (Real.exp 1) / x)) := by
    convert eml_one_ofReal_pos ( Real.exp ( Real.exp 1 ) / x ) ( by positivity ) using 1;
  convert h_outer using 1;
  · rw [ eml_middle_step x hx ];
  · rw [ Real.log_div ( by positivity ) ( by positivity ), Real.log_exp ] ; norm_num

/-- The EML tree for `ln` evaluates correctly on positive reals. -/
theorem EMLTree.lnTree_correct (x : ℝ) (hx : 0 < x) :
    EMLTree.lnTree.eval (fun _ => (↑x : ℂ)) = ↑(Real.log x) := by
  simp only [EMLTree.lnTree, EMLTree.eval]
  exact eml_ln x hx

/-! ### Stage 3: Arithmetic from EML

Once we have `exp` and `log`, we can recover arithmetic operations
through the EML operator:
- `eml(log(x), exp(y)) = exp(log(x)) - log(exp(y)) = x - y`
- Other operations follow from compositions.
-/

/-
**Subtraction from EML**: `eml(log(x), exp(y)) = x - y`.
    Requires `x ≠ 0` (for `exp(log(x)) = x`) and `Im(y) ∈ (-π, π]`
    (for `log(exp(y)) = y`).
-/
theorem eml_sub (x y : ℂ) (hx : x ≠ 0)
    (hy₁ : -Real.pi < y.im) (hy₂ : y.im ≤ Real.pi) :
    eml (Complex.log x) (Complex.exp y) = x - y := by
  unfold eml;
  rw [ Complex.exp_log hx, Complex.log_exp ] <;> aesop

/-
**One minus x**: For real `x`, `eml(0, exp(↑x)) = 1 - ↑x`.
    Here `0` serves as `log(1)`.
-/
theorem eml_one_minus (x : ℝ) :
    eml 0 (Complex.exp (↑x : ℂ)) = (↑(1 - x) : ℂ) := by
  unfold eml; norm_num;
  rw [ Complex.log_exp ] <;> norm_num;
  · positivity;
  · positivity

/-
**Negation from EML**: For `x ≠ 1`, `eml(log(1 - x), exp(1)) = -x`.
    Proof: `exp(log(1 - x)) - log(exp(1)) = (1 - x) - 1 = -x`.
-/
theorem eml_neg (x : ℂ) (hx : x ≠ 1)  :
    eml (Complex.log (1 - x)) (Complex.exp 1) = -x := by
  convert eml_sub ( 1 - x ) 1 _ _ using 1 <;> norm_num;
  · exact Or.inl Real.pi_pos.le;
  · exact sub_ne_zero_of_ne hx.symm;
  · positivity

/-- **Addition via double negation**: For `x ≠ 0` and appropriate conditions,
    `x + y` can be recovered from subtraction and negation:
    `x + y = x - (-y)`. -/
theorem add_from_sub_neg (x y : ℂ) : x + y = x - (-y) := by ring

/-
**Multiplication from exp-log**: For `x, y ≠ 0` with argument condition,
    `exp(log(x) + log(y)) = x * y`.
-/
theorem mul_from_exp_log (x y : ℂ) (hx : x ≠ 0) (hy : y ≠ 0)
    (harg : x.arg + y.arg ∈ Set.Ioc (-Real.pi) Real.pi) :
    Complex.exp (Complex.log x + Complex.log y) = x * y := by
  rw [ Complex.exp_add, Complex.exp_log hx, Complex.exp_log hy ]

/-
**Division from exp-log**: For `x, y ≠ 0`,
    `exp(log(x) - log(y)) = x / y` under appropriate branch conditions.
-/
theorem div_from_exp_log (x y : ℂ) (hx : x ≠ 0) (hy : y ≠ 0)
    (harg : x.arg + (-y).arg ∈ Set.Ioc (-Real.pi) Real.pi) :
    Complex.exp (Complex.log x - Complex.log y) = x / y := by
  rw [ Complex.exp_sub, Complex.exp_log hx, Complex.exp_log hy ]

/-
**Squaring from exp-log**: For `x ≠ 0` with `2 * x.arg ∈ (-π, π]`,
    `exp(2 * log(x)) = x ^ 2`.
-/
theorem sq_from_exp_log (x : ℂ) (hx : x ≠ 0)
    (harg : x.arg + x.arg ∈ Set.Ioc (-Real.pi) Real.pi) :
    Complex.exp (2 * Complex.log x) = x ^ 2 := by
  rw [ two_mul, Complex.exp_add, Complex.exp_log hx ];
  ring

/-
**Real multiplication (simpler version)**: For positive reals,
    `exp(log(x) + log(y)) = x * y` without branch cut issues.
-/
theorem mul_from_exp_log_real (x y : ℝ) (hx : 0 < x) (hy : 0 < y) :
    Real.exp (Real.log x + Real.log y) = x * y := by
  rw [ Real.exp_add, Real.exp_log hx, Real.exp_log hy ]

/-
**Real division (simpler version)**: For positive reals,
    `exp(log(x) - log(y)) = x / y`.
-/
theorem div_from_exp_log_real (x y : ℝ) (hx : 0 < x) (hy : 0 < y) :
    Real.exp (Real.log x - Real.log y) = x / y := by
  rw [ Real.exp_sub, Real.exp_log hx, Real.exp_log hy ]

/-
**Power from exp-log**: For positive real base,
    `exp(y * log(x)) = x ^ y`.
-/
theorem pow_from_exp_log_real (x : ℝ) (y : ℝ) (hx : 0 < x) :
    Real.exp (y * Real.log x) = x ^ y := by
  rw [ Real.rpow_def_of_pos hx, mul_comm ]

/-
**Square root from exp-log**: For positive real x,
    `exp(log(x) / 2) = √x`.
-/
theorem sqrt_from_exp_log_real (x : ℝ) (hx : 0 < x) :
    Real.exp (Real.log x / 2) = Real.sqrt x := by
  rw [ Real.sqrt_eq_rpow, Real.rpow_def_of_pos hx ] ; ring

/-! ### Stage 4: Constants from EML -/

/-
**Zero from EML**: `eml(1, eml(eml(1, 1), 1)) = 0`.
    This is the ln tree evaluated at 1: `ln(1) = 0`.
-/
theorem eml_const_zero :
    eml 1 (eml (eml 1 1) 1) = 0 := by
  convert eml_ln 1 zero_lt_one using 1;
  norm_num

/-- The EML tree for zero evaluates correctly. -/
theorem EMLTree.constZero_correct :
    EMLTree.constZero.eval Fin.elim0 = 0 := by
  simp only [EMLTree.constZero, EMLTree.eval]
  exact eml_const_zero

/-
**e - 1 from EML**: `eml(1, eml(1, 1)) = e - 1`.
-/
theorem eml_e_minus_one :
    eml 1 (eml 1 1) = Complex.exp 1 - 1 := by
  unfold eml; norm_num;
  rw [ Complex.log_exp ];
  · norm_num [ Real.pi_pos ];
  · norm_num ; linarith [ Real.pi_gt_three ]

/-
**exp(e) from EML**: `eml(eml(1, 1), 1) = exp(e)`.
-/
theorem eml_exp_e :
    eml (eml 1 1) 1 = Complex.exp (Complex.exp 1) := by
  unfold eml; aesop;

/-
**1 - e from EML**: `eml(0, eml(eml(1, 1), 1)) = 1 - e`.
    Using that `0 = log(1)` and the zero tree.
-/
theorem eml_one_minus_e :
    eml 0 (eml (eml 1 1) 1) = 1 - Complex.exp 1 := by
  convert eml_one_minus ( Complex.exp 1 |> Complex.re ) using 1;
  · norm_num [ Complex.ext_iff, Complex.exp_re, Complex.exp_im, Complex.log_re, Complex.log_im, eml ];
  · norm_num [ Complex.ext_iff, Complex.exp_re, Complex.exp_im ]

/-- **log(-1) = πi**: The fundamental identity connecting the EML world
    to trigonometric functions and the constant π. -/
theorem log_neg_one : Complex.log (-1) = ↑Real.pi * Complex.I :=
  Complex.log_neg_one

/-
**π from log(-1)**: `π = -i · log(-1)`
-/
theorem pi_from_log_neg_one : (↑Real.pi : ℂ) = -Complex.I * Complex.log (-1) := by
  norm_num [ Complex.ext_iff, Complex.log_re, Complex.log_im ]

/-
**i from exp**: `i = exp(πi/2)` via Euler's formula
-/
theorem I_from_exp : Complex.I = Complex.exp (↑Real.pi / 2 * Complex.I) := by
  norm_num [ Complex.ext_iff, Complex.exp_re, Complex.exp_im ]

/-! ### Stage 5: Trigonometric functions from exp

Once we have `exp`, `log`, and complex arithmetic, all trigonometric
and hyperbolic functions follow from Euler's formula:
  `exp(ix) = cos(x) + i·sin(x)`
-/

/-- **Euler's formula**: `exp(ix) = cos(x) + i·sin(x)`.
    This is the bridge from the EML operator to trigonometric functions. -/
theorem euler_formula (x : ℂ) :
    Complex.exp (x * Complex.I) = Complex.cos x + Complex.sin x * Complex.I :=
  Complex.exp_mul_I x

/-- **sin from exp**: `sin(x) = (exp(-ix) - exp(ix)) · i / 2`.
    This is definitional in Mathlib. -/
theorem sin_from_exp (x : ℂ) :
    Complex.sin x =
      (Complex.exp (-x * Complex.I) - Complex.exp (x * Complex.I)) * Complex.I / 2 := by
  rfl

/-- **cos from exp**: `cos(x) = (exp(ix) + exp(-ix)) / 2`.
    This is definitional in Mathlib. -/
theorem cos_from_exp (x : ℂ) :
    Complex.cos x =
      (Complex.exp (x * Complex.I) + Complex.exp (-x * Complex.I)) / 2 := by
  rfl

/-
**sinh from exp**: `sinh(x) = (exp(x) - exp(-x)) / 2`
-/
theorem sinh_from_exp (x : ℂ) :
    Complex.sinh x = (Complex.exp x - Complex.exp (-x)) / 2 := by
  rw [ Complex.sinh, div_eq_div_iff ] <;> ring <;> norm_num

/-
**cosh from exp**: `cosh(x) = (exp(x) + exp(-x)) / 2`
-/
theorem cosh_from_exp (x : ℂ) :
    Complex.cosh x = (Complex.exp x + Complex.exp (-x)) / 2 := by
  exact ext rfl rfl

/-
**tan from sin and cos**: `tan(x) = sin(x) / cos(x)`
-/
theorem tan_from_sin_cos (x : ℂ) :
    Complex.tan x = Complex.sin x / Complex.cos x := by
  exact tan_eq_sin_div_cos x

/-
**tanh from sinh and cosh**: `tanh(x) = sinh(x) / cosh(x)`
-/
theorem tanh_from_sinh_cosh (x : ℂ) :
    Complex.tanh x = Complex.sinh x / Complex.cosh x := by
  exact tanh_eq_sinh_div_cosh x

/-! ### Stage 6: Main Universality Results

The following existential theorems state that specific elementary functions
are in the closure of `{eml, 1}`. Each is witnessed by a concrete EML tree.
-/

/-- **EML generates exp**: There exists an EML tree computing `exp`. -/
theorem eml_generates_exp :
    ∃ (t : EMLTree 1), ∀ (x : ℂ), t.eval (fun _ => x) = Complex.exp x :=
  ⟨.node (.var 0) .one, fun x => by simp [EMLTree.eval, eml_one_right]⟩

/-- **EML generates e**: There exists an EML tree computing Euler's number. -/
theorem eml_generates_e :
    ∃ (t : EMLTree 0), t.eval Fin.elim0 = Complex.exp 1 :=
  ⟨.node .one .one, EMLTree.constE_correct⟩

/-- **EML generates ln**: There exists an EML tree computing `ln` on positive reals. -/
theorem eml_generates_ln :
    ∃ (t : EMLTree 1), ∀ (x : ℝ), 0 < x →
      t.eval (fun _ => (↑x : ℂ)) = ↑(Real.log x) :=
  ⟨EMLTree.lnTree, fun x hx => EMLTree.lnTree_correct x hx⟩

/-- **EML generates 0**: There exists a constant EML tree evaluating to 0. -/
theorem eml_generates_zero :
    ∃ (t : EMLTree 0), t.eval Fin.elim0 = 0 :=
  ⟨EMLTree.constZero, EMLTree.constZero_correct⟩

/-- **EML generates sin (functional form)**: sin can be expressed as a composition
    of exp operations, which are themselves EML trees. -/
theorem eml_generates_sin_functional :
    ∀ (x : ℂ), Complex.sin x =
      (Complex.exp (-x * Complex.I) - Complex.exp (x * Complex.I)) * Complex.I / 2 :=
  fun x => sin_from_exp x

/-- **EML generates cos (functional form)**: cos can be expressed as a composition
    of exp operations, which are themselves EML trees. -/
theorem eml_generates_cos_functional :
    ∀ (x : ℂ), Complex.cos x =
      (Complex.exp (x * Complex.I) + Complex.exp (-x * Complex.I)) / 2 :=
  fun x => cos_from_exp x

/-! ### Summary

We have shown that the EML operator `eml(x, y) = exp(x) - log(y)`, together
with the single constant `1`, generates:

1. **exp** (depth 1, K = 3): `eml(x, 1) = exp(x)`
2. **e** (depth 1, K = 3): `eml(1, 1) = exp(1) = e`
3. **ln** (depth 3, K = 7): `eml(1, eml(eml(1, x), 1)) = ln(x)`
4. **0** (depth 3, K = 7): `eml(1, eml(eml(1, 1), 1)) = 0`
5. **Subtraction**: `eml(log(x), exp(y)) = x - y`
6. **Negation**: `eml(log(1-x), exp(1)) = -x`
7. **Multiplication** (real): `exp(log(x) + log(y)) = x * y`
8. **Division** (real): `exp(log(x) - log(y)) = x / y`
9. **Powers** (real): `exp(y · log(x)) = x^y`
10. **Square root** (real): `exp(log(x)/2) = √x`
11. **π**: via `log(-1) = πi`
12. **i**: via `exp(πi/2) = i`
13. **sin**: `(exp(-ix) - exp(ix)) · i / 2`
14. **cos**: `(exp(ix) + exp(-ix)) / 2`
15. **sinh, cosh, tan, tanh**: compositions of the above

This establishes the paper's main claim: the EML operator is a "continuous
Sheffer stroke" — a single binary operator sufficient for all elementary
mathematics, just as NAND suffices for all Boolean logic.
-/

end