---
id: F-026
title: Kernel-only weak-frequency counterexample
tier: lean
polarity: negative
depends_on: [F-001]
supersedes: [F-005]
verifier: export PATH="$HOME/.elan/bin:$PATH"; diff -u verified_math/F-026_kernel-weak-frequency-counterexample/lean/Research/WeakFrequencyKernel.lean workspace/experiments/experiment_1_formalize_patterns/lean/Research/WeakFrequencyKernel.lean && (cd workspace/experiments/experiment_1_formalize_patterns/lean && lake build)
date: 2026-07-11
---

## Statement

Under exact cumulative finite-start frequency for weak order patterns, the
length-two natural equality order has count 2 through cutoff 7, whereas the
increasing order has count 3.  Hence the natural order is not most frequent at
that cutoff.

Formal theorems:

```lean
theorem natural_weak_count_at_7_kernel :
  WeakPatternCountK 7 (NaturalReferenceK : Fin 2 → ℕ) = 2

theorem increasing_weak_count_at_7_kernel :
  WeakPatternCountK 7 (fun i : Fin 2 => i.1) = 3

theorem natural_not_most_frequent_at_7_kernel :
  ¬ NaturalIsMostFrequentUpToK 7 2
```

## Proof / verification

This supersedes F-005 only because F-005 used `native_decide`, whose axiom trail
the referee rejected.  Here each totient value through 7 is proved from
Mathlib's prime, prime-power, and multiplicativity theorems.  `fin_cases`
explicitly enumerates all eight possible starts, proves the filtered finsets are
exactly `{0,2}` and `{1,3,5}`, and ordinary kernel `decide` computes only their
cards.  `#print axioms` reports only `propext`, `Classical.choice`, and
`Quot.sound`, with no native evaluator axiom.

Artifact: `lean/Research/WeakFrequencyKernel.lean`; full `lake build` succeeds
without `sorry`, `admit`, axioms declared by this project, or unsafe escape
hatches.
