# Approximate counting and entropy of perfect matchings

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [A Fully Polynomial Randomized Approximation Scheme for Perfect Matchings in General Graphs](../../preprints/A-Fully-Polynomial-Randomized-Approximation-Scheme-for-Perfect-Matchings-in-General-Graphs-September-23-2026/main.pdf)
- [Entropy and Face Dimension of the Perfect-Matching Polytope](../../preprints/Entropy-and-Face-Dimension-of-the-Perfect-Matching-Polytope-September-23-2026/main.pdf)

## Scope

The formalization gives a fully polynomial randomized approximation scheme for counting perfect matchings in every finite simple undirected graph. For rational $0<\varepsilon<1$ and $0<\delta<1/2$, it returns a nonnegative rational estimate with relative error at most $\varepsilon$ with probability at least $1-\delta$. If the graph has no perfect matching, every execution returns zero.

The algorithm is a fixed finite-alphabet randomized machine. Its worst-case running time is polynomial in the binary input length, $\varepsilon^{-1}$, and $\log(\delta^{-1})$, including on unsuccessful random tapes.

For feasible edge marginals $x$ of perfect matchings in a loopless multigraph on $2m$ vertices, let $F(x)=-\sum_e x_e\log x_e$, $B(x)=-\sum_e(1-x_e)\log(1-x_e)$, and let $H(x)$ be the maximum entropy of a matching law with those marginals. The formalization proves $F(x)-(2-2/m)B(x)\le H(x)\le F(x)$ for $m\ge1$, including boundary points of the polytope. It retains the earlier coefficient-eight entropy bound and the deterministic counting approximations with factors $512^n$ for loopless graphs and $2^{18n}$ with singleton loops.

A further statement identifies the exact face obtained by expanding a degree-three vertex into a triangle and shows that minimal faces are carried to minimal faces by the expansion. The paper's sharp global face-dimension bound is not part of that selected statement.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Randomized approximation of the perfect-matching count | [MatchingFPRAS.lean](../ComparatorChallenges/MatchingFPRAS.lean) |
| Perfect-matching entropy bound | [MatchingEntropy.lean](../ComparatorChallenges/MatchingEntropy.lean) |
| Deterministic approximate matching count | [BinaryMatching.lean](../ComparatorChallenges/BinaryMatching.lean) |
| Approximate counting with singleton loops | [SingletonLoopMatching.lean](../ComparatorChallenges/SingletonLoopMatching.lean) |
| Refined pointwise perfect-matching entropy bounds | [MatchingEntropyBounds.lean](../ComparatorChallenges/MatchingEntropyBounds.lean) |
| Face correspondence under triangle expansion | [TriangleFace.lean](../ComparatorChallenges/TriangleFace.lean) |