Erdős 522: `h_unif` is unsatisfiable by measurable coefficients — the defaulted `volume` reference measure degenerates on the null set {-1, 1}

### Describe the misformalization

`Erdos522.KacCoefficients` requires each coefficient to be uniformly
distributed via `pdf.IsUniform`, with the reference measure `μ` a structure
parameter defaulting to `volume` (through `volume_tac`):

https://github.com/google-deepmind/formal-conjectures/blob/0bf1250c42e675c5677186ca6ac7f4b07655b346/FormalConjectures/ErdosProblems/522.lean#L37-L43

All four statements in the file (`erdos_522`, `erdos_522.variants.zero_one`,
`erdos_522.variants.number_real_roots`, `erdos_522.variants.yakir_solution`)
instantiate the structure with `μ` elided — e.g.
`c : KacCoefficients ({-1, 1} : Set ℂ) Ω` — so the `volume` default fires.

That default makes `h_unif` degenerate. Mathlib defines

```text
pdf.IsUniform X s ℙ μ := Measure.map X ℙ = ProbabilityTheory.cond μ s
cond μ s := (μ s)⁻¹ • μ.restrict s
```

and every coefficient set used here (`{-1, 1} ⊆ ℂ`, `{0, 1} ⊆ ℂ`,
`{-1, 1} ⊆ ℝ`) is finite, hence `volume`-null, so `μ.restrict s = 0` and
`cond volume S` is the **zero measure**. `h_unif` therefore asserts
`Measure.map (toFun i) ℙ = 0`.

But `ℙ` is a probability measure, so `Measure.map (toFun i) ℙ` is a
probability measure — in particular nonzero — whenever `toFun i` is
a.e.-measurable (`Measure.map` returns the junk value `0` exactly when the
function is not a.e.-measurable). Hence:

- every honest coefficient (an a.e.-measurable ±1 Rademacher or {0,1}
Bernoulli variable) **fails** `h_unif`;
- the only potential inhabitants of `KacCoefficients S Ω` have
non-a.e.-measurable coefficient functions.

So the `∀`-quantified statements range over no intended instance (only
measure-theoretic pathologies, if any exist), and none of the four theorems
constrains actual Kac polynomials. In particular `erdos_522` as stated is not
a faithful formalization of the almost-sure problem, and the two
`research solved` variants assert their bounds vacuously with respect to the
intended ensemble.

This is independent of #3473 / PR #3896: that fix corrected the convergence
mode (in-probability → almost-sure) but kept `h_unif` and the defaulted `μ`.

### Trivial proof/disproof

Machine-checked against current Mathlib (verified on Lean/Mathlib v4.31.0;
both `#print axioms` report exactly `[propext, Classical.choice, Quot.sound]`):

