Problems / erdos-402 / erdos-402--h2
Reduction to primitive sets, division in N
erdos-402--h2
superseded
Derived by the compiler.
Superseded by erdos-402--h2-v2. Work continues on the replacement; this statement is kept for its history (D-8). The curator's record: superseded by erdos-402--h2-v2 on revision request targets/erdos-402/nodes/erdos-402--h2/revisions/20260917T171216Z-calib-402-f480.yaml (wrong-domain; D-8)
$\displaystyle \Bigl(\forall B \subset \mathbb{N}\ \text{finite}:\ 0 \notin B,\ |B| = |A|,\ \gcd(B) = 1 \Rightarrow \exists\, a, b \in B:\ \gcd(a,b) \le \bigl\lfloor \tfrac{a}{|B|} \bigr\rfloor\Bigr) \Rightarrow \exists\, a, b \in A:\ \gcd(a,b) \le \Bigl\lfloor \frac{a}{|A|} \Bigr\rfloor$
Assuming the Farey-structure claim as a hypothesis (for every finite A ⊂ ℕ with 0 ∉ A and every m, a ≤ m·gcd(a, b) for all a, b ∈ A implies that each pair has a·v = b·u for some coprime u, v with 1 ≤ u, v ≤ m): for every finite nonempty A ⊂ ℕ with 0 ∉ A, if the bound holds for every set B of the same size whose elements have greatest common divisor 1, then it holds for A. As written, the coercion arrows carry no target type and elaborate as the identity on ℕ, so a/|B| and a/|A| are natural-number divisions rounding down, not the rational divisions of the parent statement; a and b may coincide.
Lean
theorem erdos_402__h2 : (∀ (A : Finset ℕ) (m : ℕ),
0 ∉ A →
(∀ a ∈ A, ∀ b ∈ A, a ≤ m * a.gcd b) →
∀ a ∈ A, ∀ b ∈ A, ∃ u v, 0 < u ∧ u ≤ m ∧ 0 < v ∧ v ≤ m ∧ u.Coprime v ∧ a * v = b * u) →
∀ (A : Finset ℕ),
0 ∉ A →
A.Nonempty →
(∀ (B : Finset ℕ), 0 ∉ B → B.card = A.card → B.gcd id = 1 → ∃ a ∈ B, ∃ b ∈ B, ↑(a.gcd b) ≤ ↑a / ↑B.card) →
∃ a ∈ A, ∃ b ∈ A, ↑(a.gcd b) ≤ ↑a / ↑A.card := by
sorryWhy does it end in sorry?
A statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →
How it is being proved
Superseded.
What is known
Work on it
How to contribute → · Pull requests in flight ↗ · See it in the problem’s graph →
Record
Statement: the Lean file and its words (1 version)
Statement not audited — only a problem’s root statement is audited for fidelity (D-9); the kernel checks a proof against this Lean as written.
import Mathlib
open Filter
/-! Hole `h2` of a merged partial proof, as a node (D-12 #5, D-29).
Statement generated by the gate from the assembly; immutable (D-3). -/
theorem erdos_402__h2 : (∀ (A : Finset ℕ) (m : ℕ),
0 ∉ A →
(∀ a ∈ A, ∀ b ∈ A, a ≤ m * a.gcd b) →
∀ a ∈ A, ∀ b ∈ A, ∃ u v, 0 < u ∧ u ≤ m ∧ 0 < v ∧ v ≤ m ∧ u.Coprime v ∧ a * v = b * u) →
∀ (A : Finset ℕ),
0 ∉ A →
A.Nonempty →
(∀ (B : Finset ℕ), 0 ∉ B → B.card = A.card → B.gcd id = 1 → ∃ a ∈ B, ∃ b ∈ B, ↑(a.gcd b) ≤ ↑a / ↑B.card) →
∃ a ∈ A, ∃ b ∈ A, ↑(a.gcd b) ≤ ↑a / ↑A.card := by
sorryA statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →
In words, unverified — what this statement says; written by f29-words, drafted with Claude Fable 5.1 (claude-fable-5-1), 2026-10-18; no one has read it against the Lean and signed it.
Draft · drafted, by the model named above
$\displaystyle \Bigl(\forall B \subset \mathbb{N}\ \text{finite}:\ 0 \notin B,\ |B| = |A|,\ \gcd(B) = 1 \Rightarrow \exists\, a, b \in B:\ \gcd(a,b) \le \bigl\lfloor \tfrac{a}{|B|} \bigr\rfloor\Bigr) \Rightarrow \exists\, a, b \in A:\ \gcd(a,b) \le \Bigl\lfloor \frac{a}{|A|} \Bigr\rfloor$
Assuming the Farey-structure claim as a hypothesis (for every finite A ⊂ ℕ with 0 ∉ A and every m, a ≤ m·gcd(a, b) for all a, b ∈ A implies that each pair has a·v = b·u for some coprime u, v with 1 ≤ u, v ≤ m): for every finite nonempty A ⊂ ℕ with 0 ∉ A, if the bound holds for every set B of the same size whose elements have greatest common divisor 1, then it holds for A. As written, the coercion arrows carry no target type and elaborate as the identity on ℕ, so a/|B| and a/|A| are natural-number divisions rounding down, not the rational divisions of the parent statement; a and b may coincide.
Rendered from gloss/5440b237d965….md · Improve these words →
Rendered from targets/erdos-402/nodes/erdos-402--h2/Statement.lean. Origin: compiler-derived.
Witness — its slot is open
Not checked — the witness slot is open.
83b3f76974bd./-! The witness slot for a hole (D-29, F07-R6). Replace `sorry` with an instance satisfying this statement's hypotheses; until then the node is blocked. -/ theorem witness : True := by sorry
No gloss yet: no one has written in words what this witness says (D-3 v3.30); the Lean above is the witness. How to write one →
How to read this page
No explainer yet. An explainer is a merged proof written as a journal would print it, so there is nothing to explain until this statement is proved (D-3).