Download the Proofs

Download & Build the Lean Proofs

The CESProofs library contains 1,923 declarations across 97 Lean 4 files with 0 sorry, 0 axioms beyond 3 justified classical results, and 99 key theorems covering CES production economics.

Prerequisites

Lean 4 (v4.28.0+) via elan
Git
~4 GB disk space (Mathlib cache)

1. Clone the repository

git clone https://github.com/jonsmirl/CESProofs.git
cd CESProofs

2. Fetch Mathlib cache

This downloads prebuilt .olean files so you don't need to rebuild Mathlib from source.

lake exe cache get

3. Build

lake build

Full build: ~2,328 jobs. Takes 10-20 minutes on first build depending on hardware.

4. Verify axiom usage

Check that any theorem uses only the 3 justified axioms:

# In Lean REPL or a scratch file:
#print axioms CESProofs.Foundations.emergent_CES

Library structure

Files are organized into 8 topic folders matching the derivation sections:

Folder	Files	Topics
`Foundations/`	13	CES definition, emergence, Hessian, information geometry, estimation
`CurvatureRoles/`	7	Superadditivity, correlation robustness, strategic, game theory, networks
`Potential/`	14	CES potential, Tsallis, effective curvature, bilateral trade, firm scope
`Dynamics/`	22	Business cycles, conservation laws, regime shifts, indicators, variance collapse
`Hierarchy/`	16	Damping cancellation, spectral hierarchy, activation, institutional reform
`EntryExit/`	7	Market structure, curvature in J, welfare, network entry
`Macro/`	6	Two-factor CES, directed technical change, green transition, tax structure
`Applications/`	11	AI transition, economics, inequality, social welfare, settlement

Axioms

Only 3 axioms are used, all classical results with citations in docstrings:

kolmogorov_nagumo — Kolmogorov-Nagumo mean theorem (1930)
aczel — Aczél functional equation theorem (1948)
transition_duration_scaling — Neishtadt GSPT scaling result