Open Proof Network

Problems / erdos-69 / spec-13f68833

Linear bound on omega bounds the tail by 2C

spec-13f68833 Opn.erdos_69_tail_le_of_linear_bound

proved

Proposed by a contributor.

$\displaystyle \forall n\in\mathbb{N},\ C\in\mathbb{R}:\quad \Bigl(\forall k\in\mathbb{N},\ \omega(n+1+k) \le C\,(k+1)\Bigr) \Rightarrow \sum_{j=0}^{\infty}\frac{\omega(n+1+j)}{2^{j+1}} \le 2C$

If, for a natural n and a real C, ω(n+1+k) ≤ C(k+1) for every natural k, then the tail ∑_{j≥0} ω(n+1+j)/2^{j+1} is at most 2C, with ω(n) the number of distinct prime factors of n. Every series is Mathlib's tsum over ℝ, which is 0 when the family is not summable.

unverified · history

Lean
theorem Opn.erdos_69_tail_le_of_linear_bound :
    ∀ (n : ℕ) (C : ℝ), (∀ k : ℕ, (ω (n + 1 + k) : ℝ) ≤ C * ((k : ℝ) + 1)) →
      ∑' j : ℕ, (ω (n + 1 + j) : ℝ) / 2 ^ (j + 1) ≤ 2 * C := 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, 000303, records the gate’s run.

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000303.json, merge commit a62c60747cb1.

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. hr have ‖(1 / 2 : ℝ)‖ < (1 : ℝ) routine: norm_num

    Leaves ∑' (j : ℕ), (↑((ω : ℕ → ℕ) (n + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) ≤ (2 : ℝ) * C, with hr : ‖(1 / 2 : ℝ)‖ < (1 : ℝ).

    Lean, line 18
      have hr : ‖(1 / 2 : ℝ)‖ < 1 := by norm_num

    targets/erdos-69/nodes/spec-13f68833/Proof.lean, line 18 at a62c60747cb1 ↗

  2. hS have HasSum (fun (j : ℕ) => ((↑j : ℝ) + (1 : ℝ)) * (1 / 2 : ℝ) ^ (j + (1 : ℕ))) (2 : ℝ)

    Leaves ∑' (j : ℕ), (↑((ω : ℕ → ℕ) (n + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) ≤ (2 : ℝ) * C, with hS : HasSum (fun (j : ℕ) => ((↑j : ℝ) + (1 : ℝ)) * (1 / 2 : ℝ) ^ (j + (1 : ℕ))) (2 : ℝ).

    Uses library HasSum HasSum f a L means that the (potentially infinite) sum of the f b for b : β converges to a along the SummationFilter L. , Nat.cast_add, Nat.cast_one.

    Lean, lines 20–26
      have hS : HasSum (fun j : ℕ => ((j : ℝ) + 1) * (1 / 2 : ℝ) ^ (j + 1)) 2 := by
    have h0 := hasSum_coe_mul_geometric_of_norm_lt_one hr
    have h1 := (hasSum_nat_add_iff' 1).mpr h0
    have e : (1 / 2 : ℝ) / (1 - 1 / 2) ^ 2 - ∑ i ∈ Finset.range 1, (i : ℝ) * (1 / 2) ^ i = 2 := by
      norm_num
    rw [e] at h1
    simpa [Nat.cast_add, Nat.cast_one] using h1

    targets/erdos-69/nodes/spec-13f68833/Proof.lean, lines 20–26 at a62c60747cb1 ↗

    1. hS.h0 have HasSum (fun (n : ℕ) => (↑n : ℝ) * (1 / 2 : ℝ) ^ n) ((1 / 2 : ℝ) / ((1 : ℝ) - (1 / 2 : ℝ)) ^ (2 : ℕ))

      Leaves HasSum (fun (j : ℕ) => ((↑j : ℝ) + (1 : ℝ)) * (1 / 2 : ℝ) ^ (j + (1 : ℕ))) (2 : ℝ), with h0 : HasSum (fun (n : ℕ) => (↑n : ℝ) * (1 / 2 : ℝ) ^ n) ((1 / 2 : ℝ) / ((1 : ℝ) - (1 / 2 : ℝ)) ^ (2 : ℕ)).

      Uses library hasSum_coe_mul_geometric_of_norm_lt_one If ‖r‖ < 1, then ∑' n : ℕ, n * r ^ n = r / (1 - r) ^ 2, HasSum version. .

      Lean, line 21
          have h0 := hasSum_coe_mul_geometric_of_norm_lt_one hr

      targets/erdos-69/nodes/spec-13f68833/Proof.lean, line 21 at a62c60747cb1 ↗

    2. hS.h1 have HasSum (fun (n : ℕ) => (↑(n + (1 : ℕ)) : ℝ) * (1 / 2 : ℝ) ^ (n + (1 : ℕ))) ((1 / 2 : ℝ) / ((1 : ℝ) - (1 / 2 : ℝ)) ^ (2 : ℕ) - ∑ i ∈ Finset.range (1 : ℕ), (↑i : ℝ) * (1 / 2 : ℝ) ^ i)

      Leaves HasSum (fun (j : ℕ) => ((↑j : ℝ) + (1 : ℝ)) * (1 / 2 : ℝ) ^ (j + (1 : ℕ))) (2 : ℝ), with h1 : HasSum (fun (n : ℕ) => (↑(n + (1 : ℕ)) : ℝ) * (1 / 2 : ℝ) ^ (n + (1 : ℕ))) ((1 / 2 : ℝ) / ((1 : ℝ) - (1 / 2 : ℝ)) ^ (2 : ℕ) - ∑ i ∈ Finset.range (1 : ℕ), (↑i : ℝ) * (1 / 2 : ℝ) ^ i).

      Uses library hasSum_nat_add_iff'.

      Lean, line 22
          have h1 := (hasSum_nat_add_iff' 1).mpr h0

      targets/erdos-69/nodes/spec-13f68833/Proof.lean, line 22 at a62c60747cb1 ↗

    3. hS.e have (1 / 2 : ℝ) / ((1 : ℝ) - (1 / 2 : ℝ)) ^ (2 : ℕ) - ∑ i ∈ Finset.range (1 : ℕ), (↑i : ℝ) * (1 / 2 : ℝ) ^ i = (2 : ℝ) routine: norm_num

      Leaves HasSum (fun (j : ℕ) => ((↑j : ℝ) + (1 : ℝ)) * (1 / 2 : ℝ) ^ (j + (1 : ℕ))) (2 : ℝ), with e : (1 / 2 : ℝ) / ((1 : ℝ) - (1 / 2 : ℝ)) ^ (2 : ℕ) - ∑ i ∈ Finset.range (1 : ℕ), (↑i : ℝ) * (1 / 2 : ℝ) ^ i = (2 : ℝ).

      Uses library Finset.range range n is the set of natural numbers less than n. .

      Lean, lines 23–24
          have e : (1 / 2 : ℝ) / (1 - 1 / 2) ^ 2 - ∑ i ∈ Finset.range 1, (i : ℝ) * (1 / 2) ^ i = 2 := by
      norm_num

      targets/erdos-69/nodes/spec-13f68833/Proof.lean, lines 23–24 at a62c60747cb1 ↗

  3. hg have HasSum (fun (j : ℕ) => C * (((↑j : ℝ) + (1 : ℝ)) * (1 / 2 : ℝ) ^ (j + (1 : ℕ)))) (C * (2 : ℝ))

    Leaves ∑' (j : ℕ), (↑((ω : ℕ → ℕ) (n + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) ≤ (2 : ℝ) * C, with hg : HasSum (fun (j : ℕ) => C * (((↑j : ℝ) + (1 : ℝ)) * (1 / 2 : ℝ) ^ (j + (1 : ℕ)))) (C * (2 : ℝ)).

    Uses library HasSum HasSum f a L means that the (potentially infinite) sum of the f b for b : β converges to a along the SummationFilter L. .

    Lean, lines 27–28
      have hg : HasSum (fun j : ℕ => C * (((j : ℝ) + 1) * (1 / 2 : ℝ) ^ (j + 1))) (C * 2) :=
    hS.mul_left C

    targets/erdos-69/nodes/spec-13f68833/Proof.lean, lines 27–28 at a62c60747cb1 ↗

  4. hfg have ∀ (j : ℕ), (↑((ω : ℕ → ℕ) (n + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) ≤ C * (((↑j : ℝ) + (1 : ℝ)) * (1 / 2 : ℝ) ^ (j + (1 : ℕ)))

    Leaves ∑' (j : ℕ), (↑((ω : ℕ → ℕ) (n + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) ≤ (2 : ℝ) * C, with hfg : ∀ (j : ℕ), (↑((ω : ℕ → ℕ) (n + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) ≤ C * (((↑j : ℝ) + (1 : ℝ)) * (1 / 2 : ℝ) ^ (j + (1 : ℕ))).

    Uses library mul_assoc, mul_le_mul_of_nonneg_right.

    Lean, lines 29–36
      have hfg : ∀ j : ℕ, (ω (n + 1 + j) : ℝ) / 2 ^ (j + 1)
      ≤ C * (((j : ℝ) + 1) * (1 / 2 : ℝ) ^ (j + 1)) := by
    intro j
    have hp : (0 : ℝ) ≤ (1 / 2 : ℝ) ^ (j + 1) := by positivity
    have e : (ω (n + 1 + j) : ℝ) / 2 ^ (j + 1) = (ω (n + 1 + j) : ℝ) * (1 / 2 : ℝ) ^ (j + 1) := by
      rw [one_div_pow, div_eq_mul_one_div]
    rw [e, ← mul_assoc]
    exact mul_le_mul_of_nonneg_right (h j) hp

    targets/erdos-69/nodes/spec-13f68833/Proof.lean, lines 29–36 at a62c60747cb1 ↗

    1. hfg.hp have (0 : ℝ) ≤ (1 / 2 : ℝ) ^ (j + (1 : ℕ)) routine: positivity

      Leaves (↑((ω : ℕ → ℕ) (n + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) ≤ C * (((↑j : ℝ) + (1 : ℝ)) * (1 / 2 : ℝ) ^ (j + (1 : ℕ))), with hp : (0 : ℝ) ≤ (1 / 2 : ℝ) ^ (j + (1 : ℕ)).

      Lean, line 32
          have hp : (0 : ℝ) ≤ (1 / 2 : ℝ) ^ (j + 1) := by positivity

      targets/erdos-69/nodes/spec-13f68833/Proof.lean, line 32 at a62c60747cb1 ↗

    2. hfg.e have (↑((ω : ℕ → ℕ) (n + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) = (↑((ω : ℕ → ℕ) (n + (1 : ℕ) + j)) : ℝ) * (1 / 2 : ℝ) ^ (j + (1 : ℕ))

      Leaves (↑((ω : ℕ → ℕ) (n + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) ≤ C * (((↑j : ℝ) + (1 : ℝ)) * (1 / 2 : ℝ) ^ (j + (1 : ℕ))), with e : (↑((ω : ℕ → ℕ) (n + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) = (↑((ω : ℕ → ℕ) (n + (1 : ℕ) + j)) : ℝ) * (1 / 2 : ℝ) ^ (j + (1 : ℕ)).

      Uses library one_div_pow, div_eq_mul_one_div.

      Lean, lines 33–34
          have e : (ω (n + 1 + j) : ℝ) / 2 ^ (j + 1) = (ω (n + 1 + j) : ℝ) * (1 / 2 : ℝ) ^ (j + 1) := by
      rw [one_div_pow, div_eq_mul_one_div]

      targets/erdos-69/nodes/spec-13f68833/Proof.lean, lines 33–34 at a62c60747cb1 ↗

  5. hf0 have ∀ (j : ℕ), (0 : ℝ) ≤ (↑((ω : ℕ → ℕ) (n + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ))

    Leaves ∑' (j : ℕ), (↑((ω : ℕ → ℕ) (n + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) ≤ (2 : ℝ) * C, with hf0 : ∀ (j : ℕ), (0 : ℝ) ≤ (↑((ω : ℕ → ℕ) (n + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)).

    Lean, line 37
      have hf0 : ∀ j : ℕ, (0 : ℝ) ≤ (ω (n + 1 + j) : ℝ) / 2 ^ (j + 1) := fun j => by positivity

    targets/erdos-69/nodes/spec-13f68833/Proof.lean, line 37 at a62c60747cb1 ↗

  6. hf have Summable fun (j : ℕ) => (↑((ω : ℕ → ℕ) (n + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ))

    Leaves ∑' (j : ℕ), (↑((ω : ℕ → ℕ) (n + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) ≤ (2 : ℝ) * C, with hf : Summable fun (j : ℕ) => (↑((ω : ℕ → ℕ) (n + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)).

    Uses library Summable Summable f means that f has some (infinite) sum with respect to L. , Summable.of_nonneg_of_le Comparison test of convergence of series of non-negative real numbers. .

    Lean, lines 38–39
      have hf : Summable (fun j : ℕ => (ω (n + 1 + j) : ℝ) / 2 ^ (j + 1)) :=
    Summable.of_nonneg_of_le hf0 hfg hg.summable

    targets/erdos-69/nodes/spec-13f68833/Proof.lean, lines 38–39 at a62c60747cb1 ↗

  7. this have ∑' (b : ℕ), (↑((ω : ℕ → ℕ) (n + (1 : ℕ) + b)) : ℝ) / (2 : ℝ) ^ (b + (1 : ℕ)) ≤ C * (2 : ℝ)

    Leaves ∑' (j : ℕ), (↑((ω : ℕ → ℕ) (n + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) ≤ (2 : ℝ) * C, with this : ∑' (b : ℕ), (↑((ω : ℕ → ℕ) (n + (1 : ℕ) + b)) : ℝ) / (2 : ℝ) ^ (b + (1 : ℕ)) ≤ C * (2 : ℝ).

    Uses library hasSum_le.

    Lean, line 40
      have := hasSum_le hfg hf.hasSum hg

    targets/erdos-69/nodes/spec-13f68833/Proof.lean, line 40 at a62c60747cb1 ↗

The proof in Lean (Proof.lean)

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

Proof.lean — its sha256 is the artifact_hash of the attestation below, so these are the bytes the gate checked. Rendered from targets/erdos-69/nodes/spec-13f68833/Proof.lean, sha256 f20bdf24f9aa.
import Mathlib
import Nodes.«spec-13f68833».Context

open scoped ArithmeticFunction.omega

/-! A speculative ingredient for erdos-69 (D-29): a linear bound on `ω` bounds the tail.
If `ω (n + 1 + k) ≤ C (k + 1)` for every `k`, then the tail
`∑' j, ω (n + 1 + j) / 2^(j+1)` (the same expression the nodes under erdos-69--h2-v2 use) is at
most `2 C`, because `∑_{j ≥ 0} (j + 1) / 2^(j+1) = 2`. The literature route
(Tao–Teräväinen, arXiv:2512.01739, abstract) gives infinitely many `n` with `ω (n + k) ≪ k`
for all `k ≥ 1`; with this lemma the tails at those `n` are bounded by a constant. That is a
bridge, not the hard step. -/

theorem Opn.erdos_69_tail_le_of_linear_bound :
    ∀ (n : ℕ) (C : ℝ), (∀ k : ℕ, (ω (n + 1 + k) : ℝ) ≤ C * ((k : ℝ) + 1)) →
      ∑' j : ℕ, (ω (n + 1 + j) : ℝ) / 2 ^ (j + 1) ≤ 2 * C := by
  intro n C h
  have hr : ‖(1 / 2 : ℝ)‖ < 1 := by norm_num
  -- Σ_{j ≥ 0} (j + 1) (1/2)^(j+1) = Σ_{m ≥ 0} m (1/2)^m = 2
  have hS : HasSum (fun j : ℕ => ((j : ℝ) + 1) * (1 / 2 : ℝ) ^ (j + 1)) 2 := by
    have h0 := hasSum_coe_mul_geometric_of_norm_lt_one hr
    have h1 := (hasSum_nat_add_iff' 1).mpr h0
    have e : (1 / 2 : ℝ) / (1 - 1 / 2) ^ 2 - ∑ i ∈ Finset.range 1, (i : ℝ) * (1 / 2) ^ i = 2 := by
      norm_num
    rw [e] at h1
    simpa [Nat.cast_add, Nat.cast_one] using h1
  have hg : HasSum (fun j : ℕ => C * (((j : ℝ) + 1) * (1 / 2 : ℝ) ^ (j + 1))) (C * 2) :=
    hS.mul_left C
  have hfg : ∀ j : ℕ, (ω (n + 1 + j) : ℝ) / 2 ^ (j + 1)
      ≤ C * (((j : ℝ) + 1) * (1 / 2 : ℝ) ^ (j + 1)) := by
    intro j
    have hp : (0 : ℝ) ≤ (1 / 2 : ℝ) ^ (j + 1) := by positivity
    have e : (ω (n + 1 + j) : ℝ) / 2 ^ (j + 1) = (ω (n + 1 + j) : ℝ) * (1 / 2 : ℝ) ^ (j + 1) := by
      rw [one_div_pow, div_eq_mul_one_div]
    rw [e, ← mul_assoc]
    exact mul_le_mul_of_nonneg_right (h j) hp
  have hf0 : ∀ j : ℕ, (0 : ℝ) ≤ (ω (n + 1 + j) : ℝ) / 2 ^ (j + 1) := fun j => by positivity
  have hf : Summable (fun j : ℕ => (ω (n + 1 + j) : ℝ) / 2 ^ (j + 1)) :=
    Summable.of_nonneg_of_le hf0 hfg hg.summable
  have := hasSum_le hfg hf.hasSum hg
  linarith

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
import Nodes.«spec-13f68833».Context

open scoped ArithmeticFunction.omega

/-! A speculative ingredient for erdos-69 (D-29): a linear bound on `ω` bounds the tail.
If `ω (n + 1 + k) ≤ C (k + 1)` for every `k`, then the tail
`∑' j, ω (n + 1 + j) / 2^(j+1)` (the same expression the nodes under erdos-69--h2-v2 use) is at
most `2 C`, because `∑_{j ≥ 0} (j + 1) / 2^(j+1) = 2`. The literature route
(Tao–Teräväinen, arXiv:2512.01739, abstract) gives infinitely many `n` with `ω (n + k) ≪ k`
for all `k ≥ 1`; with this lemma the tails at those `n` are bounded by a constant. That is a
bridge, not the hard step. -/

theorem Opn.erdos_69_tail_le_of_linear_bound :
    ∀ (n : ℕ) (C : ℝ), (∀ k : ℕ, (ω (n + 1 + k) : ℝ) ≤ C * ((k : ℝ) + 1)) →
      ∑' j : ℕ, (ω (n + 1 + j) : ℝ) / 2 ^ (j + 1) ≤ 2 * C := 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 n\in\mathbb{N},\ C\in\mathbb{R}:\quad \Bigl(\forall k\in\mathbb{N},\ \omega(n+1+k) \le C\,(k+1)\Bigr) \Rightarrow \sum_{j=0}^{\infty}\frac{\omega(n+1+j)}{2^{j+1}} \le 2C$

If, for a natural n and a real C, ω(n+1+k) ≤ C(k+1) for every natural k, then the tail ∑_{j≥0} ω(n+1+j)/2^{j+1} is at most 2C, with ω(n) the number of distinct prime factors of n. Every series is Mathlib's tsum over ℝ, which is 0 when the family is not summable.

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

Rendered from targets/erdos-69/nodes/spec-13f68833/Statement.lean. Origin: authored.

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000303.json, merge commit a62c60747cb1.

Verdict pass, from attestations/000303.json.

Submitter
t0929-3
Toolchain
leanprover/lean4:v4.33.1 (hash f54d0bc916bf76a7fae460ce9d078ccd1f74aeb4fd12c4b6546bca28b6aa1c63)
Mathlib
0df444a360eaa60ab8c11dca51a86af692955474
Reviewer
none needed (calibration)
StepCheckResult
1toolchainpass
2pathspass
4kernel-replaypass
5axiomspass
6hazardspass
7witnesspass
8depspass
Witness

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

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/erdos-69/nodes/spec-13f68833/Witness.lean, sha256 cb6062de321a.
import Mathlib

open scoped ArithmeticFunction.omega

theorem witness : ∃ (n : ℕ) (C : ℝ), ∀ k : ℕ, (ω (n + 1 + k) : ℝ) ≤ C * ((k : ℝ) + 1) := by
  refine ⟨0, 2, fun k => ?_⟩
  have hsub : (0 + 1 + k).primeFactors ⊆ Finset.range (0 + 1 + k + 1) := by
    intro p hp
    have hp' := Nat.mem_primeFactors.1 hp
    exact Finset.mem_range.2 (Nat.lt_succ_of_le (Nat.le_of_dvd (by omega) hp'.2.1))
  have hcard := Finset.card_le_card hsub
  rw [Finset.card_range] at hcard
  have hω : ω (0 + 1 + k) = (0 + 1 + k).primeFactors.card := by
    rw [ArithmeticFunction.cardDistinctFactors_apply, Nat.primeFactors, List.card_toFinset]
  have h1 : ω (0 + 1 + k) ≤ 2 * (k + 1) := by omega
  have h2 : ((ω (0 + 1 + k) : ℕ) : ℝ) ≤ ((2 * (k + 1) : ℕ) : ℝ) := by exact_mod_cast h1
  push_cast at h2
  linarith

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 →

Acknowledged findings (1)

Untrusted contributor text — the prover’s justification for a finding.

Untrusted: acknowledgment of a div-zero finding at ↑(ω (n + 1 + j)) / 2 ^ (j + 1)

The real divisor 2^(j+1) is positive for every j, never 0, so no term is a junk value.

How to read this page

How to read a statement’s page →