The Oxford Invariants Puzzle Challenges - Summer 2021, Week 3, Problem 1

Original statement

Let n ≥ 3, a₁, ..., aₙ be strictly positive integers such that aᵢ ∣ aᵢ₋₁ + aᵢ₊₁ for i = 2, ..., n - 1. Show that $\sum_{i=1}^{n-1}\dfrac{a_0a_n}{a_ia_{i+1}} ∈ \mathbb N$.

Comments

Mathlib is based on type theory, so saying that a rational is a natural doesn't make sense. Instead, we ask that there exists b : ℕ whose cast to α is the sum we want.

In mathlib, ℕ starts at 0. To make the indexing cleaner, we use a₀, ..., aₙ₋₁ instead of a₁, ..., aₙ. Similarly, it's nicer to not use subtraction of naturals, so we replace aᵢ ∣ aᵢ₋₁ + aᵢ₊₁ by aᵢ₊₁ ∣ aᵢ + aᵢ₊₂.

We don't actually have to work in ℚ or ℝ. We can be even more general by stating the result for any linearly ordered field.

Instead of having n naturals, we use a function a : ℕ → ℕ.

In the proof itself, we replace n : ℕ, 1 ≤ n by n + 1.

The statement is actually true for n = 0, 1 (n = 1, 2 before the reindexing) as the sum is simply 0 and 1 respectively. So the version we prove is slightly more general.

Overall, the indexing is a bit of a mess to understand. But, trust Lean, it works.

Formalised statement

Let n : ℕ, a : ℕ → ℕ, ∀ i ≤ n, 0 < a i, ∀ i, i + 2 ≤ n → aᵢ₊₁ ∣ aᵢ + aᵢ₊₂ (read → as "implies"). Then there exists b : ℕ such that b as an element of any linearly ordered field equals $\sum_{i=0}^{n-1} (a_0 a_n) / (a_i a_{i+1})$.

Proof outline

The case n = 0 is trivial.

For n + 1, we prove the result by induction but by adding aₙ₊₁ ∣ aₙ * b - a₀ to the induction hypothesis, where b is the previous sum, $\sum_{i=0}^{n-1} (a_0 a_n) / (a_i a_{i+1})$, as a natural.

• Base case:
  • $\sum_{i=0}^0 (a_0 a_{0+1}) / (a_0 a_{0+1})$ is a natural: $\sum_{i=0}^0 (a_0 a_{0+1}) / (a_0 a_{0+1}) = (a_0 a_1) / (a_0 a_1) = 1$.
  • Divisibility condition: a₀ * 1 - a₀ = 0 is clearly divisible by a₁.
• Induction step:
  • $\sum_{i=0}^n (a_0 a_{n+1}) / (a_i a_{i+1})$ is a natural: $$\sum_{i=0}^{n+1} (a_0 a_{n+2}) / (a_i a_{i+1}) = \sum_{i=0}^n\ (a_0 a_{n+2}) / (a_i a_{i+1}) + (a_0 a_{n+2}) / (a_{n+1} a_{n+2}) = a_{n+2} / a_{n+1} × \sum_{i=0}^n (a_0 a_{n+1}) / (a_i a_{i+1}) + a_0 / a_{n+1} = a_{n+2} / a_{n+1} × b + a_0 / a_{n+1} = (a_n + a_{n+2}) / a_{n+1} × b - (a_n b - a_0)(a_{n+1})$$ which is a natural because (aₙ + aₙ₊₂)/aₙ₊₁, b and (aₙ * b - a₀)/aₙ₊₁ are (plus an annoying inequality, or the fact that the original sum is positive because its terms are).
  • Divisibility condition: aₙ₊₁ * ((aₙ + aₙ₊₂)/aₙ₊₁ * b - (aₙ * b - a₀)/aₙ₊₁) - a₀ = aₙ₊₁aₙ₊₂b is divisible by aₙ₊₂.

theorem OxfordInvariants.Week3P1 {α : Type u_1} [LinearOrderedField α] (n : ℕ) (a : ℕ → ℕ) (a_pos : ∀ i ≤ n, 0 < a i) (ha : ∀ (i : ℕ), i + 2 ≤ n → a (i + 1) ∣ a i + a (i + 2)) : ∃ (b : ℕ), ↑b = (Finset.range n).sum fun (i : ℕ) => ↑(a 0) * ↑(a n) / (↑(a i) * ↑(a (i + 1)))