477 Lean statements across 14 files. Zero sorries in 13 of the 14 files.
Before every deploy, each flagship below is checked against a pinned monogate-lean commit: its source
must appear there verbatim, and its theorem must compile with no sorryAx.
Verify this yourself
git clone https://github.com/agent-maestro/monogate-lean
cd monogate-lean
lake build
# expect: Build completed successfully.
# a sorry compiles too, with a "declaration uses 'sorry'" warning
First run takes 2–5 minutes (Mathlib oleans download from the GitHub cache). Runs locally.
No network verifier, no remote kernel. If lake build exits 0, every theorem on
this page compiled, and the ones without a documented sorry are checked from the
axioms of type theory up. #print axioms <name> tells the two apart: a checked
theorem never lists sorryAx.
Lean 4 is a proof assistant that mechanically checks every logical step of every proof against
the axioms of constructive type theory. It is not a linter. It is not a testing framework.
The kernel is a small, auditable program that either accepts a proof or rejects it.
The 14 files below contain 477 named theorems and lemmas. They are not all equally original. Here is the accounting:
- 50
- EML-original theorems, per the hand audit of 2026-04-26 — results specific to this framework (SuperBEST lower bounds, F16-shape witnesses, EMLTree depth hierarchy, ELC preservation, self-map conjugacies). This is that audit's count: it was not re-derived when files changed later, and no check verifies it.
- 427
- Everything else, by the same audit: Mathlib identity wrappers (named aliases of lemmas already in Mathlib, re-exported under EML-readable names, e.g.
exp_ln_cancel is Real.exp_log), per-operator witnesses, trivial evaluations, definitional unfolds, and proof scaffolding that feed the originals. The split between those kinds is not counted. - 477
- Total statements, all 0-sorry except as noted below.
- 2
- Sorry statements, all in
InfiniteZerosBarrier.lean: sin_not_in_eml and sin_not_in_real_EML_k. Both flag the same open gap — a quantitative zero-count bound on EML-k trees needs o-minimal structure theory (Wilkie 1996, not yet formalized in Mathlib).
Below: 39 flagship theorems across the 14 files. Every block is a verbatim copy of the source.
Each is linked to its GitHub line number. The "by" tactic block is the proof, not a description of the proof.
T_DIV_EXP_OUTER_LB — covers all 1024 circuits with F13/F14/F15/F16 as outer node. The wedge: these always return exp(...) > 0, but x/y at (−1, 2) is −1/2 < 0.
/-- **T_DIV_EXP_OUTER_LB** — No 2-node F16 circuit with exp-type outer operator
(F13, F14, F15, or F16) computes general division on ℝ².
Covers all 1024 such circuits (4 outer ops × 16 inner ops × 16 wire configs).
The g and h parameters encode any inner F16 operator applied to any wire selection from {x,y}. -/
theorem no_exp_outer_2node_div
(outer g h : ℝ → ℝ → ℝ)
(houter : outer ∈ ([D_F13, D_F14, D_F15, D_F16] : List (ℝ → ℝ → ℝ))) :
¬ (∀ x y : ℝ, outer (g x y) (h x y) = x / y) := by
simp only [List.mem_cons, List.mem_nil_iff, or_false] at houter
rcases houter with rfl | rfl | rfl | rfl
· exact no_F13_outer_2node_div g h
· exact no_F14_outer_2node_div g h
· exact no_F15_outer_2node_div g h
· exact no_F16fn_outer_2node_div g h
T_DIV_TWO_NODE_POS — the 2-node upper bound: D_F16(x, D_F13(−1, y)) = x/y for x, y > 0. Exactly one wire of reciprocal, exactly one wire of product.
/-- **T_DIV_TWO_NODE_POS** — Division is computable by a 2-node F16 circuit on (0,∞)²:
D_F16(x, D_F13(−1, y)) = x/y for all x, y > 0.
Proof:
D_F13(−1, y) = exp(−log y) = y⁻¹
D_F16(x, y⁻¹) = exp(log x + log y⁻¹) = exp(log x − log y) = exp(log(x/y)) = x/y. -/
theorem div_two_node_pos_domain (x y : ℝ) (hx : 0 < x) (hy : 0 < y) :
D_F16 x (D_F13 (-1) y) = x / y := by
have hinv : D_F13 (-1 : ℝ) y = y⁻¹ := by
unfold D_F13
rw [show (-1 : ℝ) * Real.log y = -(Real.log y) from by ring]
rw [Real.exp_neg, Real.exp_log hy]
rw [hinv]
unfold D_F16
rw [show Real.log y⁻¹ = -(Real.log y) from Real.log_inv y]
rw [Real.exp_add, Real.exp_log hx, Real.exp_neg, Real.exp_log hy]
field_simp
Multiplication on positives: one F16 node. The identity exp(log x + log y) = x·y is three Mathlib rewrites.
/-- Multiplication is a single F16 node on the positive domain:
F16fn(x,y) = exp(log(x) + log(y)) = x · y for x,y > 0. -/
theorem mul_one_node_positive (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 power x^n as a single F13 node: exp(n · log x) = x^n for x > 0. Covers recip (n = −1), sqrt (n = 1/2), general powers.
/-- Real power x^n is a single F16 node via EPL:
F13(n, x) = exp(n · log(x)) = x^n for x > 0. -/
theorem rpow_one_node_positive (n x : ℝ) (hx : 0 < x) :
Real.exp (n * Real.log x) = x ^ n := by
rw [Real.rpow_def_of_pos hx]; ring_nf
ln via EXL: exp(0) · log(x) = log(x). The extended-EXL operator makes ln a single node, closing the SuperBEST 14n positive-domain count, the count that uses EXL; /superbest counts in F16, where ln takes 2 nodes and the total is 15n.
/-- EXL identity: exp(0) * log(x) = log(x) for all real x.
Justifies the SuperBEST 1-node accounting of `ln(x)` via the extended
operator EXL(a, b) := exp(a) * log(b), with EXL(0, x) = log(x).
Note on scope: EXL is in the extended 23-operator catalogue (it has
the form h(exp(±x), log(±y)) with h(u, v) = u * v) but is not one of
the F1..F16 operators defined in AddLowerBound.lean / DivLowerBound.lean
(which use h ∈ {subtraction, identity, log-of-arithmetic, exp-of-arithmetic}).
The 14n SuperBEST headline that counts ln = 1n therefore relies on this
extended-op accounting. -/
theorem ln_one_node_via_exl (x : ℝ) :
Real.exp 0 * Real.log x = Real.log x := by
rw [Real.exp_zero, one_mul]
F14 identity — exp(x + log y) = exp(x) · y for y > 0. Computes the exp-times-positive product as a single F14 node.
/-- F14 identity: exp(x + log(y)) = exp(x) · y for y > 0.
Useful for computing exp(x) * y with a single F14 node. -/
theorem f14_identity (x y : ℝ) (hy : 0 < y) :
Real.exp (x + Real.log y) = Real.exp x * y := by
rw [Real.exp_add, Real.exp_log hy]
F15 identity — exp(x − log y) = exp(x) / y for y > 0. The division partner of F14.
/-- F15 identity: exp(x − log(y)) = exp(x) / y for y > 0.
Useful for computing exp(x) / y with a single F15 node. -/
theorem f15_identity (x y : ℝ) (hy : 0 < y) :
Real.exp (x - Real.log y) = Real.exp x / y := by
rw [Real.exp_sub, Real.exp_log hy]
F16 identity — exp(log x + log y) = x · y for x, y > 0. Named alias of mul_one_node_positive that completes the F13-F16 naming symmetry.
/-- F16 identity: exp(log(x) + log(y)) = x · y for x, y > 0.
Named alias of `mul_one_node_positive` that completes the F13–F16
naming symmetry alongside `f14_identity` and `f15_identity`. -/
theorem f16_identity (x y : ℝ) (hx : 0 < x) (hy : 0 < y) :
Real.exp (Real.log x + Real.log y) = x * y :=
mul_one_node_positive x y hx hy
Same-sign negative multiplication is a single F16 node: exp(log(−x) + log(−y)) = x · y for x, y < 0. Extends mul_one_node_positive to the negative quadrant via neg_pos.
/-- Multiplication of two negatives is a single F16 node:
exp(log(−x) + log(−y)) = x · y for x, y < 0.
Extends `mul_one_node_positive` to the same-sign negative domain,
using `neg_pos` to reduce to the positive case and `neg_mul_neg`
to close the product. -/
theorem mul_of_negatives_one_node (x y : ℝ) (hx : x < 0) (hy : y < 0) :
Real.exp (Real.log (-x) + Real.log (-y)) = x * y := by
have hxp : 0 < -x := neg_pos.mpr hx
have hyp : 0 < -y := neg_pos.mpr hy
rw [mul_one_node_positive (-x) (-y) hxp hyp]
ring
The SuperBEST positive-domain summary theorem — all seven 1-node operations bundled in a single conjunction (exp, mul, pow, recip, sqrt, ln-via-EXL, F14 identity).
/-- All seven 1-node positive-domain results, collected:
exp, mul, pow, recip, sqrt, ln (via EXL), and the F14 identity. -/
theorem superbest_positive_one_node_ops :
(∀ x : ℝ, Real.exp x - Real.log 1 = Real.exp x) ∧ -- exp: 1n
(∀ x y : ℝ, 0 < x → 0 < y →
Real.exp (Real.log x + Real.log y) = x * y) ∧ -- mul: 1n (x,y>0)
(∀ n x : ℝ, 0 < x → Real.exp (n * Real.log x) = x ^ n) ∧ -- pow: 1n (x>0)
(∀ x : ℝ, 0 < x →
Real.exp ((-1) * Real.log x) = 1 / x) ∧ -- recip: 1n (x>0)
(∀ x : ℝ, 0 < x →
Real.exp ((1/2) * Real.log x) = Real.sqrt x) ∧ -- sqrt: 1n (x>0)
(∀ x : ℝ, Real.exp 0 * Real.log x = Real.log x) ∧ -- ln: 1n via EXL
(∀ x y : ℝ, 0 < y →
Real.exp (x + Real.log y) = Real.exp x * y) := -- f14: exp(x)·y, y>0
⟨fun x => by simp [Real.log_one],
mul_one_node_positive,
rpow_one_node_positive,
recip_one_node_positive,
sqrt_one_node_positive',
ln_one_node_via_exl,
f14_identity⟩
sqrt = EPL(0.5, x) = exp(0.5 · log x). Same mechanism as recip (−1) and pow. This is the witness that collapsed sqrt from 2n to 1n.
/-- EPL(0.5, x) = exp(0.5 · log(x)) = x^(1/2) = sqrt(x) for x > 0.
Same mechanism as pow = 1n and recip = 1n via the EPL/F13 primitive. -/
theorem sqrt_is_one_node_positive (x : ℝ) (hx : 0 < x) :
Real.exp (0.5 * Real.log x) = Real.sqrt x := by
rw [Real.sqrt_eq_rpow]
simp [Real.rpow_def_of_pos hx]
ring_nf
The ModelAudit companion to mul_one_node_positive (UpperBounds.lean:44). Duplicate statement, cross-referenced in the audit narrative.
/-- F16fn(x,y) = exp(log(x) + log(y)) = x · y for x,y > 0.
Multiplication is a single F16 node on the positive domain. -/
theorem mul_is_one_node_positive (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]
EPL(n, x) = exp(n · log x) = x^n for x > 0. Closes pow as a single F13 node — the construction that subsumes recip (n = −1), sqrt (n = 1/2), and general powers in the v5.3 audit.
/-- EPL(n, x) = exp(n · log x) = x^n for x > 0 (pow = 1n). -/
theorem pow_is_one_node_positive (n x : ℝ) (hx : 0 < x) :
Real.exp (n * Real.log x) = x ^ n := by
rw [Real.rpow_def_of_pos hx]; ring_nf
CEML-T5 — Euler's identity inside the EMLTree inductive type. The tree ceml(iπ, 1) evaluates to e^(iπ) = −1, so the tree +1 equals 0.
/-- CEML-T5: Euler Identity (principal branch).
ceml(iπ, 1) = exp(iπ) = -1, so ceml(iπ, 1) + 1 = 0. -/
theorem euler_identity :
EMLTree.eval (.ceml (.const (Complex.I * Real.pi)) (.const 1)) 0 + 1 = 0 := by
simp only [EMLTree.eval, Complex.log_one, sub_zero]
rw [show Complex.I * ↑Real.pi = ↑Real.pi * Complex.I from mul_comm _ _,
Complex.exp_pi_mul_I]
norm_num
EML-0 ⊊ EML-1. The depth-1 tree computing exp cannot be constant, proved by evaluating at 0 and 1 and invoking Real.exp_one_gt_d9.
/-- expTree is not constant (EML-0 ⊊ EML-1). -/
theorem exp_not_constant : ¬ (∃ c : ℂ, ∀ x, expTree.eval x = c) := by
intro ⟨c, hc⟩
have h0 : Complex.exp 0 = c := by simpa [expTree_eval] using hc 0
have h1 : Complex.exp 1 = c := by simpa [expTree_eval] using hc 1
have heq : Complex.exp (1 : ℂ) = 1 := by rw [h1, ← h0]; simp
have hre : Real.exp 1 = 1 := by
have := congr_arg Complex.re heq
simp only [Complex.one_re] at this
rwa [show (Complex.exp (1:ℂ)).re = Real.exp 1 from by
have : (1:ℂ) = ((1:ℝ):ℂ) := by norm_cast
rw [this, Complex.exp_ofReal_re]] at this
linarith [Real.exp_one_gt_d9]
OBS 08-C — sinh(ln 2) = 3/4. One half of the 3-4-5 Pythagorean triple that lives on the hyperbolic unit curve at x = ln 2.
/-- Numeric witness used in the session: `sinh(ln 2) = 3/4`.
Part of the 3-4-5 Pythagorean-triple observation (OBS 08-C). -/
theorem sinh_log_two : Real.sinh (Real.log 2) = 3 / 4 := by
rw [Real.sinh_eq, Real.exp_log (by norm_num : (2:ℝ) > 0), Real.exp_neg,
Real.exp_log (by norm_num : (2:ℝ) > 0)]
norm_num
The 3-4-5 Pythagorean triple witnessed inside the hyperbolic identity cosh² − sinh² = 1 at x = ln 2. (5/4)² − (3/4)² = 1.
/-- The 3-4-5 Pythagorean triple witness at `x = ln 2` in the hyperbolic
identity (OBS 08-C, proved). -/
theorem pythagorean_triple_at_log_two :
(Real.cosh (Real.log 2)) ^ 2 - (Real.sinh (Real.log 2)) ^ 2 = 1 := by
exact cosh_sq_sub_sinh_sq (Real.log 2)
The headline ELC-preservation witness — sinh x = (exp x − exp(−x))/2. Makes sinh an arithmetic combination of two exp-applications, hence sinh ∘ ELC ⊆ ELC.
/-- **Explicit ELC-primitive decomposition of sinh**: `sinh x = (exp x − exp(−x))/2`.
This makes sinh an arithmetic combination of two exp-applications (each
one F16 node), hence sinh ∘ ELC ⊆ ELC under the standard ELC definition
closed under {+, −, ·, /, exp, log}. -/
theorem sinh_as_exp_arithmetic (x : ℝ) :
Real.sinh x = (Real.exp x - Real.exp (-x)) / 2 := by
rw [Real.sinh_eq]
The cosh partner — cosh x = (exp x + exp(−x))/2. Same ELC-arithmetic decomposition; combined with sinh, gives the full hyperbolic ELC-preservation result.
/-- **Explicit ELC-primitive decomposition of cosh**: `cosh x = (exp x + exp(−x))/2`. -/
theorem cosh_as_exp_arithmetic (x : ℝ) :
Real.cosh x = (Real.exp x + Real.exp (-x)) / 2 := by
rw [Real.cosh_eq]
g ∘ exp = exp ∘ f on (0,∞), where f(x) = exp(x) + ln(x) is the EAL self-map and g(y) = exp(y) · ln(y) is the EXL self-map.
/-- **EAL↔EXL conjugacy via exp.** Let `f(x) = exp(x) + ln(x)` be the EAL
self-map (the value of the F16 operator `EAL` evaluated on the diagonal)
and `g(y) = exp(y) · ln(y)` the EXL self-map. Then on the positive reals,
`g(exp(x)) = exp(f(x))`.
This is the identity `exp(exp(x) + ln(x)) = exp(exp(x)) · x = exp(exp(x)) · ln(exp(x))`.
-/
theorem eal_exl_conjugacy (x : ℝ) (hx : 0 < x) :
Real.exp (Real.exp x) * Real.log (Real.exp x)
= Real.exp (Real.exp x + Real.log x) := by
rw [Real.exp_add, Real.log_exp, Real.exp_log hx]
The subtractive / divisive partner: exp(y) / ln(y) and exp(x) − ln(x) conjugate via exp on (0,∞) \ {1}.
/-- **EML↔EDL conjugacy via exp.** Let `f(x) = exp(x) − ln(x)` be the EML
self-map and `g(y) = exp(y) / ln(y)` the EDL self-map. Then on the
positive reals with `x ≠ 1` (so `ln(x) ≠ 0`), `g(exp(x)) = exp(f(x))`.
This is the identity `exp(exp(x) − ln(x)) = exp(exp(x)) / x = exp(exp(x)) / ln(exp(x))`.
-/
theorem eml_edl_conjugacy (x : ℝ) (hx : 0 < x) (hx1 : x ≠ 1) :
Real.exp (Real.exp x) / Real.log (Real.exp x)
= Real.exp (Real.exp x - Real.log x) := by
have h_log_ne : Real.log x ≠ 0 := Real.log_ne_zero_of_pos_of_ne_one hx hx1
rw [Real.exp_sub, Real.log_exp, Real.exp_log hx]
The key rewrite used in both EAL↔EXL and EML↔EDL conjugacies — for x > 0, exp(log x) = x. Lifted into the conjugacy namespace as a citable lemma.
/-- The key rewrite used in both conjugacies: for x > 0,
`ln(exp x) = x` AND `exp(ln x) = x`. Packaged as a named step. -/
theorem exp_log_round_trip (x : ℝ) (hx : 0 < x) :
Real.log (Real.exp x) = x ∧ Real.exp (Real.log x) = x :=
⟨Real.log_exp x, Real.exp_log hx⟩
Part B of T01 — a non-zero real-analytic function on [a,b] has finitely many zeros there. Bolzano-Weierstrass + Mathlib's analytic identity theorem.
/-- A non-zero real-analytic function on [a,b] has finitely many zeros.
Proof: If the zero set Z is infinite, Bolzano-Weierstrass gives an accumulation point
x₀ ∈ [a,b] (Set.Infinite.exists_accPt_of_subset_isCompact). Then f is frequently zero
near x₀. By the analytic identity theorem f = 0 on all of [a,b], contradicting hf_nonzero. -/
lemma analytic_finite_zeros_compact (f : ℝ → ℝ) (a b : ℝ) (hab : a < b)
(hf_analytic : AnalyticOnNhd ℝ f (Set.Icc a b))
(hf_nonzero : ∃ x ∈ Set.Ioo a b, f x ≠ 0) :
Set.Finite {x ∈ Set.Icc a b | f x = 0} := by
by_contra h_not_fin
-- `Set.Infinite` is defeq to `¬ Set.Finite`, but dot notation needs the
-- explicit `Set.Infinite` type for field resolution.
have h_inf : Set.Infinite {x ∈ Set.Icc a b | f x = 0} := h_not_fin
obtain ⟨x₀, hx₀_mem, hx₀_acc⟩ :=
h_inf.exists_accPt_of_subset_isCompact isCompact_Icc (Set.sep_subset _ _)
have haccf : AccPt x₀ (𝓟 {z | f z = 0}) :=
hx₀_acc.mono (Filter.principal_mono.mpr fun y hy => hy.2)
have hfreq : ∃ᶠ z in 𝓝[≠] x₀, f z = 0 :=
frequently_iff_neBot.mpr haccf
have heqon : Set.EqOn f 0 (Set.Icc a b) :=
hf_analytic.eqOn_zero_of_preconnected_of_frequently_eq_zero
isPreconnected_Icc hx₀_mem hfreq
obtain ⟨x₁, hx₁_mem, hfx₁⟩ := hf_nonzero
exact hfx₁ (heqon (Set.Ioo_subset_Icc_self hx₁_mem))
Part C of T01 — every well-formed real EML tree is real-analytic on (0, ∞). Lifted from ℝ→ℂ analyticity via Complex.reCLM.
/-- Every well-formed real EML tree function is real-analytic on (0, ∞).
Requires WellFormedPos: all log arguments must evaluate to positive reals on (0,∞).
This is necessary — without it the ceml/ceml slit-plane condition can fail.
Derived from `eml_tree_eval_analyticOnNhd` (ℝ→ℂ analyticity of t.eval ∘ (↑·))
by composing with Complex.reCLM (continuous ℝ-linear map ℂ →L[ℝ] ℝ). (0 sorry) -/
lemma eml_tree_analytic (t : EMLTree)
(hwf : ∀ x ∈ Set.Ioi 0, t.WellFormedPos x) :
AnalyticOnNhd ℝ t.evalReal (Set.Ioi 0) := by
have hcomplex := eml_tree_eval_analyticOnNhd t hwf
have heq : t.evalReal = Complex.reCLM ∘ (fun x : ℝ => t.eval (↑x : ℂ)) := by
ext x; simp [EMLTree.evalReal, Complex.reCLM]
rw [heq]
exact (Complex.reCLM.analyticOnNhd Set.univ).comp hcomplex (Set.mapsTo_univ _ _)
The honest partial. T01 at depth k. The final step — "EML-k trees have at most B(k) real zeros" — needs o-minimal structure theory (Wilkie 1996). Documented as a single sorry, not hidden.
⚠ Contains sorry — documented open gap. The statement is the T01
barrier; the missing step is the quantitative zero-count bound for EML-k trees,
which requires o-minimal structure theory not yet formalized in Mathlib.
/-- T01 (Infinite Zeros Barrier) — open.
`sin` is not representable by any finite EML tree.
### Mathematical content
Every depth-`k` EML tree (in the F16 grammar) is real-analytic on
`(0, ∞)` and has only finitely many zeros on every bounded
sub-interval — let `B(k)` be that bound. `sin` has a zero at
every `nπ`, hence infinitely many on every unbounded interval.
For sufficiently large intervals the zero count exceeds `B(k)`,
contradiction.
### Why it matters
This is **T01**, the headline barrier theorem of the EML/Pfaffian
hierarchy: it shows the entire EML grammar (under any depth) is
strictly weaker than `ℝ_an,exp`. Forge's runtime treats `sin` as
an external transcendental for exactly this reason.
### Mathlib infrastructure needed
* Khovanskii's zero-count theorem on Pfaffian chains: every
Pfaffian function of order `r` and degree `d` has at most a
polynomial-in-`(r, d)` number of zeros on a bounded interval.
* Equivalently, the o-minimality of `ℝ_exp` (Wilkie 1996), which
gives a uniform finite-zero bound for every definable function.
* `Real.exp` and `Real.log` are already in Mathlib; what's
missing is the meta-theorem that the structure they generate
is o-minimal, plus the constructive zero bound that drops out
of o-minimality. Tracking issue: see
`MATHLIB_KHOVANSKII_NEEDS.md` for a survey of the gap. -/
theorem sin_not_in_eml (k : ℕ) :
∀ t : EMLTree, t.depth ≤ k →
¬ (∀ x : ℝ, t.evalReal x = Real.sin x) := by
sorry -- Open: needs Khovanskii zero-count or o-minimal ℝ_exp.
-- See docstring for the missing Mathlib infrastructure.
The headline theorem — every EML-elementary function admits an EMLTree witness whose evaluation matches the function pointwise. Proof is one-line by definition unfolding; the mathematical content is what FUNCTIONS are EML-elementary, captured by the closure theorem + concrete witnesses.
/-- **EML universality (statement form).** Every EML-elementary function
admits an EML routing tree witness whose evaluation matches the
function pointwise.
The proof is one line by unfolding the definition; the mathematical
content of universality is in *which* functions are EML-elementary,
captured by the witness theorems below + closure under composition. -/
theorem eml_universality :
∀ f : ℂ → ℂ, IsEMLElementary f → ∃ t : EMLTree, ∀ x, f x = t.eval x := by
intro f hf
obtain ⟨_, t, _hd, ht⟩ := hf
exact ⟨t, ht⟩
Concrete witness — the constant function fun _ => c is EML-elementary at depth 0. The base case for the universality witness ladder.
/-- The constant function is EML-elementary at depth 0. -/
theorem const_isEMLElementary (c : ℂ) :
IsEMLElementary (fun _ : ℂ => c) :=
⟨0, const_in_EML_k c 0⟩
Concrete witness — the identity function fun x => x is EML-elementary at depth 0.
/-- The identity function is EML-elementary at depth 0. -/
theorem id_isEMLElementary : IsEMLElementary (fun x : ℂ => x) :=
⟨0, id_in_EML_k 0⟩
Concrete witness — Complex.exp is EML-elementary at depth 1. The first non-trivial witness in the ladder.
/-- Complex exponential is EML-elementary at depth 1. -/
theorem exp_isEMLElementary :
IsEMLElementary (fun x : ℂ => Complex.exp x) :=
⟨1, exp_in_EML_one⟩
Concrete compositional witness — exp(exp(x)) is EML-elementary at depth ≤ 2 via IsEMLElementary.comp closure. Confirms composition closure ships, not just statement.
/-- exp(exp(x)) is EML-elementary at depth ≤ 2. -/
theorem exp_exp_isEMLElementary :
IsEMLElementary (fun x : ℂ => Complex.exp (Complex.exp x)) := by
have h := IsEMLElementary.comp exp_isEMLElementary exp_isEMLElementary
-- h : IsEMLElementary ((fun x => exp x) ∘ (fun x => exp x))
-- = IsEMLElementary (fun x => exp (exp x)) by comp definition
exact h
The structural non-elementary witness — no elementary function satisfies Γ(s+1) = s·Γ(s). This is the standard textbook argument that gamma sits outside the elementary class (cf. Hardy, Boros-Moll).
/-- **Functional equation** Γ(s+1) = s · Γ(s) for s ≠ 0.
No elementary function satisfies this functional equation;
this is the standard "gamma is not elementary" witness used in
textbook treatments (cf. Hardy, Boros-Moll). -/
theorem gamma_functional_equation {s : ℝ} (hs : s ≠ 0) :
Gamma (s + 1) = s * Gamma s :=
Real.Gamma_add_one hs
Functional equation + base case fix Γ on positive integers as the factorial — the consistency check that the Mathlib Gamma matches the textbook definition.
/-- **Factorial connection** Γ(n+1) = n! for natural n. The two
properties (functional equation + base case) determine Γ on ℕ. -/
theorem gamma_nat_eq_factorial (n : ℕ) : Gamma (n + 1) = n.factorial :=
Real.Gamma_nat_eq_factorial n
Mathlib analogue of the textbook chain identity Γ'(s) = Γ(s)·ψ(s); at integer points ψ(n+1) = -γ + harmonic n. Closest available Lean-4 expression of the digamma relation pending a named digamma function.
/-- **Derivative at positive integers** (Mathlib's `deriv_Gamma_nat`):
Γ'(n+1) = n! · (-γ + harmonic n), where γ is the Euler-Mascheroni
constant and harmonic n = 1 + 1/2 + ... + 1/n.
This is the closest Mathlib analogue of the textbook chain identity
Γ'(s) = Γ(s) · ψ(s); at integer points ψ(n+1) = -γ + harmonic n,
so the formula matches once digamma is named. -/
theorem deriv_gamma_at_nat (n : ℕ) :
deriv Gamma (n + 1) = n.factorial * (-eulerMascheroniConstant + harmonic n) :=
Real.deriv_Gamma_nat n