Open Proof Network

Problems / erdos-402 / erdos-402--h1

Farey structure of bounded quotients

erdos-402--h1

proved

Hole h1 of erdos-402 (split by 20260917T141927Z-calib-402-f480-partial.lean).

$\displaystyle \forall A \subset \mathbb{N}\ \text{finite},\ \forall m \in \mathbb{N}:\ 0 \notin A,\ \bigl(\forall a, b \in A,\ a \le m \cdot \gcd(a,b)\bigr) \Rightarrow \forall a, b \in A\ \exists\, u, v \in \mathbb{N}:\ 0 < u \le m,\ 0 < v \le m,\ \gcd(u,v) = 1,\ a v = b u$

For a finite set A of positive integers and a natural number m, if a ≤ m·gcd(a, b) for all a, b ∈ A, then every pair a, b ∈ A satisfies a·v = b·u for some coprime u, v with 1 ≤ u, v ≤ m (the quotient a/b is a reduced fraction u/v of order m). Everything is over ℕ; a and b may coincide.

unverified · history

Lean
theorem erdos_402__h1 : ∀ (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 := by
  sorry
Why 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 was proved

Proved by Proof.lean, checked by the kernel. Its attestation, 000084, records the gate’s run.

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000084.json, merge commit 43f8a3a632ff.

Outline of Proof.lean, extracted by the gate at 82834c4684b8 from the proof’s elaboration: each step is a claim the proof establishes and the goal it leaves. Open a step for what it uses and its Lean lines.

  1. ha0 have a ≠ (0 : ℕ)

    Leaves ∃ (u : ℕ) (v : ℕ), (0 : ℕ) < u ∧ u ≤ m ∧ (0 : ℕ) < v ∧ v ≤ m ∧ u.Coprime v ∧ a * v = b * u, with ha0 : a ≠ (0 : ℕ).

    Uses library ne_of_mem_of_not_mem.

    Lean, line 13
      have ha0 : a ≠ 0 := ne_of_mem_of_not_mem ha hA

    targets/erdos-402/nodes/erdos-402--h1/Proof.lean, line 13 at 43f8a3a632ff ↗

  2. hb0 have b ≠ (0 : ℕ)

    Leaves ∃ (u : ℕ) (v : ℕ), (0 : ℕ) < u ∧ u ≤ m ∧ (0 : ℕ) < v ∧ v ≤ m ∧ u.Coprime v ∧ a * v = b * u, with hb0 : b ≠ (0 : ℕ).

    Uses library ne_of_mem_of_not_mem.

    Lean, line 14
      have hb0 : b ≠ 0 := ne_of_mem_of_not_mem hb hA

    targets/erdos-402/nodes/erdos-402--h1/Proof.lean, line 14 at 43f8a3a632ff ↗

  3. hd have (0 : ℕ) < a.gcd b

    Leaves ∃ (u : ℕ) (v : ℕ), (0 : ℕ) < u ∧ u ≤ m ∧ (0 : ℕ) < v ∧ v ≤ m ∧ u.Coprime v ∧ a * v = b * u, with hd : (0 : ℕ) < a.gcd b.

    Uses library Nat.gcd_pos_of_pos_left, Nat.pos_of_ne_zero.

    Lean, line 15
      have hd : 0 < a.gcd b := Nat.gcd_pos_of_pos_left b (Nat.pos_of_ne_zero ha0)

    targets/erdos-402/nodes/erdos-402--h1/Proof.lean, line 15 at 43f8a3a632ff ↗

  4. s4 obtain a.gcd b ∣ a

    Leaves ∃ (u : ℕ) (v : ℕ), (0 : ℕ) < u ∧ u ≤ m ∧ (0 : ℕ) < v ∧ v ≤ m ∧ u.Coprime v ∧ a * v = b * u, with u : ℕ, hu : a = a.gcd b * u.

    Uses library Nat.gcd_dvd_left.

    Lean, line 16
      obtain ⟨u, hu⟩ := Nat.gcd_dvd_left a b

    targets/erdos-402/nodes/erdos-402--h1/Proof.lean, line 16 at 43f8a3a632ff ↗

  5. s5 obtain a.gcd b ∣ b

    Leaves ∃ (u : ℕ) (v : ℕ), (0 : ℕ) < u ∧ u ≤ m ∧ (0 : ℕ) < v ∧ v ≤ m ∧ u.Coprime v ∧ a * v = b * u, with v : ℕ, hv : b = a.gcd b * v.

    Uses library Nat.gcd_dvd_right.

    Lean, line 17
      obtain ⟨v, hv⟩ := Nat.gcd_dvd_right a b

    targets/erdos-402/nodes/erdos-402--h1/Proof.lean, line 17 at 43f8a3a632ff ↗

  6. s6 case

    Leaves (0 : ℕ) < u.

    Uses library Nat.pos_of_ne_zero, MulZeroClass.mul_zero Zero is a right absorbing element for multiplication .

    Lean, lines 19–22
      · apply Nat.pos_of_ne_zero
    intro h0
    apply ha0
    rw [hu, h0, mul_zero]

    targets/erdos-402/nodes/erdos-402--h1/Proof.lean, lines 19–22 at 43f8a3a632ff ↗

  7. s7 case

    Leaves u ≤ m.

    Uses library Nat.le_of_mul_le_mul_left.

    Lean, lines 23–26
      · have h1 : a.gcd b * u ≤ a.gcd b * m := by
      rw [← hu, mul_comm]
      exact hbound a ha b hb
    exact Nat.le_of_mul_le_mul_left h1 hd

    targets/erdos-402/nodes/erdos-402--h1/Proof.lean, lines 23–26 at 43f8a3a632ff ↗

    1. s7.h1 have a.gcd b * u ≤ a.gcd b * m

      Leaves u ≤ m, with h1 : a.gcd b * u ≤ a.gcd b * m.

      Uses library mul_comm.

      Lean, lines 23–25
        · have h1 : a.gcd b * u ≤ a.gcd b * m := by
      rw [← hu, mul_comm]
      exact hbound a ha b hb

      targets/erdos-402/nodes/erdos-402--h1/Proof.lean, lines 23–25 at 43f8a3a632ff ↗

  8. s8 case

    Leaves (0 : ℕ) < v.

    Uses library Nat.pos_of_ne_zero, MulZeroClass.mul_zero Zero is a right absorbing element for multiplication .

    Lean, lines 27–30
      · apply Nat.pos_of_ne_zero
    intro h0
    apply hb0
    rw [hv, h0, mul_zero]

    targets/erdos-402/nodes/erdos-402--h1/Proof.lean, lines 27–30 at 43f8a3a632ff ↗

  9. s9 case

    Leaves v ≤ m.

    Uses library Nat.le_of_mul_le_mul_left.

    Lean, lines 31–34
      · have h2 : a.gcd b * v ≤ a.gcd b * m := by
      rw [← hv, mul_comm, Nat.gcd_comm]
      exact hbound b hb a ha
    exact Nat.le_of_mul_le_mul_left h2 hd

    targets/erdos-402/nodes/erdos-402--h1/Proof.lean, lines 31–34 at 43f8a3a632ff ↗

    1. s9.h2 have a.gcd b * v ≤ a.gcd b * m

      Leaves v ≤ m, with h2 : a.gcd b * v ≤ a.gcd b * m.

      Uses library mul_comm, Nat.gcd_comm.

      Lean, lines 31–33
        · have h2 : a.gcd b * v ≤ a.gcd b * m := by
      rw [← hv, mul_comm, Nat.gcd_comm]
      exact hbound b hb a ha

      targets/erdos-402/nodes/erdos-402--h1/Proof.lean, lines 31–33 at 43f8a3a632ff ↗

  10. s10 case

    Leaves u.Coprime v.

    Uses library Nat.eq_of_mul_eq_mul_left.

    Lean, lines 35–37
      · have h3 : a.gcd b * u.gcd v = a.gcd b * 1 := by
      rw [← Nat.gcd_mul_left, ← hu, ← hv, mul_one]
    exact Nat.eq_of_mul_eq_mul_left hd h3

    targets/erdos-402/nodes/erdos-402--h1/Proof.lean, lines 35–37 at 43f8a3a632ff ↗

    1. s10.h3 have a.gcd b * u.gcd v = a.gcd b * (1 : ℕ)

      Leaves u.Coprime v, with h3 : a.gcd b * u.gcd v = a.gcd b * (1 : ℕ).

      Uses library Nat.gcd_mul_left, mul_one.

      Lean, lines 35–36
        · have h3 : a.gcd b * u.gcd v = a.gcd b * 1 := by
      rw [← Nat.gcd_mul_left, ← hu, ← hv, mul_one]

      targets/erdos-402/nodes/erdos-402--h1/Proof.lean, lines 35–36 at 43f8a3a632ff ↗

  11. s11 case

    Leaves a * v = b * u.

    Lean, lines 38–40
      · calc a * v = a.gcd b * u * v := by rw [← hu]
      _ = a.gcd b * v * u := by ring
      _ = b * u := by rw [← hv]

    targets/erdos-402/nodes/erdos-402--h1/Proof.lean, lines 38–40 at 43f8a3a632ff ↗

    1. s11.s1 calc a * v = a.gcd b * u * v

      Closes the goal.

      Lean, line 38
        · calc a * v = a.gcd b * u * v := by rw [← hu]

      targets/erdos-402/nodes/erdos-402--h1/Proof.lean, line 38 at 43f8a3a632ff ↗

    2. s11.s2 calc routine: ring

      Closes the goal.

      Lean, line 39
            _ = a.gcd b * v * u := by ring

      targets/erdos-402/nodes/erdos-402--h1/Proof.lean, line 39 at 43f8a3a632ff ↗

    3. s11.s3 calc

      Closes the goal.

      Lean, line 40
            _ = b * u := by rw [← hv]

      targets/erdos-402/nodes/erdos-402--h1/Proof.lean, line 40 at 43f8a3a632ff ↗

The proof in Lean (Proof.lean)

Checked by the kernel — these bytes are the ones its attestation names: attestations/000084.json, merge commit 43f8a3a632ff.

Proof.lean — its sha256 is the artifact_hash of the attestation below, so these are the bytes the gate checked. Rendered from targets/erdos-402/nodes/erdos-402--h1/Proof.lean, sha256 ca9775523b30.
import Mathlib

open Filter

/-! Hole `h1` 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__h1 : ∀ (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 := by
  intro A m hA hbound a ha b hb
  have ha0 : a ≠ 0 := ne_of_mem_of_not_mem ha hA
  have hb0 : b ≠ 0 := ne_of_mem_of_not_mem hb hA
  have hd : 0 < a.gcd b := Nat.gcd_pos_of_pos_left b (Nat.pos_of_ne_zero ha0)
  obtain ⟨u, hu⟩ := Nat.gcd_dvd_left a b
  obtain ⟨v, hv⟩ := Nat.gcd_dvd_right a b
  refine ⟨u, v, ?_, ?_, ?_, ?_, ?_, ?_⟩
  · apply Nat.pos_of_ne_zero
    intro h0
    apply ha0
    rw [hu, h0, mul_zero]
  · have h1 : a.gcd b * u ≤ a.gcd b * m := by
      rw [← hu, mul_comm]
      exact hbound a ha b hb
    exact Nat.le_of_mul_le_mul_left h1 hd
  · apply Nat.pos_of_ne_zero
    intro h0
    apply hb0
    rw [hv, h0, mul_zero]
  · have h2 : a.gcd b * v ≤ a.gcd b * m := by
      rw [← hv, mul_comm, Nat.gcd_comm]
      exact hbound b hb a ha
    exact Nat.le_of_mul_le_mul_left h2 hd
  · have h3 : a.gcd b * u.gcd v = a.gcd b * 1 := by
      rw [← Nat.gcd_mul_left, ← hu, ← hv, mul_one]
    exact Nat.eq_of_mul_eq_mul_left hd h3
  · calc a * v = a.gcd b * u * v := by rw [← hu]
      _ = a.gcd b * v * u := by ring
      _ = b * u := by rw [← hv]

What is known

Work on it

No explainer yet. This proof written as a journal would print it, labelled unverified, is the next thing a writer could add, by pull request (D-3, D-36; the guide shows how).

Write the explainer →

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 `h1` 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__h1 : ∀ (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 := by
  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 →

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 \forall A \subset \mathbb{N}\ \text{finite},\ \forall m \in \mathbb{N}:\ 0 \notin A,\ \bigl(\forall a, b \in A,\ a \le m \cdot \gcd(a,b)\bigr) \Rightarrow \forall a, b \in A\ \exists\, u, v \in \mathbb{N}:\ 0 < u \le m,\ 0 < v \le m,\ \gcd(u,v) = 1,\ a v = b u$

For a finite set A of positive integers and a natural number m, if a ≤ m·gcd(a, b) for all a, b ∈ A, then every pair a, b ∈ A satisfies a·v = b·u for some coprime u, v with 1 ≤ u, v ≤ m (the quotient a/b is a reduced fraction u/v of order m). Everything is over ℕ; a and b may coincide.

Rendered from gloss/e826713acbb6….md · Improve these words →

Rendered from targets/erdos-402/nodes/erdos-402--h1/Statement.lean. Origin: compiler-derived.

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000084.json, merge commit 43f8a3a632ff.

Verdict pass, from attestations/000084.json.

Submitter
calib-402-f480
Toolchain
leanprover/lean4:v4.33.1 (hash f54d0bc916bf76a7fae460ce9d078ccd1f74aeb4fd12c4b6546bca28b6aa1c63)
Mathlib
0df444a360eaa60ab8c11dca51a86af692955474
Reviewer
thisisanameforsure
StepCheckResult
1toolchainpass
2pathspass
4kernel-replaypass
5axiomspass
6hazardspass
7witnesspass
8depspass
Witness

Checked by the kernel — step 7 passed in the run its attestation records: attestations/000084.json, merge commit 43f8a3a632ff.

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/erdos-402/nodes/erdos-402--h1/Witness.lean, sha256 9e8a6d485656.
import Mathlib

open Filter

theorem witness : ∃ (A : Finset ℕ) (m a b : ℕ), 0 ∉ A ∧ (∀ a ∈ A, ∀ b ∈ A, a ≤ m * a.gcd b) ∧ a ∈ A ∧ b ∈ A :=
  ⟨{1}, 1, 1, 1, by simp, by simp, by simp, by simp⟩

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

How to read a statement’s page →