---
id: F-001
title: Faithful strict-pattern formalization and finite-witness gate
tier: gate
polarity: positive
depends_on: []
supersedes: []
verifier: export PATH="$HOME/.elan/bin:$HOME/.cargo/bin:$PATH"; diff -u verified_math/F-001_verifier-formalization/lean/Research/Basic.lean workspace/experiments/experiment_1_formalize_patterns/lean/Research/Basic.lean && (cd workspace/experiments/experiment_1_formalize_patterns/lean && lake build) && (cd check_answer && cargo test --release)
date: 2026-07-11
---

## Statement

The strict-permutation interpretation of Erdős Problem 415 is pinned down by
the following machine-checked definitions:

* an ordering pattern of length `k` is a permutation of `Fin k`, interpreted as
  the rank at each position;
* a block realizes the pattern iff all pairwise strict comparisons agree;
* `OccursUpTo`, `AllPatternsUpTo`, and `F` exactly encode the cutoff
  `m+k≤n` and largest successful length;
* `AsymptoticQuestion` is the positive-constant ratio-limit formulation; and
* `DecreasingIsFirstMissingQuestion` says the decreasing length-`F(n)+1`
  pattern is absent.

The wording of the third question does not define its “natural ordering”, and
`φ(1)=φ(2)` makes a strict interpretation impossible.  The gate explicitly
records this ambiguity and defines only the unambiguous frequency statistic.

For a finite disproof of the second question, the independent Rust gate accepts
exactly a triple `n F(n) m` for which exhaustive enumeration establishes that
length `F(n)+1` is the first failed strict-pattern length while the block at
`m` is strictly decreasing.

## Proof / verification

`lake build` accepts all definitions in `lean/Research/Basic.lean`.  The
line-by-line fidelity audit is copied as `rust/README.md`.  The Rust verifier
uses an exact Euler sieve and exhaustive rank-pattern sets; its unit tests
cross-check every sieve value through 1000 against direct gcd counting and test
tie rejection.  The prefix-extension argument in the README justifies stopping
at the first failed length.

Frozen artifacts:

* `lean/` — formal definitions and pinned Mathlib manifest;
* `rust/src/main.rs` — independent finite-witness checker;
* `rust/README.md` — format, exact checks, and statement audit.
