FormalConjectures/Paper/FusibleNumber.lean

GitHub source file

4 declarations, 1 contain sorry, 0 declared as axioms

1. inductive FusibleNumber.IsFusible 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$ line 42 source

   Source documentation

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

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Rat

   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]

   Mentions: test, AMS

2. theorem FusibleNumber.isFusible_one_half The rational number $1/2$ is fusible line 48 source

   Source documentation

   The rational number $1/2$ is fusible.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: FusibleNumber.IsFusible, HDiv.hDiv, Rat, OfNat.ofNat

   Proof uses: HAdd.hAdd, FusibleNumber.IsFusible.fuse, FusibleNumber.IsFusible.zero, Mathlib.Meta.NormNum.isNat_lt_true, abs, HSub.hSub, Mathlib.Meta.NormNum.isNat_abs_nonneg, Mathlib.Meta.NormNum.IsInt.to_isNat, Mathlib.Meta.NormNum.isInt_sub, Int.ofNat, Eq.refl, Mathlib.Meta.NormNum.IsNat.to_isInt, Mathlib.Meta.NormNum.isNat_ofNat, Int, Bool, Bool.false, Eq.mp, Eq.trans, congrArg, Mathlib.Meta.NormNum.IsNNRat.to_eq and 9 more

   45 instances, coercions and auxiliary constants left out.

   Tactic trace: 4 steps

   Open to load the checked before-and-after goal states.

   theorem isFusible_one_half : IsFusible (1 / 2 : ℚ) := by
   …

   Mentions: FusibleNumber.IsFusible

3. theorem FusibleNumber.isFusible_one The rational number $1$ is fusible line 55 source

   Source documentation

   The rational number $1$ is fusible.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: FusibleNumber.IsFusible, OfNat.ofNat, Rat

   Proof uses: HDiv.hDiv, HAdd.hAdd, FusibleNumber.IsFusible.fuse, FusibleNumber.isFusible_one_half, Mathlib.Meta.NormNum.isNat_lt_true, abs, HSub.hSub, Mathlib.Meta.NormNum.isNat_abs_nonneg, Mathlib.Meta.NormNum.IsInt.to_isNat, Mathlib.Meta.NormNum.IsRat.to_isInt, Int.ofNat, Mathlib.Meta.NormNum.isRat_sub, Eq.refl, Mathlib.Meta.NormNum.IsNNRat.to_isRat, Mathlib.Meta.NormNum.isNNRat_div, Mathlib.Meta.NormNum.isNNRat_mul, HMul.hMul, Inv.inv, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_ofNat and 13 more

   42 instances, coercions and auxiliary constants left out.

   Tactic trace: 4 steps

   Open to load the checked before-and-after goal states.

   theorem isFusible_one : IsFusible (1 : ℚ) := by
   …

   Mentions: FusibleNumber.IsFusible

4. theorem FusibleNumber.conj_7_1 Documented declaration: conj_7_1 sorry line 72 source

   Source documentation

   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.

   depends on sorry what this means

   Statement uses: Rat, Nat, FusibleNumber.IsFusible, LT.lt, Not, Membership.mem, Set, Set.Ioo, HSub.hSub, HAdd.hAdd, OfNat.ofNat, HDiv.hDiv, HPow.hPow, Set.Ico, HMul.hMul

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   32 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   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
   …

   Mentions: FusibleNumber.IsFusible