---
id: F-034
title: The natural length-two weak order is asymptotically not most frequent
tier: lean
polarity: negative
depends_on: [F-028, F-033]
supersedes: []
verifier: export PATH="$HOME/.elan/bin:$PATH"; diff -u verified_math/F-034_natural-frequency-negative/lean/Research/NaturalFrequencyNegative.lean workspace/experiments/experiment_3_adjacent_equal_density/lean/Research/NaturalFrequencyNegative.lean && (cd workspace/experiments/experiment_3_adjacent_equal_density/lean && lake build)
date: 2026-07-11
---

## Statement

For all sufficiently large finite cutoffs, the natural weak order of
`(φ(1),φ(2))=(1,1)` is not most frequent:

```lean
∀ᶠ n : ℕ in atTop, ¬NaturalIsMostFrequentUpToK n 2.
```

Hence the canonical eventual reading from F-028 is false:

```lean
¬EventuallyNaturalIsMostFrequentK2.
```

The corresponding limiting-frequency claim is also false.  Formally,
`¬LimitingNaturalIsMostFrequentK2`, where that proposition says that the
cumulative equality, increase, and decrease frequencies all converge and the
equality limit is at least both strict-order limits.

## Proof / verification

At cutoff `N+1`, weak-pattern counts are exactly the `Nat.count` values for the
three adjacent orders.  F-033 says equality eventually occupies less than one
third, while equality, increase, and decrease partition all `N` starts.  Thus
one strict order beats equality at every sufficiently large cutoff.  For the
limiting version, the stronger construction gives equality frequency below
`3/10` eventually; if all three limits existed and equality dominated both,
their sum would be at most `9/10`, contradicting the formally proved partition
limit `e+i+d=1`.

Artifact: `lean/Research/NaturalFrequencyNegative.lean`; Lean accepts it with
no `sorry`, `admit`, native evaluator axiom, or project-declared axiom.
