/-
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 FormalConjecturesUtilMain conjecture on fusible numbers
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 : ℚ) := ⊢ IsFusible (1 / 2)
have h := IsFusible.fuse 0 0 IsFusible.zero IsFusible.zero (⊢ |0 - 0| < 1 All goals completed! 🐙)
h:IsFusible (1 / 2)⊢ IsFusible (1 / 2)
All goals completed! 🐙The rational number $1$ is fusible.
@[category test, AMS 5]
theorem isFusible_one : IsFusible (1 : ℚ) := ⊢ IsFusible 1
have h := IsFusible.fuse (1 / 2) (1 / 2) isFusible_one_half isFusible_one_half (⊢ |1 / 2 - 1 / 2| < 1 All goals completed! 🐙)
h:IsFusible 1⊢ IsFusible 1
All 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) := x:ℚ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)
All goals completed! 🐙
end FusibleNumber