Tracking: possible misformalizations found in statement audits

## Purpose

This issue tracks possible mismatches between Formal Conjectures statements
and their cited sources, together with degenerate boundary cases and a few
`answer`-semantics questions.

The initial audit was discussed on Zulip:
https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Possible.20misformalizations/with/616080167

These are triage leads, not claims that every item is a confirmed bug. For
each item, the goal is to confirm the intended statement, link any dedicated
issue/PR, and check it off here once resolved.

## Source / statement mismatches

- [ ] Optimization Constant C1a — integration interval
- [ ] Erdős 996 — Fourier coefficient index and tail norm
- [ ] Erdős 697 — reversed thresholds and the `m = 0` case
- [ ] Erdős 887 — `answer` scope and the coefficient in `rosenfeld_4`
- [ ] Erdős 918 — fixed `ω` versus a universal ordinal binder
- [ ] Erdős 1167 — omitted `κ α > r` condition
- [ ] Erdős 757 — `= 11` versus `11 ≤`
- [ ] Green 72 — apparent reversal of the intended conclusion

## Boundary cases / vacuous wrappers

- [x] Erdős 940 `large_integers` — range starts at `r = 2` — fixed by [PR #4933](https://github.com/google-deepmind/formal-conjectures/pull/4933)
- [ ] Erdős 694 — empty totient fiber makes the wrapper vacuous
- [ ] Erdős 939 — positivity of summands is missing
- [ ] Green 21 `fox_kleitman_modular` — `k = 0`

## Interpretation / `answer` semantics

- [ ] Erdős 357 weak-monotone variant — treatment of repeated values
- [ ] Self-answer / classical-choice patterns — Erdős 195, 188, 1047

## Existing tracking

- Erdős 80: #4867
- Erdős 319: #4892
- Erdős 769: #4806

## Open-PR blockers

- [ ] PR #4660 — `tsum` without `Summable` / `HasSum`
- [ ] PR #4866 — missing nondegeneracy / lattice hypotheses

- [ ] [PR #4258 — Erdős 1208](https://github.com/google-deepmind/formal-conjectures/pull/4258) — the proposed all-`d` exponent statement conflicts at `d = 2` with [arXiv:2607.05374](https://arxiv.org/abs/2607.05374), which gives a fixed power saving. The statement/status should be rechecked before merge.

- [ ] [PR #3588 — Erdős 190](https://github.com/google-deepmind/formal-conjectures/pull/3588) — `HasRainbowAP` uses 3-term progressions, while the cited problem and solution use rainbow `k`-term progressions.

## Caveat

This list was organized with AI assistance from long working notes and may
contain transcription or interpretation errors. Please treat the entries as
triage leads until each one has been checked against the source and current
Lean statement.

Start by reading the linked Zulip discussion, then inspect the current Lean statements and cited sources for one unchecked item. Confirm whether the mismatch or boundary case is real, link any dedicated issue or PR, and check the item off once the statement is resolved or tracked.

Written by the indexing model from the issue text.