FormalConjectures.Paper.FusibleNumber

FormalConjectures
Paper
FusibleNumber

/-
Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

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).

namespace FusibleNumber

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

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

The rational number $1/2$ is fusible.


@[category test, AMS 5]
theorem isFusible_one_half : IsFusible (1 / 2 : ℚ) := by⊢ IsFusible (1 / 2)
  have h := IsFusible.fuse 0 0 IsFusible.zero IsFusible.zero (by⊢ |0 - 0| < 1h:IsFusible ((0 + 0 + 1) / 2)⊢ IsFusible (1 / 2) norm_numAll goals completed! 🐙h:IsFusible ((0 + 0 + 1) / 2)⊢ IsFusible (1 / 2))h:IsFusible ((0 + 0 + 1) / 2)⊢ IsFusible (1 / 2)
  norm_num at hh:IsFusible (1 / 2)⊢ IsFusible (1 / 2)
  exact hAll goals completed! 🐙

The rational number $1$ is fusible.


@[category test, AMS 5]
theorem isFusible_one : IsFusible (1 : ℚ) := by⊢ IsFusible 1
  have h := IsFusible.fuse (1 / 2) (1 / 2) isFusible_one_half isFusible_one_half (by⊢ |1 / 2 - 1 / 2| < 1h:IsFusible ((1 / 2 + 1 / 2 + 1) / 2)⊢ IsFusible 1 norm_numAll goals completed! 🐙h:IsFusible ((1 / 2 + 1 / 2 + 1) / 2)⊢ IsFusible 1)h:IsFusible ((1 / 2 + 1 / 2 + 1) / 2)⊢ IsFusible 1
  norm_num at hh:IsFusible 1⊢ IsFusible 1
  exact hAll goals completed! 🐙

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.

@[category research open, AMS 5]
theorem 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) :
    let m := y - x
    let ℓ (n : ℕ) := y + 1 - m / 2 ^ n
    IsFusible q → q ∈ Set.Ico (ℓ n) (ℓ (n + 1)) → IsFusible (2 * q - 1 - x - (2 - 1 / 2 ^ n) * m) := byx:ℚy:ℚq:ℚn:ℕfus_x:IsFusible xfus_y:IsFusible ylt:x < ynmem_Ioo:∀ (z : ℚ), IsFusible z → z ∉ Set.Ioo x y⊢ let m := y - x;
let ℓ := 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)
  sorryAll goals completed! 🐙

end FusibleNumber