Wikipedia/RudinsConjecture: counterexample to rudins_conjecture_unique at N = 6

## Summary

The theorem `rudins_conjecture_unique` is false as currently stated. This is a
counterexample to the repository's literal uniqueness formalization, not to
Rudin's original `O(sqrt N)` conjecture or to the strong claim that `24n + 1`
attains the maximum.

This follows up on #2282 and the merged implementation in #4434. The affected
declaration is here:

https://github.com/google-deepmind/formal-conjectures/blob/e923379e609b9d5987011a1d1f06ec22ea25cd20/FormalConjectures/Wikipedia/RudinsConjecture.lean#L112-L120

## Finite counterexample

Take

- `N = 6`
- `q = 120`
- `a = 49`

The first six terms of `120n + 49` are

```
49, 169, 289, 409, 529, 649.
```

Exactly four are squares:

```
49 = 7^2
169 = 13^2
289 = 17^2
529 = 23^2
```

The other two are not squares because

```
20^2 < 409 < 21^2
25^2 < 649 < 26^2.
```

Therefore `Q 6 120 49 = 4`. Also `Nat.Coprime 120 49`, so `(120, 49)`
satisfies `IsNontrivial`.

## Why this progression is extremal

The file already proves `Q 6 24 1 = 4` in `Q_six_twentyfour_one`.
González-Jiménez and Xarles prove the strong equality

`Q(N) = Q(N; 24, 1)` for `6 <= N <= 52`:

https://arxiv.org/abs/1301.5122

Consequently `Qmax 6 = 4`, and hence

```
Q 6 120 49 = Qmax 6
```

while `120 != 24`. This contradicts the conclusion of
`rudins_conjecture_unique`.

## Scope and suggested correction

The cited uniqueness formulation is qualified by "up to equivalence" and has
more restricted scope. The current Lean theorem drops the equivalence relation
and asserts the literal conclusion `q = 24` for every `N >= 6`.

A safe correction would be to remove `rudins_conjecture_unique` until the
intended equivalence relation and source-accurate range are formalized, or to
restate it with those conditions. `rudins_conjecture` and
`rudins_conjecture_strong` are unaffected by this counterexample.

## AI assistance disclosure

OpenAI Codex assisted with the counterexample search, exact arithmetic
verification, comparison with the cited paper, and preparation of this report.
The account holder directed the investigation and authorized publication. The
displayed finite certificate and the literature-based extremality step should
receive normal independent review.

Read FormalConjectures/Wikipedia/RudinsConjecture.lean at rudins_conjecture_unique and review the linked follow-up issues #2282 and #4434. Verify the stated N = 6 counterexample and determine whether the theorem should be removed or restated with the intended equivalence and range. The affected Lean file should check successfully with the corrected declaration.

Written by the indexing model from the issue text.