FormalConjectures/ErdosProblems/354.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

4 declarations, 2 contain sorry, 0 declared as axioms

Erdős Problem 354

Reference: erdosproblems.com/354

Imports (1)
  1. def Erdos354.FloorMultiples The sequence ⌊a⌋, ⌊γ * a⌋, ⌊γ ^ 2 * a⌋, ..., ⌊γ ^ i * a⌋, ... line 30 source

    Source documentation

    The sequence ⌊a⌋, ⌊γ * a⌋, ⌊γ ^ 2 * a⌋, ..., ⌊γ ^ i * a⌋, ....

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Real, Nat, Int

    Proof uses: Int.floor, HMul.hMul, HPow.hPow

    9 instances, coercions and auxiliary constants left out.

    noncomputable def FloorMultiples (a γ : ℝ) (n : ℕ) : ℤ := ⌊γ ^ n * a⌋
  2. def Erdos354.FloorMultiples.interleave The sequence `⌊a⌋, ⌊b⌋, ⌊γ * a⌋, ⌊γ * b⌋, line 33 source

    Source documentation

    The sequence ⌊a⌋, ⌊b⌋, ⌊γ * a⌋, ⌊γ * b⌋, ... ⌊γ ^ i * a⌋, ⌊γ ^ i * b⌋, ...

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Real, Nat, Int

    Proof uses: ite, Eq, HMod.hMod, OfNat.ofNat, Erdos354.FloorMultiples, HDiv.hDiv

    6 instances, coercions and auxiliary constants left out.

    noncomputable def FloorMultiples.interleave (a b γ : ℝ) (n : ℕ) : ℤ :=
…
  3. theorem Erdos354.erdos_354.parts.i Let $\alpha,\beta\in \mathbb{R}_{>0}$ such that $\alpha/\beta$ is irrational sorry line 43 source

    Source documentation

    Let $\alpha,\beta\in \mathbb{R}_{>0}$ such that $\alpha/\beta$ is irrational. Is the multiset $$\{ \lfloor \alpha\rfloor,\lfloor 2\alpha\rfloor,\lfloor 4\alpha\rfloor,\ldots\}\cup \{ \lfloor \beta\rfloor,\lfloor 2\beta\rfloor,\lfloor 4\beta\rfloor,\ldots\}$$ complete?

    depends on sorry what this means

    Statement uses: Iff, True, Real, GT.gt, OfNat.ofNat, Irrational, HDiv.hDiv, IsAddCompleteNatSeq', Int, Erdos354.FloorMultiples.interleave, Nat

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    36 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem erdos_354.parts.i : answer(sorry) ↔ ∀ᵉ (α > 0) (β > 0), Irrational (α / β) →
    IsAddCompleteNatSeq' (FloorMultiples.interleave α β 2) := by
…

    Mentions: IsAddCompleteNatSeq', Erdos354.FloorMultiples.interleave

  4. theorem Erdos354.erdos_354.parts.ii Let $\alpha,\beta\in \mathbb{R}_{>0}$ such that $\alpha/\beta$ is irrational sorry line 51 source

    Source documentation

    Let $\alpha,\beta\in \mathbb{R}_{>0}$ such that $\alpha/\beta$ is irrational. Is $$\{ \lfloor \alpha\rfloor,\lfloor \gamma\alpha\rfloor,\lfloor \gamma^2\alpha\rfloor,\ldots\}\cup \{ \lfloor \beta\rfloor,\lfloor \gamma\beta\rfloor,\lfloor \gamma^2\beta\rfloor,\ldots\}$$ complete?

    depends on sorry what this means

    Statement uses: Iff, True, Exists, Real, And, Membership.mem, Set, Set.Ioo, OfNat.ofNat, Nat, GT.gt, Irrational, HDiv.hDiv, IsAddCompleteNatSeq', Int, Erdos354.FloorMultiples.interleave

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    44 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem erdos_354.parts.ii : answer(sorry) ↔ ∃ γ ∈ Set.Ioo (1 : ℝ) 2, ∀ᵉ (α > 0) (β > 0), Irrational (α / β) →
    IsAddCompleteNatSeq' (FloorMultiples.interleave α β γ) := by
…

    Mentions: IsAddCompleteNatSeq', Erdos354.FloorMultiples.interleave