---
id: F-003
title: Every-pattern length is bounded by decreasing-run length
tier: lean
polarity: negative
depends_on: [F-001]
supersedes: []
verifier: export PATH="$HOME/.elan/bin:$PATH"; diff -u verified_math/F-003_all-patterns-bounded-by-decreasing/lean/Research/Structural.lean workspace/experiments/experiment_1_formalize_patterns/lean/Research/Structural.lean && (cd workspace/experiments/experiment_1_formalize_patterns/lean && lake build)
date: 2026-07-11
---

## Statement

Let `G(n)` be the largest `k≤n` for which some block
`φ(m+1),…,φ(m+k)`, ending by `n`, is strictly decreasing.  Then every cutoff
satisfies

\[
F(n)\leq G(n).
\]

Formal statements in `Research/Structural.lean`:

```lean
theorem allPatternsUpTo_implies_decreasing {n k : ℕ}
    (h : AllPatternsUpTo n k) : DecreasingOccursUpTo n k

theorem F_le_G (n : ℕ) : F n ≤ G n
```

## Proof / verification

Choose the reverse permutation `Fin.revPerm` among the patterns supplied by
`AllPatternsUpTo`.  Its rank comparison reverses every index comparison, so its
realizing block is strictly decreasing.  Apply this at the greatest successful
length defining `F`; `Nat.le_findGreatest` then bounds it by the greatest
successful decreasing length defining `G`.  The empty pattern proves the base
predicate needed by `Nat.findGreatest_spec`.

Lean's kernel accepts the proof with no `sorry`, `admit`, or axioms.  Frozen
sources and project metadata are in `lean/`.
