Books/Equidistribution: `isEquidistributedModuloOne_transcendental_three_halves_pow` is false as written — the cited source says "almost all", not "every transcendental"

## Summary

`Equidistribution.isEquidistributedModuloOne_transcendental_three_halves_pow` asserts that
**every** transcendental `x` makes `(x · (3/2)ⁿ)` equidistributed mod 1. The file's own
header cites Kuipers–Niederreiter Ch. 1 Cor. 4.2, which says **almost all** `x > 1`. Replacing
"almost all" by "every transcendental" is not a weakening of a measure-theoretic statement: it
is a different, and **false**, claim. Below is an explicit construction of a Cantor set of
real numbers `x` — of cardinality `2^ℵ₀`, hence containing transcendentals — for which
`Int.fract (x · (3/2)ⁿ) ∈ [0, 1/10]` on a set of `n` of density at least `1/8`, so the
required limiting density `1/10` fails.

https://github.com/google-deepmind/formal-conjectures/blob/638da20efd8eeeed2993fc2550fc596dc90c1ce8/FormalConjectures/Books/UniformDistributionOfSequences/Equidistribution.lean#L62-L68

```lean
/-- For any transcendental number `x`, the sequence `x * (3 / 2) ^ n` is
equidistributed modulo 1. -/
@[category research open, AMS 11]
theorem isEquidistributedModuloOne_transcendental_three_halves_pow (x : ℝ)
(hx : Transcendental ℚ x) :
IsEquidistributedModuloOne (fun n ↦ x * (3 / 2 : ℝ) ^ n) := by
sorry
```

unfolding (`FormalConjecturesForMathlib/Analysis/Equidistribution/ModOne.lean`) to

```lean
def IsEquidistributed (a b : ℝ) (s : ℕ → ℝ) : Prop :=
∀ c d, c ≤ d → Set.Icc c d ⊆ Set.Icc a b →
Filter.atTop.Tendsto (fun n => ((Finset.range n).filter
fun m => s m ∈ Set.Icc c d).card / (n : ℝ)) (𝓝 <| (d - c) / (b - a))

def IsEquidistributedModuloOne (s : ℕ → ℝ) : Prop :=
IsEquidistributed 0 1 (fun n => Int.fract (s n))
```

so the declaration claims: for every transcendental `x` and every `0 ≤ c ≤ d ≤ 1`,

```
#{ m < N : Int.fract (x · (3/2)^m) ∈ [c, d] } / N → d − c.
```

The counterexample below breaks it at `(c, d) = (0, 1/10)`.

## Counterexample

Put `λ = 3/2`, `c = 1/10`, `G = 8`, so

```
c · λ^G = (1/10)·(6561/256) = 6561/2560 = 2.562890625 ≥ 2 + c = 2.1.
```

**Construction.** Build nested closed intervals `I₀ ⊇ I₁ ⊇ …` with
`I_j = [k_j·λ^(−jG), (k_j + c)·λ^(−jG)]` for integers `k_j`, so `|I_j| = c·λ^(−jG)`.

* *Base:* `k₀ = 1`, i.e. `I₀ = [1, 1 + 1/10]`.
* *Step:* multiplying `I_j` by `λ^((j+1)G)` gives an interval `J` of length `c·λ^G`. The
integers `k` with `[k, k+c] ⊆ J` fill an interval of length at least
`c·λ^G − c − 1 = 3745/2560 ≈ 1.463 ≥ 1`, so there are **at least two** of them. Pick any
one as `k_{j+1}`; then `I_{j+1} ⊆ I_j` by construction.

**Consequences.**

1. Two admissible choices at every level, and the blocks `[k, k+c]`, `[k′, k′+c]` for
`k ≠ k′` are disjoint (`c = 1/10 < 1`), so distinct branches give disjoint intervals and
hence distinct limit points. The set of `x = ⋂_j I_j` therefore has cardinality `2^ℵ₀`.
The algebraic numbers are countable, so **some such `x` is transcendental**.
2. For any such `x` and every `j ≥ 0`, `x·λ^(jG) ∈ [k_j, k_j + c]`, so
`Int.fract (x·λ^(jG)) ∈ [0, 1/10]`.
3. Hence for every `N`,
`#{m < N : Int.fract (x·λ^m) ∈ [0, 1/10]} ≥ ⌈N/8⌉`, so every limit point of the counting
ratio is `≥ 1/8 = 0.125`. Equidistribution requires the limit to be
`(d − c)/(b − a) = 1/10 = 0.1`. Since `1/8 > 1/10`, the limit cannot be `1/10`, and
`IsEquidistributedModuloOne (fun n ↦ x * (3/2)^n)` is false for this transcendental `x`.

Nothing in the argument is special to `3/2`; any rational `λ > 1` that is not an integer
admits the same construction for a suitable `G`.

**Numeric check** (exact `Fraction` arithmetic, no floating point in any decision; 60 levels;
three branch choices; runs in well under a second):

