Formalize Conjecture 7.1 on the local structure of fusible numbers (Erickson–Nivasch–Xu) in Lean 4

With `IsFusible : ℚ → Prop` the smallest predicate containing $0$ and closed under $a\sim b=(a+b+1)/2$ whenever $|a-b|<1$, prove (currently a `sorry`): ``` 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) ``` Meaning: for consecutive fusible numbers $x<y$ (no fusible strictly between), the fusible numbers in each dyadic sub-interval $[\ell_n,\ell_{n+1})$ of $[x+1,y+1)$ are obtained by fusing a specific successor of $x$ with another fusible number — a self-similarity/structure statement (Conjecture 7.1 of the paper, reindexed as the repo documents).

Acceptance. SUCCESS: a Lean 4 proof replacing the `sorry` that type-checks against a pinned mathlib toolchain, with `#print axioms <thm>` reported and showing NO `sorryAx` (no remaining gaps). Expected pure-kernel: the only axioms should be `[propext, Classical.choice, Quot.sound]`; state explicitly that this holds. Genuinely open: a full proof resolves it; a rigorous counterexample (disproof of the formalized statement) is also a first-class result. Progress on special cases / small $n$ counts as partial.