Main conjecture on fusible numbers

References:

• Fusible numbers and Peano Arithmetic, by Jeff Erickson, Gabriel Nivasch, and Junyan Xu.
• Fusible numbers and Peano Arithmetic, Logical Methods in Computer Science, Volume 18, Issue 3 (July 28, 2022).

inductive FusibleNumber.IsFusible : ℚ → Prop

A rational number is fusible if it belongs to the smallest set containing $0$ and closed under the operation $$ a \sim b = \frac{a + b + 1}{2} $$ whenever $|a-b| < 1$.

• zero : IsFusible 0
• fuse (a b : ℚ) : IsFusible a → IsFusible b → |a - b| < 1 → IsFusible ((a + b + 1) / 2)

theorem FusibleNumber.isFusible_one_half : IsFusible (1 / 2)

The rational number $1/2$ is fusible.

theorem FusibleNumber.isFusible_one : IsFusible 1

The rational number $1$ is fusible.

theorem FusibleNumber.conj_7_1 (x y q : ℚ) (n : ℕ) (fus_x : IsFusible x) (fus_y : IsFusible y) (lt : x < y) (nmem_Ioo : ∀ (z : ℚ), IsFusible z → z ∉ Set.Ioo x y) : have m := y - x; have ℓ := fun (n : ℕ) => y + 1 - m / 2 ^ n; IsFusible q → q ∈ Set.Ico (ℓ n) (ℓ (n + 1)) → IsFusible (2 * q - 1 - x - (2 - 1 / 2 ^ n) * m)

If x is a fusible number and y is its successor, then the interval [x + 1, y + 1) can be divided into intervals [ℓₙ, ℓₙ₊₁), such that the fusible numbers in [ℓₙ, ℓₙ₊₁) are obtained by fusing the n + 1st successor of x with a fusible number. This formalization differs from Conjecture 7.1 in the paper in four ways: (1) it is obtained from Conjecture 7.1 by plugging in n + 1 into n, which simplifies the expressions and removes the need to assume n ≥ 1; (2) the n + 1st successor s^(n+1)(x) is replaced by the explicit value x + (2 - 1 / 2 ^ n) * m; (3) instead of defining y to be the successor of x, we assert that there is no fusible number strictly between x and y; (4) instead of using ∃ z, IsFusible z ∧ q = s^(n+1)(x) ~ z we use the value of z determined by the equality, namely z = 2 * q - 1 - s^(n+1)(x), and it is easy to see z ∈ [x + 1 - m / 2 ^ n, x + 1) as required.