Papers and Lean sources

Full Boolean Holant

Chenghua Liu, Boning Meng, and Juqiu Wang (2026). A Full Complexity Dichotomy for Complex-Valued Boolean Holant Problems.

Public entry: Counting.Flagships.Holant. The API retains ordinary and native-disequality wiring contracts, exact output representations, and the fixed-language evaluation / uniform recognition distinction.

Binary-disequality Holant

Chenghua Liu and Boning Meng (2026). A Dichotomy for Complex Boolean Holant with Binary Disequality.

The pinned Lean release contains a revised manuscript and correspondence notes. Its contract follows that bundled revision; it is not asserted identical to arXiv v1. This research line shares Counting.Flagships.Holant with the full Boolean result.

Complex-weighted counting CSP

Chenghua Liu and Boning Meng (2026). From Block Orthogonality to Decidability in Complex-Weighted Counting CSP.

Public entry: Counting.Flagships.ComplexCSP. The recognition chain uses the proved all-finite-instance correction of the isomorphism criterion associated with Theorem 5.2. The printed simple-instance formulation and its counterexample are recorded separately.

Nonnegative planar homomorphisms

Chenghua Liu and Boning Meng (2026). A Dichotomy for Planar Graph Homomorphisms with Nonnegative Weights.

Public entry: Counting.Flagships.PlanarHom. The selected library endpoints concern symmetric algebraic-real matrices and preserve the ordinary planar multigraph promise. The original source also retains an author-hosted manuscript and additional material outside the selected proof closure.

Matchgate width

Chenghua Liu and Boning Meng (2026). When Matchgate Base Collapse Fails: A Qutrit Trichotomy and Unbounded Exact Width.

Public entry: Counting.Flagships.MatchgateWidth. Exact realization, compression, and width statements retain their domain, field, rank, deficiency, and presentation assumptions.

Foundations and algorithm literature

These works provide context for the library's interfaces. Their inclusion does not claim that every result in each paper has been formalized. Read the algorithm contracts for the guarantees actually supplied.

Lean infrastructure and citation

CountingLib pins Lean 4.34.1 and mathlib commit d13f23b723b8a846827a245b89c10fc7d3f11612. Original component attribution and license scopes are preserved.

When using a research result, cite its paper and identify the original Lean source commit. Identify the CountingLib release or commit separately when using the assembled library or its public bridges.