# A <i>C</i><sup>1</sup> counterexample to the entropy conjecture

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

- [A $C^1$ Counterexample to the Entropy Conjecture](../../preprints/A-C1-Counterexample-to-the-Entropy-Conjecture-September-25-2026/article.pdf)

## Scope

Shub's entropy conjecture predicts that a smooth self-map's topological entropy is at least the logarithm of the spectral radius of its action on real homology. The formalization gives a counterexample to the general $C^1$ self-map version: a noninvertible $C^1$ map on a compact smooth manifold without boundary has topological entropy zero, while its action on second real homology has a nonzero eigenvector with eigenvalue $2$. Thus the homological lower bound is strictly positive and fails for this map.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| A $C^1$ counterexample to the entropy conjecture | [C1EntropyCounterexample.lean](../ComparatorChallenges/C1EntropyCounterexample.lean) |