# Lech’s multiplicity conjecture

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

- [Lech's multiplicity conjecture](../../preprints/Lechs-multiplicity-conjecture-September-23-2026/paper.pdf)

## Scope

Lech's multiplicity conjecture compares Hilbert–Samuel multiplicities across flat local maps. The linked formalization covers a supporting characteristic-$p$ comparison over a complete Noetherian local domain $D$: for a complex satisfying the stated short-complex and finite-length homology conditions, its Frobenius multiplicity sequence converges to its Dutta multiplicity, and the Hilbert–Samuel multiplicity of $D$ is at most that Dutta multiplicity.

This selected statement is the complete-domain Dutta comparison. The paper's full flat-local result in arbitrary characteristic is outside it.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Complete-domain Dutta multiplicity comparison | [DuttaDomain.lean](../ComparatorChallenges/DuttaDomain.lean) |