Problems / erdos-402 / erdos-402--h3
Primitive sets with Farey quotients, division in N
erdos-402--h3
superseded
Derived by the compiler.
Superseded by erdos-402--h3-v2. Work continues on the replacement; this statement is kept for its history (D-8). The curator's record: superseded by erdos-402--h3-v2 on revision request targets/erdos-402/nodes/erdos-402--h3/revisions/20260917T171219Z-calib-402-f480.yaml (wrong-domain; D-8)
$\displaystyle 0 \notin A,\ A \ne \emptyset,\ \gcd(A) = 1,\ \bigl(\forall a, b \in A\ \exists\, u, v:\ 0 < u \le |A|,\ 0 < v \le |A|,\ \gcd(u,v) = 1,\ a v = b u\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) and the reduction to primitive sets as a hypothesis (for every finite nonempty A ⊂ ℕ with 0 ∉ A, the bound for every B of the same size with gcd(B) = 1 gives the bound for A): every finite nonempty A ⊂ ℕ with 0 ∉ A whose elements have greatest common divisor 1, and in which every pair a, b satisfies a·v = b·u for some coprime u, v with 1 ≤ u, v ≤ |A|, contains a pair with gcd(a, b) ≤ a/|A|. As written, the coercion arrows carry no target type and elaborate as the identity on ℕ, so every a/|A| here, including the one inside the second hypothesis, is natural-number division rounding down, not the rational division of the parent statement; a and b may coincide.
Lean
theorem erdos_402__h3 : (∀ (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) →
∀ (A : Finset ℕ),
0 ∉ A →
A.Nonempty →
A.gcd id = 1 →
(∀ a ∈ A, ∀ b ∈ A, ∃ u v, 0 < u ∧ u ≤ A.card ∧ 0 < v ∧ v ≤ A.card ∧ u.Coprime v ∧ a * v = b * u) →
∃ 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 `h3` 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__h3 : (∀ (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) →
∀ (A : Finset ℕ),
0 ∉ A →
A.Nonempty →
A.gcd id = 1 →
(∀ a ∈ A, ∀ b ∈ A, ∃ u v, 0 < u ∧ u ≤ A.card ∧ 0 < v ∧ v ≤ A.card ∧ u.Coprime v ∧ a * v = b * u) →
∃ 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 0 \notin A,\ A \ne \emptyset,\ \gcd(A) = 1,\ \bigl(\forall a, b \in A\ \exists\, u, v:\ 0 < u \le |A|,\ 0 < v \le |A|,\ \gcd(u,v) = 1,\ a v = b u\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) and the reduction to primitive sets as a hypothesis (for every finite nonempty A ⊂ ℕ with 0 ∉ A, the bound for every B of the same size with gcd(B) = 1 gives the bound for A): every finite nonempty A ⊂ ℕ with 0 ∉ A whose elements have greatest common divisor 1, and in which every pair a, b satisfies a·v = b·u for some coprime u, v with 1 ≤ u, v ≤ |A|, contains a pair with gcd(a, b) ≤ a/|A|. As written, the coercion arrows carry no target type and elaborate as the identity on ℕ, so every a/|A| here, including the one inside the second hypothesis, is natural-number division rounding down, not the rational division of the parent statement; a and b may coincide.
Rendered from gloss/53bce6595669….md · Improve these words →
Rendered from targets/erdos-402/nodes/erdos-402--h3/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).