# 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ₙ₊₂`

.

- $\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