```
lambda = 3/2, c = 1/10, G = 8
image-interval length c*lambda^G = 6561/2560 = 2.562891
>= 1+c = 1.1000 (one block) : True
>= 2+c = 2.1000 (two blocks) : True

branch all-0 : x ~ 1.01549955161749250 |I_60| = 2.994e-86
fract(x*lam^(iG)) in [0,c] for i=0..60: violations = []
branch all-1 : x ~ 1.05512276586672149 |I_60| = 2.994e-86
fract(x*lam^(iG)) in [0,c] for i=0..60: violations = []
branch mixed : x ~ 1.05363479177655939 |I_60| = 2.994e-86
fract(x*lam^(iG)) in [0,c] for i=0..60: violations = []

branch all-0 and all-1 intervals disjoint: True

over n < 480: hits in [0,1/10] = 155 (density 0.3229)
guaranteed by construction: >= ceil(N/G) = 60 (density >= 0.125)
required by equidistribution: density -> d - c = 0.1
```

The empirical density `0.3229` is comfortably above the guaranteed `0.125`, itself above the
required `0.1`. (The individual `x` printed here are the rational left endpoints of `I₆₀`, not
the transcendental limit points; they are shown only to make the intervals reproducible. The
cardinality step, not any single printed number, is what supplies a transcendental witness.)

## What is *not* claimed

The underlying mathematics is untouched. Whether `((3/2)ⁿ)` itself is equidistributed mod 1 —
the sibling declaration `isEquidistributedModuloOne_three_halves_pow`, and the question
Kuipers–Niederreiter explicitly record as unknown — remains **open**, and nothing here bears
on it. This is a statement about what the Lean declaration asserts, not a mathematical result.

## Suggested fix

The declaration is stated as an assertion, so by CONTRIBUTING's convention ("If the problem has
been solved to the negative, then `P` should be replaced with `¬ P`") the eventual form should
be negative. Pending review of the argument above, the conservative step is to stop asserting
it and ask it instead, in the style of `green_72` in
https://github.com/google-deepmind/formal-conjectures/pull/4941:

```lean
/-- Is the sequence `x * (3 / 2) ^ n` equidistributed modulo `1` for every transcendental `x`?

The reference (Chapter 1, Corollary 4.2) states equidistribution of `(x ^ n)` for *almost all*
`x > 1`, not for every transcendental `x`. -/
@[category research open, AMS 11]
theorem isEquidistributedModuloOne_transcendental_three_halves_pow :
answer(sorry) ↔ ∀ (x : ℝ), Transcendental ℚ x →
IsEquidistributedModuloOne (fun n ↦ x * (3 / 2 : ℝ) ^ n) := by
sorry
```

I have opened a PR with exactly that change. If the construction above is accepted, the
`answer(sorry)` should become `answer(False)` and the category `research solved`; I have not
made that stronger edit because the refutation is a hand argument rather than a citation or a
Lean proof. Alternatively, the "almost all" statement the source actually supports could be
recorded in its place — that one is classical, so it would be `research solved`, and I have not
tried to pin down which Kuipers–Niederreiter theorem covers `(x·θⁿ)` for fixed `θ`, as opposed
to `(xⁿ)`.

## Source/status note

The file's own header quotes Kuipers–Niederreiter: "Corollary 4.2 of Chapter 1 states that the
sequence `(x^n)` … is equidistributed modulo 1 for almost all `x > 1`", followed by "one does
not know whether sequences such as `(e^n)`, `(π^n)`, or even `((3/2)^n)` are equidistributed
modulo 1 or not". The declaration under report carries **no** citation of its own: it was added
by https://github.com/google-deepmind/formal-conjectures/pull/3609 (2026-04-13, commit
`ba885891`) as an 8-line diff whose commit message is "This would help in the decidability
question of some halting problems ;-)". Nothing else in the file's history touches it.

I did not consult the Kuipers–Niederreiter text directly; the "almost all" attribution is taken
from the file's own header. The counterexample does not depend on it.

## Duplicate check

`isEquidistributedModuloOne_transcendental`, `transcendental_three_halves`,
`UniformDistributionOfSequences`, `Kuipers`, `Niederreiter`: no issue or PR reports this. The
only issue naming this module is #4747, and it names a different declaration
(`isAccumulationPoint_three_halves_pow_exists`). Of the open PRs touching the file, #4004 is
docstring LaTeX only and #4428 touches only `isAccumulationPoint_iff_exists_subsequence_tendsto`;
#4688 and #4428 are module-system chores. Not listed in #4896, #4923 or #4927.

## Relationship to the C₅[K₄] campaign

Found while auditing `research open` declarations in the non-Wikipedia collections for
faithfulness to their cited sources. Full triage of all 131 targets, the derivation, and the
duplicate search:

https://github.com/Kuberwastaken/c5-k4/blob/aa598efc894f2ab9628ccd8019b41318f20111ac/results/expansion/live-search-2026-08-15/other-corpora-scan.md

## AI assistance disclosure

This report was prepared with AI assistance (Claude, Anthropic) for the audit, the construction,
the exact-arithmetic verification, and drafting. The submitter reviewed the declaration, the
argument, and the suggested repair, and takes responsibility for the submission.

### Choose either option
- [x] I plan on working on this issue
- [ ] This issue is up for grabs: I would like to see this misformalization fixed by somebody else

Start at FormalConjectures/Books/UniformDistributionOfSequences/Equidistribution.lean around the named declaration, then read FormalConjecturesForMathlib/Analysis/Equidistribution/ModOne.lean and the file header. Review the Cantor-set counterexample and the linked PR's proposed question form. Done means the declaration accurately reflects the supported claim and its category and answer status are settled.

Written by the indexing model from the issue text.