# Positive metric entropy for the standard map

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

- [Positive Metric Entropy for the Standard Map at Large Parameters](../../preprints/Positive-Metric-Entropy-for-the-Standard-Map-at-Large-Parameters-September-23-2026/paper.pdf)

## Scope

The formalization proves Sinai's positive-entropy conjecture for the standard sine map on the two-dimensional torus in the stronger form of a full positive parameter tail. For every sufficiently large parameter, normalized area has positive metric entropy, and a positive-area set has positive largest Lyapunov exponent with the stated derivative-growth limit.

It also constructs a positive-area invariant ergodic hyperbolic component. That component splits into finitely many cyclic pieces on each of which the corresponding iterate is Bernoulli. No genericity assumption on the parameter is used.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Positive-area hyperbolic Bernoulli component | [StandardMapComponents.lean](../ComparatorChallenges/StandardMapComponents.lean) |
| Positive metric entropy for all sufficiently large parameters | [StandardMapEntropy.lean](../ComparatorChallenges/StandardMapEntropy.lean) |
| Positive Lyapunov exponents and entropy | [StandardMapLyapunov.lean](../ComparatorChallenges/StandardMapLyapunov.lean) |