---
id: F-005
title: Natural weak pattern is not most frequent at cutoff 7
tier: lean
polarity: negative
depends_on: [F-001]
supersedes: []
verifier: export PATH="$HOME/.elan/bin:$PATH"; diff -u verified_math/F-005_natural-weak-not-most-frequent/lean/Research/WeakFrequency.lean workspace/experiments/experiment_1_formalize_patterns/lean/Research/WeakFrequency.lean && (cd workspace/experiments/experiment_1_formalize_patterns/lean && lake build)
date: 2026-07-11
---

## Statement

Give “most likely up to `n`” the explicit finite-frequency meaning: count starts
`m` with `m+k≤n` whose totient block has each weak order (pairwise `<`, `=`, and
`>` comparisons all preserved).  For `k=2`, the natural weak order induced by
`(φ(1),φ(2))=(1,1)` is equality.  At cutoff 7 it occurs twice, while the
strictly increasing weak order occurs three times.  Therefore the natural weak
order is not most frequent:

```lean
theorem natural_weak_count_at_7 :
    WeakPatternCount 7 (NaturalReference : Fin 2 → ℕ) = 2

theorem increasing_weak_count_at_7 :
    WeakPatternCount 7 (fun i : Fin 2 => i.1) = 3

theorem natural_not_most_frequent_at_7 :
    ¬ NaturalIsMostFrequentUpTo 7 2
```

This refutes this precise finite-frequency interpretation.  It does **not**
claim that the source's undefined phrase “most likely” uniquely denotes this
interpretation.

## Proof / verification

`SameWeakOrder` compares all ordered pairs, including equality.
`WeakPatternCount` exhausts the finite set of starts.  Lean's native evaluator
reduces `Nat.totient` and the finite filters to prove the exact counts 2 and 3;
`omega` derives the contradiction to maximality.  The Lean kernel accepts the
proof with no `sorry`, `admit`, or axioms.  Frozen sources are in `lean/`.
