COUNTING COMPLEXITY IN LEAN
Counting complexity in Lean
CountingLib brings finite counting, weighted partition models, algorithms, and classification results into one reusable Lean 4 library.
Start with a small interface
Use a focused import for a definition or algorithm. Add a flagship module when you need a classification theorem. The Lean package is named countingComplexity; its public namespace is Counting.
import Counting.Foundation.Witness
open Counting.Foundation
example : countAccepted (fun b : Bool => decide (b = true)) = 1 :=
countAccepted_singleton trueFour flagship directions
The library is anchored in full research results. Public entry points retain their original hypotheses, exact representations, and reduction models.
| Direction | Public import | Scope |
|---|---|---|
| Holant | Counting.Flagships.Holant | Full Boolean dichotomy and binary-disequality variants |
| Complex-weighted CSP | Counting.Flagships.ComplexCSP | Structural collapse, effective recognition, and fixed-language classification |
| Planar homomorphisms | Counting.Flagships.PlanarHom | Nonnegative symmetric algebraic interactions on planar multigraphs |
| Matchgate width | Counting.Flagships.MatchgateWidth | Qutrit structure, exact realizations, and width obstructions |
How the library fits together
Shared definitions have one source provider. Bridges prove compatibility between representations; machine contracts remain separate from semantic identities.
| Layer | Responsibility | Entry points |
|---|---|---|
| Foundations | Finite counts, witnesses, encodings, and reductions | Counting |
| Weighted models | Ordered occurrences, open partitions, and gadgets | Counting.Model.Basic; Counting.Gadget.Composition |
| Algorithms | Evaluators, correctness, and explicitly scoped cost bounds | Counting.Algorithms |
| Reusable bridges | Model translation, resource elimination, and complexity transport | Counting.Reuse |
| Classification | Fixed research endpoints and their precise contracts | Counting.Flagships.* |
About this reference
The searchable API presents 333 selected declarations from 80 provider modules, organized into 30 contract families. It is an entry point to the library rather than an inventory of every internal declaration. Signatures come from recorded Lean environment exports; complete explicit types remain available alongside readable views.
This is a local design preview for v0.1.1. Source links identify the existing 6ca34e1 snapshot. The published release remains v0.1.0.