# 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`.

## 3. Exact first-cutoff census checker

The independent binary `pattern_threshold` verifies a claim that `N` is the
**first** cutoff at which all strict patterns of a fixed length `k` have
appeared.  Its candidate file contains exactly:

```text
k  N
```

It independently sieves all totients through `N`, scans every length-`k` block,
rejects ties, and stores canonical rank vectors.  It requires fewer than `k!`
patterns through `N-1` and exactly `k!` through `N`, and prints every pattern
newly completed at `N`.  Run it with:

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

This binary uses a separately written sieve update and rank encoder.  Its own
tests again compare the sieve against direct gcd counting through 1000.  Limits:
`1≤k≤10`, `N≤200,000,000`.

## 4. Final answer artifacts

The strict first question is answered in
[`../workspace/experiments/experiment_2_elementary_upper_bound/lean/Research/DecreasingRunAsymptotic.lean`](../workspace/experiments/experiment_2_elementary_upper_bound/lean/Research/DecreasingRunAsymptotic.lean).
It proves, without importing the external PPT13 asymptotic,

```lean
theorem G_ratio_tendsto_zero :
  Tendsto (fun X : ℕ ↦ (G X : ℝ) / tripleLog X) atTop (𝓝 0)

theorem not_AsymptoticQuestion : ¬ AsymptoticQuestion
```

Thus `F(X)/log log log X→0`; in particular the intended positive constant does
not exist.  Reverify the complete proof chain with:

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

The strict second question is disproved by the exact accepted witness in
[`../verified_math/F-002_decreasing-not-first/`](../verified_math/F-002_decreasing-not-first/).
Run:

```bash
cd /root/snapshot
cargo run --release --bin check-erdos-415 \
  --manifest-path /root/snapshot/check_answer/Cargo.toml -- \
  /root/snapshot/verified_math/F-002_decreasing-not-first/candidate.txt
```

The final question is not literally a probability statement as written: it
specifies no sample space or cutoff quantifier, and it cannot use strict
permutations because `φ(1)=φ(2)=1`.  The project therefore pins down the two
standard cumulative-frequency readings using weak orders (equality is
remembered):

* `EventuallyNaturalIsMostFrequentK2` says that at every sufficiently large
  finite cutoff, the weak order of `(φ(1),φ(2))=(1,1)` has count at least every
  rank reference.  F-034 proves its negation, and in fact proves the stronger
  statement
  ```lean
  ∀ᶠ n : ℕ in atTop, ¬NaturalIsMostFrequentUpToK n 2.
  ```
* `LimitingNaturalIsMostFrequentK2` says that the cumulative equality,
  increase, and decrease frequencies all converge and that the equality limit
  is at least both strict-order limits.  F-034 proves its negation as well.

Failure already at `k=2` answers the proposed natural-order maximality question
**no** under either canonical asymptotic reading.  The proof does not assume or
settle the open infinitude problem `φ(n)=φ(n+1)`.  Instead, F-029--F-033 give a
self-contained truncation argument: the two-prime adjacent log-loss has six
separated residue values; adding finitely many coprime prime states cannot
raise short-interval concentration above one sixth; and the omitted
large-prime tail has arbitrarily small mean.  This yields an eventual equality
frequency below `1/3` (indeed the construction gives a coarse `3/10` bound), so
one of increase or decrease must occur more often.

Reverify the complete kernel-only third-question chain with:

```bash
export PATH="$HOME/.elan/bin:$PATH"
cd /root/snapshot/workspace/experiments/experiment_3_adjacent_equal_density/lean
lake build
cat >/tmp/AuditNaturalNegative.lean <<'EOF'
import Research.NaturalFrequencyNegative
#print axioms Erdos415.eventually_natural_not_most_frequent_K2
#print axioms Erdos415.not_EventuallyNaturalIsMostFrequentK2
#print axioms Erdos415.not_LimitingNaturalIsMostFrequentK2
EOF
lake env lean /tmp/AuditNaturalNegative.lean
```

The axiom audit reports only `propext`, `Classical.choice`, and `Quot.sound`;
there is no native evaluator or project-declared axiom.
