ErdosProblems/486: erdos_486 is degenerate — missing activation threshold, and n = 0 admitted

erdos_486 currently reads:

theorem erdos_486 : answer(sorry) ↔
∀ X : (n : ℕ) → Set (ZMod n), ∃ d,
{m : ℕ | ∀ n, (m : ZMod n) ∉ X n}.HasLogDensity d

There are two independent problems with it, and the obvious fix for the first does not address the second.

1. The activation threshold is missing
The intended problem constrains m only by moduli n < m. In the discussion on erdosproblems.com/486 on 2026-01-11, Liam Price asked whether the site statement was right, and Terence Tao inspected [Er61, p.236] and confirmed the condition is present there as b ≥ a_i in (I.26.1). The site was corrected the same day. This file was created on 2025-12-29 (d4863de138) and edited on 2026-01-06 (a22f98abef), 2026-01-17 (1607ff44d8) and 2026-07-16 (c252a41054) without the condition being added. The docstring omits it as well.

2. n = 0 is admitted, and ZMod 0 = ℤ
Nothing constrains the modulus, so the single row X 0 ⊆ ℤ can delete an arbitrary set of naturals. This is independent of the first problem. The consequence is that erdos_486 as written asserts exactly that every subset of ℕ has a logarithmic density.

What we checked
Both points are machine-checked against this repository's own Set.HasLogDensity at 735aee074327, transcribing the right-hand side verbatim:

theorem fc_B_arbitrary (S : Set ℕ) :
{m : ℕ | ∀ n, (m : ZMod n) ∉ badX S n} = S

theorem fc_assertion_iff_all_sets :
FCAssertion ↔ ∀ S : Set ℕ, ∃ d, S.HasLogDensity d

where badX S 0 = {z : ℤ | ∃ m : ℕ, m ∉ S ∧ (m : ℤ) = z} and every other row is empty.
Adding only the threshold does not repair it, since 0 < m leaves n = 0 active:

theorem fc_thresholded_B_arbitrary (S : Set ℕ) (hS : 0 ∉ S) :
{m : ℕ | 0 < m ∧ ∀ n, n < m → (m : ZMod n) ∉ badX S n} = S

Proposed statement
Both guards are needed:

theorem erdos_486 : answer(sorry) ↔
∀ X : (n : ℕ) → Set (ZMod n), ∃ d,
{m : ℕ | 0 < m ∧ ∀ n, 0 < n → n < m →
(m : ZMod n) ∉ X n}.HasLogDensity d

with the docstring restored to "for every n with m > n".

Worth noting that erdos_25 in this repository, the singleton special case of this same problem, already carries both guards, via ∀ i, 0 < seq_n i and the (x : ℤ) < seq_n i ∨ … disjunct. (Its threshold activates at x ≥ seq_n i rather than x > seq_n i, a one-element boundary difference that cannot affect a logarithmic density.) So the general case and its own special case currently disagree.

Artifacts
The theorems above, their axiom output, and build instructions are at
https://github.com/ibrahimmian36/Pilus/blob/main/tools/MR486Defect.lean

A corrected file is at
https://github.com/ibrahimmian36/Pilus/blob/main/fc-fix/486.lean
It compiles against 735aee07 with only the expected sorry warning. We also checked that the fix closes the hole rather than merely appearing to: with the 0 < n guard, row X 0 is provably never consulted, so it can be set to all of ℤ without changing the survivor set by one element
(https://github.com/ibrahimmian36/Pilus/blob/main/tools/MR486FixCheck.lean).

We are leaving the patch here rather than opening a PR, since we publish audit findings about this repository and staying outside the contributor relationship keeps that clean. Both files are Apache-2.0 and yours to use without attribution or conditions. If you would prefer a PR, say so and we will open one.

One caution
A machine-checked negative resolution of the corrected statement has been claimed (ShouqiaoW/erdos, 486/), and we have independently verified it: https://github.com/ibrahimmian36/Pilus/blob/main/reports/erdos-486.md

It does not resolve erdos_486 as currently written, and should not be recorded as doing so. Fixing the statement is a precondition for any resolution PR against this file.

Inspect the erdos_486 declaration and its docstring, then compare them with fc-fix/486.lean. Review tools/MR486Defect.lean and tools/MR486FixCheck.lean for the checked defect and build instructions. Done means both guards appear in the theorem and the docstring states the corrected condition, with the file compiling against the referenced commit.

Written by the indexing model from the issue text.