# Verifier for Erdős Problem 267

This is a theorem problem, so the only final verifier is the Lean 4 kernel with
Mathlib.  The pinned formal target is
[`../workspace/experiments/experiment_1_pin_statement/lean/Research/Basic.lean`](../workspace/experiments/experiment_1_pin_statement/lean/Research/Basic.lean).
The target now has a complete proof. Acceptance requires the following
warning-as-error build to succeed:

```bash
cd workspace/experiments/experiment_1_pin_statement/lean
lake --wfail build
```

## Line-by-line fidelity audit

* A function `n : ℕ → ℕ` represents the infinite sequence, with `n 0`
  corresponding to the displayed `n₁`.
* `hpos : ∀ k, 0 < n k` says that all sequence entries are positive indices.
  This is the standard meaning of an index sequence `n₁<n₂<⋯`.
* `hmono : StrictMono n` says exactly `n₁<n₂<⋯`.
* `HasRatioGap n` expands to the existence of one real `c` such that `1<c`
  and, for every `k`, `c ≤ (n (k+1):ℝ)/(n k:ℝ)`.  This is exactly the uniform
  hypothesis `n_{k+1}/n_k ≥ c>1`; casts occur before real division.
* Mathlib's `Nat.fib` begins `0,1,1,2,…`; because `hpos` excludes index zero,
  `Nat.fib (n k)` is exactly the problem's `F_{n_k}` under `F₁=F₂=1`.
* `reciprocalFibSeries n` is the real `tsum`
  `∑' k, (Nat.fib (n k):ℝ)⁻¹`, i.e. `Σ_k 1/F_{n_k}`.  Its convergence follows
  from the hypotheses and must be established rather than assumed in a final
  proof.
* Mathlib's `Irrational x` means that no rational number casts to the real
  number `x`, exactly the requested conclusion.

This audit also guards against the common weakenings: fixing `c`, restricting
`n` to a special family, assuming summability as an extra premise, or proving
only finitely many cases would not establish the pinned theorem.

## Verified result

On 2026-07-12, `lake --wfail build` completed successfully for the faithful
target. `Research/Basic.lean` imports the self-contained kernel proof in
`Research/Solution.lean`, converts the quotient ratio hypothesis using
positivity of every index, and applies the fully quantified theorem. The proof
sources contain no proof placeholders.
