50 original theorems verified by computer. 478 total Lean statements. Zero sorries across 13 files.
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 repository contains 478 named statements. They are not all equally original. Here is the accounting:
- 50
- EML-original theorems — results specific to this framework (SuperBEST lower bounds, F16-shape witnesses, EMLTree depth hierarchy, ELC preservation, self-map conjugacies).
- 179
- 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). - 237
- Supporting lemmas — per-operator witnesses, trivial evaluations, definitional unfolds, and proof scaffolding that feed the originals.
- 478
- Total verified 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.
/-- 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). -/
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 :=
rpow_one_node_positive n x hx
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,
exp(log x) = x. -/
theorem exp_log_round_trip (x : ℝ) (hx : 0 < x) :
Real.exp (Real.log x) = 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
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): sin is not representable by any finite EML tree.
Sorry: quantitative zero-count bound needed — EML-k trees have ≤ B(k) zeros on ℝ.
This requires o-minimal structure theory (ℝ_exp is o-minimal). -/
theorem sin_not_in_eml (k : ℕ) :
∀ t : EMLTree, t.depth ≤ k →
¬ (∀ x : ℝ, t.evalReal x = Real.sin x) := by
sorry
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