feat: main conjecture on fusible numbers #103
Conversation
alreadydone
changed the title
| Logical Methods in Computer Science, Volume 18, Issue 3 (July 28, 2022) lmcs:8555 | ||
| -/ | ||
|
|
||
| inductive IsFusible : ℚ → Prop |
There was a problem hiding this comment.
Would you mind adding a docstring for this definition?
| inductive IsFusible : ℚ → Prop | ||
| | zero : IsFusible 0 | ||
| | fuse (a b : ℚ) : IsFusible a → IsFusible b → |a - b| < 1 → IsFusible ((a + b + 1) / 2) | ||
|
|
There was a problem hiding this comment.
I think it could also be nice to add a few "test"/API statements about this definition, e.g. proving certain known numbers are fusible, and basic results (which can be left sorried out:))
There was a problem hiding this comment.
Let's move it to the Arxiv folder.
There was a problem hiding this comment.
Should published papers be there?
There was a problem hiding this comment.
ah, if it is published, then this place is fine, let's in addition to the arxiv link also add the doi link (
https://doi.org/10.46298/lmcs-18%283%3A6%292022) or direct journal link (https://lmcs.episciences.org/9850) perhaps?
| 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 05] | ||
| theorem conj_7_1 (x y q : ℚ) (n : ℕ) (fus_x : IsFusible x) (fus_y : IsFusible y) (lt : x < y) | ||
| (nmem_Icc : ∀ z, IsFusible z → z ∉ Set.Icc x y) : |
There was a problem hiding this comment.
Something seems off here: isn't nmem_Icc x fus_ x the statement x ∉ Set.Icc x y, which is always False, making this entire conjecture empty?
Should "instead of defining y to be the successor of x, we assert that there is no fusible number between x and y;" it be something like (no_fus_between : ∀ z ∈ Set.Ioo x y, ¬ IsFusible z)?
There was a problem hiding this comment.
Good catch! It should indeed be Ioo, and switching order looks better too
Paul-Lez
added
the
Awaiting author
A conjecture by myself in a research paper.