# Verifier for Erdős Problem 415

This problem mixes an asymptotic proof question with two questions about ordering
patterns.  Verification therefore has two independent parts.

## 1. Faithful Lean statement (proof claims)

The pinned definitions are in
[`../workspace/experiments/experiment_1_formalize_patterns/lean/Research/Basic.lean`](../workspace/experiments/experiment_1_formalize_patterns/lean/Research/Basic.lean).
They type-check with:

```bash
export PATH="$HOME/.elan/bin:$HOME/.cargo/bin:$PATH"
cd workspace/experiments/experiment_1_formalize_patterns/lean
lake build
```

Line-by-line correspondence with `problem.md`:

* `OrderingPattern k = Equiv.Perm (Fin k)` has exactly `k!` elements.
* `Realizes a p` says `a i < a j ↔ p i < p j`; thus it means a **strict**
  ordering and rejects every block containing a tie.
* `totientBlock m i` is exactly `φ(m+1+i)`.
* `OccursUpTo n p` searches natural starts `m` satisfying `m+k ≤ n`.
  Writing the start as `Fin (n+1)` changes no valid start and makes the
  existential finite.
* `AllPatternsUpTo n k` quantifies over every one of the `k!` permutations.
* `F n = Nat.findGreatest (AllPatternsUpTo n) n`.  Restricting to `k≤n` is
  exact, because no positive block longer than `n` can satisfy `m+k≤n`; the
  length-zero pattern supplies the base case.
* `AsymptoticQuestion` is the standard ratio-limit interpretation: there is
  `c>0` such that `F(n)/log(log(log n)) → c` as `n→∞`.  Values at finitely many
  small `n` do not affect this limit.
* `DecreasingIsFirstMissingQuestion` says that at length `F(n)+1` the strictly
  decreasing pattern has not occurred.  This is the literal finite-cutoff
  reading of “the first pattern which fails to appear”.
* `PatternCount` and `IsMostFrequentUpTo` give an exact finite-cutoff meaning to
  “most likely”.  The phrase **“natural ordering which mimics what happens to
  φ(1),…,φ(k)” is not mathematically defined in the source**, so no guessed
  final theorem about it has been smuggled into the verifier.

### Source ambiguity

The original source is ambiguous about whether an ordering pattern may contain
equalities.  The first two pinned questions use strict patterns, consistent
with the displayed strict decreasing pattern and with the phrase `k! possible
ordering patterns`.  The final question cannot literally use only strict
patterns because `φ(1)=φ(2)=1`; a separate weak-order formalization is required
before that question can have a truth value.  Any claimed final solution must
state which interpretation it resolves rather than exploiting this ambiguity.

A theorem counts only if `lake build` succeeds and its source contains no
`sorry`, `admit`, `axiom`, or `unsound` escape hatch.  Type-checking the
propositions above pins the target; it does not by itself answer them.

## 2. Exact finite counterexample checker

`check-erdos-415` independently verifies a finite witness disproving the strict
version of the “decreasing is first missing” claim.  It shares no source with a
candidate generator.

Candidate format: exactly three whitespace-separated nonnegative integers

```text
n  claimed_F_n  decreasing_start_m
```

The checker:

1. computes every `φ(1),…,φ(n)` by an exact Euler sieve;
2. exhaustively scans blocks and encodes a tie-free block by its vector of
   ranks;
3. compares the number of distinct observed patterns with `k!` to determine
   the first failed length and hence `F(n)`;
4. checks the claimed value of `F(n)`; and
5. checks `m+F(n)+1≤n` and every adjacent strict decrease in the witness block.

The first failed length really determines `F`: if all patterns of length
`k+1` occur, extend any desired length-`k` pattern by appending a new largest
rank and restrict its occurrence to the first `k` positions.  Thus all
length-`k` patterns occur too.

Build and cross-check the checker with:

```bash
cd check_answer
cargo test --release
cargo run --release -- path/to/candidate.txt
```

Exit code 0 and a line beginning `PASS:` mean acceptance; every malformed or
false candidate exits nonzero with `FAIL:`.  The test suite cross-validates the
sieve against the defining gcd count through 1000.  Arithmetic is integer-only;
there is no floating point or sampling.  The documented resource ceiling is
`n≤200,000,000`.
