The AczelCES library contains 2,059 declarations across 164 Lean 4 files with 0 sorry and only 2 axioms, both classical literature results (Aczél functional equation, Kolmogorov-Nagumo mean). All other theorems depend only on propext, Classical.choice, and Quot.sound.
elangit clone https://github.com/jonsmirl/AczelCES.git
cd AczelCESThis downloads prebuilt .olean files so you don't need to rebuild Mathlib from source.
lake exe cache getlake build AczelCESFull build: ~3,543 jobs. Takes 10-20 minutes on first build depending on hardware.
Check that any theorem depends only on the two classical axioms plus Lean's standard trio:
# In Lean REPL or a scratch file:
#print axioms AczelCES.Core.Uniqueness.ces_uniquenessFiles are organized into 16 topic folders matching the layered design of the archive:
| Folder | Files | Topics |
|---|---|---|
Core/ | 8 | Master generator, Aczél/KN axioms, uniqueness, network uniqueness, general weights |
Derivatives/ | 7 | Aggregator, factor shares, curvature, cost function, Fisher info, bridge |
Structure/ | 8 | Homogeneity, symmetry, log relation, concavity, cumulant tower, Hessian, isoquant Riemannian |
SextupleRole/ | 10 | Superadditivity, correlation robustness, strategic, network scaling, estimation, phase ordering, capstone, game theory |
Static/ | 5 | Production duality, Arrow-Pratt, elasticity, ten-way identity, IRS |
Network/ | 7 | Laplacian, spectral gap, Fiedler, fragmentation, diversity premium, uniqueness |
Potential/ | 11 | Effective curvature, Tsallis uniqueness, Q-equilibrium/dynamics, bilateral trade, firm scope, phase transition, welfare |
Lyapunov/ | 8 | Antitone, Tsallis concavity, unique minimizer, Shannon/Tsallis gradient flow, A3 iteration |
Dynamics/ | 22 | Business cycles, conservation, regime shifts, Phillips, indicators, Minsky speed, fiscal dynamics |
Hierarchy/ | 17 | Damping cancellation, spectral hierarchy, activation, institutional, RG, monetary policy, EMD bridge |
Macro/ | 10 | Multiplier, recession, stagflation, two-factor, tax, growth, directed change, green, accumulation |
EntryExit/ | 7 | Market structure, curvature in J, welfare, network entry |
Information/ | 6 | KL, binEntropy, Shannon, Chentsov bridge, welfare Bregman, Fisher-Rao geodesic |
Chentsov/ | 16 | Escort, exponential family, KL divergence, Fisher-Rao, Cramér-Rao, MLE, sufficiency, natural gradient, logit bridge |
SocialChoice/ | 7 | Preferences, Debreu, Arrow, Condorcet, voting rules, DeGroot, Sen |
Applications/ | 15 | Consumer theory, trade theory, welfare, inequality, AI transition, open economy, settlement |
Only 2 axioms are used, both classical results cited in their docstrings:
lit_aczel — Aczél functional equation theorem (1948)lit_kolmogorov_nagumo — Kolmogorov-Nagumo mean theorem (1930)Every other theorem depends only on Lean's standard metatheoretic axioms: propext, Classical.choice, Quot.sound.