---
id: F-007
title: Universal strict-pattern occurrence is prefix-closed in length
tier: lean
polarity: positive
depends_on: [F-001]
supersedes: []
verifier: export PATH="$HOME/.elan/bin:$PATH"; diff -u verified_math/F-007_universal-pattern-prefix-closure/lean/Research/PrefixClosure.lean workspace/experiments/experiment_1_formalize_patterns/lean/Research/PrefixClosure.lean && (cd workspace/experiments/experiment_1_formalize_patterns/lean && lake build)
date: 2026-07-11
---

## Statement

For every cutoff `n` and length `k`, if all strict patterns of length `k+1`
occur by `n`, then all strict patterns of length `k` occur by `n`:

```lean
theorem allPatternsUpTo_succ_implies (n k : ℕ)
    (h : AllPatternsUpTo n (k + 1)) : AllPatternsUpTo n k
```

Thus the successful lengths form an initial segment; in particular, an exact
census may stop at the first failed length when computing `F(n)`.

## Proof / verification

Given a desired permutation `q` of `Fin k`, extend it along
`Fin.castSuccEmb` to a permutation of `Fin (k+1)` fixing the last position.
An occurrence of that extended pattern restricts on its first `k` entries to
an occurrence of `q`; the endpoint inequality only becomes weaker.  Mathlib's
`Equiv.Perm.viaEmbedding_apply` verifies the rank comparisons.

Lean accepts the proof with no `sorry`, `admit`, or axioms.  Frozen sources are
in `lean/`.