```lean
import Mathlib.MeasureTheory.Measure.Lebesgue.Complex
import Mathlib.Probability.Distributions.Uniform
import Mathlib.Probability.UniformOn

open MeasureTheory

-- (1) The defaulted reference measure degenerates: conditioning `volume` on the
-- Lebesgue-null coefficient set {-1, 1} yields the ZERO measure.
theorem cond_volume_pm_one_eq_zero :
ProbabilityTheory.cond (volume : Measure ℂ) ({-1, 1} : Set ℂ) = 0 := by
have hS : (volume : Measure ℂ) ({-1, 1} : Set ℂ) = 0 :=
((Set.finite_singleton (1 : ℂ)).insert (-1 : ℂ)).measure_zero _
unfold ProbabilityTheory.cond
rw [Measure.restrict_eq_zero.mpr hS, smul_zero]

-- (2) Hence `h_unif` (with the defaulted μ = volume) excludes every honest
-- coefficient: ANY a.e.-measurable random variable on ANY probability space
-- fails it, ±1-valued or not. (`ℙ` in 522.lean instantiates `P`.)
theorem h_unif_fails_for_aemeasurable
{Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
{f : Ω → ℂ} (hf : AEMeasurable f P) :
¬ MeasureTheory.pdf.IsUniform f ({-1, 1} : Set ℂ) P volume := by
intro h
have hmap : (Measure.map f P) Set.univ = 1 := by
rw [Measure.map_apply_of_aemeasurable hf MeasurableSet.univ]
simp
unfold MeasureTheory.pdf.IsUniform at h
rw [h, cond_volume_pm_one_eq_zero] at hmap
simp at hmap

-- (3) The suggested fix is non-degenerate: with μ := Measure.count, `h_unif`
-- says exactly that the law of the coefficient is `uniformOn {-1, 1}` — the
-- honest Rademacher law, a genuine probability measure.
example {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) (X : Ω → ℂ) :
MeasureTheory.pdf.IsUniform X ({-1, 1} : Set ℂ) P Measure.count ↔
Measure.map X P = ProbabilityTheory.uniformOn ({-1, 1} : Set ℂ) :=
Iff.rfl

example : IsProbabilityMeasure (ProbabilityTheory.uniformOn ({-1, 1} : Set ℂ)) :=
ProbabilityTheory.isProbabilityMeasure_uniformOn (Set.toFinite _) ⟨-1, by simp⟩
```

(The `{0, 1} ⊆ ℂ` and `{-1, 1} ⊆ ℝ` cases used by the variants are the same
proof with the set/field changed.)

This is a faithfulness refutation in the same sense as #3473: the point is
not that the formal statements are false in Lean, but that their hypotheses
exclude every instance the informal problem is about.

### Suggested fix

**Option A (minimal, no structure change).** Instantiate the reference
measure as the counting measure at the four statement sites:

```lean
c : KacCoefficients ({-1, 1} : Set ℂ) Ω Measure.count
```

Then `h_unif` unfolds definitionally (example (3) above) to
`Measure.map (c i) ℙ = ProbabilityTheory.uniformOn {-1, 1}` — the coefficient
law is the uniform distribution on the two points, as intended. A pleasant
side effect: since `Measure.map` junk-defaults to `0` for non-a.e.-measurable
functions and `uniformOn {-1, 1} ≠ 0`, the fixed `h_unif` automatically forces
each coefficient to be a.e.-measurable — no separate measurability field is
needed.

**Option B (structural).** Replace the `h_unif` field with an explicit
law-pinning field and drop the exposed `μ` parameter for these
discrete-coefficient problems:

```lean
h_law : ∀ i, Measure.map (toFun i) ℙ = ProbabilityTheory.uniformOn S
```

Equivalent to Option A by the `Iff.rfl` above, and removes the defaulted
parameter that is easy to elide by accident.

Either way, a cheap regression guard would be to exhibit one honest instance
(e.g. coordinate projections on a Bernoulli product space, mapped to ±1)
inhabiting the fixed structure, so the statements are known to quantify over
at least the intended objects.

### Additional context

- Mathlib defines `pdf.IsUniform` w.r.t. an arbitrary reference measure
precisely so that discrete supports can use `Measure.count`; the defect here
is only the elided `volume` default, not `pdf.IsUniform` itself.
- Other problem files that use `pdf.IsUniform` with a finite/countable support
and the defaulted `volume` would degenerate the same way; it may be worth a
repo-wide audit (we have not performed one).
- Found while building a conditional Lean development of Erdős 522 downstream;
we machine-checked the exclusion there before reporting. Happy to submit the
fix as a PR (Option A or B, plus the witness instance) if useful.

### 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 in FormalConjectures/ErdosProblems/522.lean at KacCoefficients and the four statements listed in the issue. Check the supplied machine-checked conditioning argument, then apply either the Measure.count instantiation or the explicit law-pinning approach. Done means the coefficient law is nondegenerate and a regression witness demonstrates that an intended instance inhabits the fixed structure.

Written by the indexing model from the issue text.