FormalConjectures/ErdosProblems/482.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

9 declarations, 3 contain sorry, 0 declared as axioms

Erdős Problem 482

References:

A formal Lean proof is given in an external repository, gotrevor/lean-gallery, formalized by Trevor Morris with Claude Code.

Imports (1)
  1. def Erdos482.a The sequence of the problem: $a_1 = 1$ and $a_{n+1} = \lfloor \sqrt{2}(a_n + 1/2) \rfloor$ for $n \geq 1$ line 43 source

    Source documentation

    The sequence of the problem: $a_1 = 1$ and $a_{n+1} = \lfloor \sqrt{2}(a_n + 1/2) \rfloor$ for $n \geq 1$. The value $a_0$ is not used.

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

    Statement uses: Nat

    2 instances, coercions and auxiliary constants left out.

    noncomputable def a : ℕ → ℕ
  | 0 => 0
  | 1 => 1
  | n + 2 => ⌊√2 * ((a (n + 1) : ℝ) + 1 / 2)⌋₊

/-- Stoll's general Graham–Pollak-type recurrence in base $g$, with real parameters $a$, $b$, and
$\varepsilon$. Its even-index differences are used to read base-$g$ digits. -/
  2. def Erdos482.generalRecurrence Stoll's general Graham–Pollak-type recurrence in base $g$, with real parameters $a$, $b$, and $\varepsilon$ line 50 source

    Source documentation

    Stoll's general Graham–Pollak-type recurrence in base $g$, with real parameters $a$, $b$, and $\varepsilon$. Its even-index differences are used to read base-$g$ digits.

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

    Statement uses: Nat, Real, Int

    2 instances, coercions and auxiliary constants left out.

    noncomputable def generalRecurrence (g : ℕ) (a b ε : ℝ) : ℕ → ℤ
  | 0 => 1
  | n + 1 =>
      if Even n then ⌊a * ((generalRecurrence g a b ε n : ℝ) + ε)⌋
      else ⌊b * ((generalRecurrence g a b ε n : ℝ) + 1 / ((g : ℝ) - 1))⌋

/-- Define a sequence by $a_1=1$ and $$a_{n+1}=\lfloor\sqrt{2}(a_n+1/2)\rfloor$$ for $n\geq 1$.
The difference $a_{2n+1}-2a_{2n-1}$ is the $n$th digit in the binary expansion of $\sqrt{2}$.

Find similar results for $\theta=\sqrt{m}$, and other algebraic numbers.

The result for $\sqrt{2}$ was obtained by Graham and Pollak [GrPo70]. The problem statement is
…

    Mentions: Erdos482.a

  3. theorem Erdos482.erdos_482 sorry line 72 source

    depends on sorry what this means

    Statement uses: And, Nat, LE.le, OfNat.ofNat, Eq, Int, HSub.hSub, Erdos482.a, HAdd.hAdd, HMul.hMul, Real.digits, HDiv.hDiv, Real, Real.sqrt, Real.ofDigits

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

    42 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  4. theorem Erdos482.erdos_482.variants.stoll_general sorry line 87 source

    depends on sorry what this means

    Statement uses: Nat, NeZero, LE.le, OfNat.ofNat, Real, LT.lt, Exists, And, Eq, HMul.hMul, Int, HSub.hSub, Erdos482.generalRecurrence, Real.digits, HDiv.hDiv, HPow.hPow, Int.floor, Real.logb

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

    60 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  5. def Erdos482.alpha The odd-step coefficient of the Rabinowitz–Gilbert/Stoll binary recurrence line 95 source

    Source documentation

    The odd-step coefficient of the Rabinowitz–Gilbert/Stoll binary recurrence.

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

    Statement uses: Real

    Proof uses: HDiv.hDiv, HMul.hMul, OfNat.ofNat, HAdd.hAdd

    12 instances, coercions and auxiliary constants left out.

    noncomputable def alpha (t : ℝ) : ℝ := 2 * (t + 1) / (t + 2)
  6. def Erdos482.beta The even-step coefficient of the Rabinowitz–Gilbert/Stoll binary recurrence line 98 source

    Source documentation

    The even-step coefficient of the Rabinowitz–Gilbert/Stoll binary recurrence.

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

    Statement uses: Real

    Proof uses: HDiv.hDiv, HAdd.hAdd, OfNat.ofNat

    10 instances, coercions and auxiliary constants left out.

    noncomputable def beta (t : ℝ) : ℝ := (t + 2) / (t + 1)
  7. def Erdos482.stollBinary Zero-based form of the Rabinowitz–Gilbert/Stoll binary recurrence: stollBinary t k is the paper's $u_{k+1}$ line 103 source

    Source documentation

    Zero-based form of the Rabinowitz–Gilbert/Stoll binary recurrence: stollBinary t k is the paper's $u_{k+1}$. At $t = \sqrt{2}$ both coefficients equal $\sqrt{2}$, and this is the sequence a shifted by one.

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

    Statement uses: Real, Nat

    2 instances, coercions and auxiliary constants left out.

    noncomputable def stollBinary (t : ℝ) : ℕ → ℕ
  | 0 => 1
  | n + 1 =>
      ⌊(if Even n then alpha t else beta t) * ((stollBinary t n : ℝ) + 1 / 2)⌋₊

/-- The binary digits of a normalized real $t \in [1, 2)$, indexed from one and including the
leading digit.  The value at index zero is padding. -/

    Mentions: Erdos482.alpha, Erdos482.beta, Erdos482.a

  8. def Erdos482.binaryDigit The binary digits of a normalized real $t \in [1, 2)$, indexed from one and including the leading digit line 110 source

    Source documentation

    The binary digits of a normalized real $t \in [1, 2)$, indexed from one and including the leading digit. The value at index zero is padding.

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

    Statement uses: Real, Nat, Fin, OfNat.ofNat

    Proof uses: Erdos482.a.match_1, Unit, Real.digits, HSub.hSub

    8 instances, coercions and auxiliary constants left out.

    noncomputable def binaryDigit (t : ℝ) : ℕ → Fin 2
  | 0 => 0
  | 1 => 1
  | k + 2 => Real.digits (t - 1) 2 k

/-- The explicit binary answer to the open-ended part [RaGi91], [St05]: for every normalized real
$t \in [1, 2)$, the recurrence with coefficients $\alpha(t) = 2(t+1)/(t+2)$ and
$\beta(t) = (t+2)/(t+1)$ reads off the binary digits of $t$, and those digits reconstruct $t$.
Unlike `erdos_482.variants.stoll_general`, the coefficients are given, not merely shown to exist. -/
@[category research solved, AMS 11,
  formal_proof using lean4 at
    "https://github.com/plby/lean-proofs/blob/33a6b9a285cb64ac276ce4d0b3a4111b82c972b6/src/latest/ErdosProblems/Erdos482.lean#L323-L332"]

    Mentions: Erdos482.alpha, Erdos482.beta, Erdos482.erdos_482.variants.stoll_general, AMS

  9. theorem Erdos482.erdos_482.variants.binary_explicit sorry line 122 source

    depends on sorry what this means

    Statement uses: Real, LE.le, OfNat.ofNat, LT.lt, Nat, And, Eq, HSub.hSub, Erdos482.stollBinary, HMul.hMul, Erdos482.binaryDigit, Real.ofDigits, HAdd.hAdd

    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.