Single_Operator_Formalization/RequestProject_Defs.lean at main · alejandrozu/Single_Operator_Formalization · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
import Mathlib

/-!
# Core Definitions for "All elementary functions from a single operator"

This file defines the EML (Exp-Minus-Log) operator and the EML expression tree type,
formalizing the core definitions from the paper by Andrzej Odrzywolek (arXiv:2603.21852v2).

## Main definitions

* `eml` - The EML operator: `eml(x, y) = exp(x) - log(y)`
* `EMLTree` - Expression trees with grammar `S → 1 | var(i) | eml(S, S)`
* `EMLTree.eval` - Evaluation of EML trees over ℂ
* `EMLTree.depth` - Depth of an EML tree
* `EMLTree.size` - Size (Kolmogorov complexity K) of an EML tree
-/

open Complex

/-- The EML (Exp-Minus-Log) operator on ℂ.
    `eml(x, y) = exp(x) - log(y)`

    This is the "continuous NAND gate" that, together with the constant 1,
    generates all elementary functions. -/
noncomputable def eml (x y : ℂ) : ℂ := Complex.exp x - Complex.log y

/-- EML expression tree with `n` input variables.

    The grammar is: `S → 1 | var(i) | eml(S, S)`

    Every elementary function can be represented as such a tree,
    using only the constant 1 and input variables as leaves.
    This is the continuous analogue of a Boolean circuit built entirely
    from NAND gates. -/
inductive EMLTree (n : ℕ) : Type where
  /-- The constant leaf `1` -/
  | one : EMLTree n
  /-- An input variable `x_i` -/
  | var : Fin n → EMLTree n
  /-- An EML node: `eml(left, right) = exp(left) - log(right)` -/
  | node : EMLTree n → EMLTree n → EMLTree n
  deriving Repr, DecidableEq

/-- Evaluate an EML tree in a given environment mapping variables to ℂ values. -/
noncomputable def EMLTree.eval (env : Fin n → ℂ) : EMLTree n → ℂ
  | .one => 1
  | .var i => env i
  | .node t₁ t₂ => eml (t₁.eval env) (t₂.eval env)

/-- The depth of an EML tree (max distance from root to leaf). -/
def EMLTree.depth : EMLTree n → ℕ
  | .one => 0
  | .var _ => 0
  | .node t₁ t₂ => 1 + max t₁.depth t₂.depth

/-- The size of an EML tree (total number of nodes, equals the Kolmogorov
    complexity K used in the paper for RPN program length). -/
def EMLTree.size : EMLTree n → ℕ
  | .one => 1
  | .var _ => 1
  | .node t₁ t₂ => 1 + t₁.size + t₂.size

/-- The number of leaves in an EML tree. -/
def EMLTree.leaves : EMLTree n → ℕ
  | .one => 1
  | .var _ => 1
  | .node t₁ t₂ => t₁.leaves + t₂.leaves

namespace EMLTree

/-- `exp(x) = eml(x, 1)` — depth 1, K = 3 -/
def expTree : EMLTree 1 := .node (.var 0) .one

/-- `e = eml(1, 1)` — depth 1, K = 3 -/
def constE : EMLTree 0 := .node .one .one

/-- `ln(x) = eml(1, eml(eml(1, x), 1))` — depth 3, K = 7 -/
def lnTree : EMLTree 1 :=
  .node .one (.node (.node .one (.var 0)) .one)

/-- `0 = eml(1, eml(eml(1, 1), 1))` = ln(1) — depth 3, K = 7 -/
def constZero : EMLTree 0 :=
  .node .one (.node (.node .one .one) .one)

/-- `exp(e) = eml(eml(1, 1), 1)` — depth 2, K = 5 -/
def constExpE : EMLTree 0 :=
  .node (.node .one .one) .one

/-- `e - 1 = eml(1, eml(1, 1))` — depth 2, K = 5 -/
def constEMinus1 : EMLTree 0 :=
  .node .one (.node .one .one)

end EMLTree