Open Proof Network

Problems / erdos-257 / spec-5e2e0890--h2

lexicographic comparison of subset sums

spec-5e2e0890--h2 spec_5e2e0890__h2

proved

Hole h3 of spec-5e2e0890 (split by 20261020T203245Z-fable-1020-e257-a-partial.lean).

$\displaystyle g \ge 0 \text{ summable}, \sum_{k \ge 0} g(n+1+k) < g(n), n \in S \setminus T, S \cap [0,n) = T \cap [0,n) \implies \sum_{T} g < \sum_{S} g$

Split both sums at $n$: the parts below $n$ agree, the $S$ side has $g(n)$ in addition, and the rest of the $T$ side is a tail bounded by the gap.

unverified · history

Lean
theorem spec_5e2e0890__h2 : ∀ (A B : Set ℕ),
  (0 : ℕ) ∉ A →
    (0 : ℕ) ∉ B →
      ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) =
          ∑' (n : (↑B : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) →
        ∀ (g : ℕ → ℝ),
          Summable g →
            (∀ (m : ℕ), (0 : ℝ) ≤ g m) →
              ∀ (S T : Set ℕ),
                ∀ n ∈ S,
                  n ∉ T →
                    (∀ m < n, m ∈ S ↔ m ∈ T) →
                      ∑' (k : ℕ), g (n + (1 : ℕ) + k) < g n →
                        ∑' (m : (↑T : Type)), g (↑m : ℕ) < ∑' (m : (↑S : Type)), g (↑m : ℕ) := 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 →

Explainer

Informal account, unverified — unverified prose about a kernel-checked proof; shown section by section, each labelled with who drafted, wrote or verified it (D-3 v3.31).

Unverified: explainer, its words from explainer/221369be4391….md, written by t1022-e, drafted with Claude Opus 5.5 (claude-opus-5-5), 2026-10-22.

Overview

Draft · drafted, by the model named above

The hypotheses about $A$ and $B$ are carried along and not used. The content: let $g \ge 0$ be summable, $n \in S$, $n \notin T$, $S$ and $T$ agree on $\{m : m < n\}$, and $\sum_{k\ge0} g(n+1+k) < g(n)$. Split $T$ into its part below $n$ and its part above $n$ (it does not contain $n$), and $S$ into its part below $n$ and $\{n\}$ plus the rest. The parts below $n$ coincide; the part of $T$ above $n$ has sum at most the whole tail $\sum_{m>n} g(m) < g(n)$; so $\sum_T g < \sum_S g$.

Read it step by step (2 more sections)

Preparations

Draft · drafted, by the model named above

Every restriction of $g$ to a subset $U \subseteq \mathbb{N}$ is summable. Agreement below $n$ gives $\{m<n\}\cap S = \{m<n\}\cap T$. Since $n \notin T$, every $m \in T$ is either below $n$ or above it: $T \subseteq (\{m<n\}\cap T) \cup \{m > n\}$. In the other direction $(\{m<n\}\cap S)\cup\{n\} \subseteq S$. The sum of $g$ over $\{m > n\}$ is $\sum_{k\ge0} g(n+1+k)$, by the bijection $k \mapsto n+1+k$ from $\mathbb{N}$ onto $\{m>n\}$. Because $g \ge 0$, the sum over a subset is at most the sum over a larger set. Finally $\{m<n\}\cap T$ is disjoint from $\{m>n\}$, and $\{m<n\}\cap S$ from $\{n\}$.

The chain of inequalities

Draft · drafted, by the model named above

$$\sum_{T} g \;\le\; \sum_{\{m<n\}\cap T} g + \sum_{m>n} g(m) \;=\; \sum_{\{m<n\}\cap T} g + \sum_{k\ge0} g(n+1+k) \;<\; \sum_{\{m<n\}\cap T} g + g(n)$$ $$=\; \sum_{\{m<n\}\cap S} g + \sum_{\{n\}} g \;=\; \sum_{(\{m<n\}\cap S)\cup\{n\}} g \;\le\; \sum_S g .$$ The first and last steps are monotonicity under inclusion, the sums over unions split by disjointness, the strict step is the hypothesis $\sum_{k\ge0} g(n+1+k) < g(n)$, and the middle equality uses $\{m<n\}\cap T = \{m<n\}\cap S$ and the one-point sum $\sum_{\{n\}} g = g(n)$.

Improve these words →

History: 1 version on record

  1. 2026-10-22 · written by t1022-e, drafted with Claude Opus 5.5 (claude-opus-5-5) · not signed · current · explainer/221369be4391….md · the first version of its chain

    Read this version

    Overview

    The hypotheses about $A$ and $B$ are carried along and not used. The content: let $g \ge 0$ be summable, $n \in S$, $n \notin T$, $S$ and $T$ agree on $\{m : m < n\}$, and $\sum_{k\ge0} g(n+1+k) < g(n)$. Split $T$ into its part below $n$ and its part above $n$ (it does not contain $n$), and $S$ into its part below $n$ and $\{n\}$ plus the rest. The parts below $n$ coincide; the part of $T$ above $n$ has sum at most the whole tail $\sum_{m>n} g(m) < g(n)$; so $\sum_T g < \sum_S g$.

    Preparations (hsum hL hT_sub hS_sup htail hmono hdisj1 hdisj2)

    Every restriction of $g$ to a subset $U \subseteq \mathbb{N}$ is summable. Agreement below $n$ gives $\{m<n\}\cap S = \{m<n\}\cap T$. Since $n \notin T$, every $m \in T$ is either below $n$ or above it: $T \subseteq (\{m<n\}\cap T) \cup \{m > n\}$. In the other direction $(\{m<n\}\cap S)\cup\{n\} \subseteq S$. The sum of $g$ over $\{m > n\}$ is $\sum_{k\ge0} g(n+1+k)$, by the bijection $k \mapsto n+1+k$ from $\mathbb{N}$ onto $\{m>n\}$. Because $g \ge 0$, the sum over a subset is at most the sum over a larger set. Finally $\{m<n\}\cap T$ is disjoint from $\{m>n\}$, and $\{m<n\}\cap S$ from $\{n\}$.

    The chain of inequalities (s9 s10 s11 s12 s13 s14 s15)

    $$\sum_{T} g \;\le\; \sum_{\{m<n\}\cap T} g + \sum_{m>n} g(m) \;=\; \sum_{\{m<n\}\cap T} g + \sum_{k\ge0} g(n+1+k) \;<\; \sum_{\{m<n\}\cap T} g + g(n)$$ $$=\; \sum_{\{m<n\}\cap S} g + \sum_{\{n\}} g \;=\; \sum_{(\{m<n\}\cap S)\cup\{n\}} g \;\le\; \sum_S g .$$ The first and last steps are monotonicity under inclusion, the sums over unions split by disjointness, the strict step is the hypothesis $\sum_{k\ge0} g(n+1+k) < g(n)$, and the middle equality uses $\{m<n\}\cap T = \{m<n\}\cap S$ and the one-point sum $\sum_{\{n\}} g = g(n)$.

Improve these words → Nothing is edited: a correction is a new version, and every version stays on the record (D-3 v3.30).

How it was proved

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

The proof step by step (outline)

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

Outline of Proof.lean, extracted by the gate at f824b6fc425c 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. hsum have ∀ (U : Set ℕ), Summable fun (m : (↑U : Type)) => g (↑m : ℕ)

    Leaves ∑' (m : (↑T : Type)), g (↑m : ℕ) < ∑' (m : (↑S : Type)), g (↑m : ℕ), with hsum : ∀ (U : Set ℕ), Summable fun (m : (↑U : Type)) => g (↑m : ℕ).

    Uses library Set A set is a collection of elements of some type α. , Summable Summable f means that f has some (infinite) sum with respect to L. .

    Lean, line 23
      have hsum : ∀ U : Set ℕ, Summable (fun m : U => g m) := fun U => hg.subtype U

    targets/erdos-257/nodes/spec-5e2e0890--h2/Proof.lean, line 23 at b45cc74b68bb ↗

  2. hL have {m : ℕ | m < n} ∩ S = {m : ℕ | m < n} ∩ T

    Leaves ∑' (m : (↑T : Type)), g (↑m : ℕ) < ∑' (m : (↑S : Type)), g (↑m : ℕ), with hL : {m : ℕ | m < n} ∩ S = {m : ℕ | m < n} ∩ T.

    Uses library Set A set is a collection of elements of some type α. , Set.mem_inter_iff, Set.mem_setOf_eq Alias of Set.mem_ofPred_eq. , and_congr_right.

    Lean, lines 24–27
      have hL : ({m | m < n} ∩ S : Set ℕ) = {m | m < n} ∩ T := by
    ext m
    simp only [Set.mem_inter_iff, Set.mem_setOf_eq]
    exact and_congr_right (hagree m)

    targets/erdos-257/nodes/spec-5e2e0890--h2/Proof.lean, lines 24–27 at b45cc74b68bb ↗

  3. hT_sub have T ⊆ {m : ℕ | m < n} ∩ T ∪ {m : ℕ | n < m}

    Leaves ∑' (m : (↑T : Type)), g (↑m : ℕ) < ∑' (m : (↑S : Type)), g (↑m : ℕ), with hT_sub : T ⊆ {m : ℕ | m < n} ∩ T ∪ {m : ℕ | n < m}.

    Uses library lt_trichotomy.

    Lean, lines 28–33
      have hT_sub : T ⊆ ({m | m < n} ∩ T) ∪ {m | n < m} := by
    intro m hm
    rcases lt_trichotomy m n with hlt | rfl | hgt
    · exact Or.inl ⟨hlt, hm⟩
    · exact absurd hm hnT
    · exact Or.inr hgt

    targets/erdos-257/nodes/spec-5e2e0890--h2/Proof.lean, lines 28–33 at b45cc74b68bb ↗

    1. hT_sub.s1 case

      Leaves m ∈ {m : ℕ | m < n} ∩ T ∪ {m : ℕ | n < m}, with hlt : m < n.

      Uses library Or.inl Or.inl is "left injection" into an Or. , And.intro And.intro : a → b → a ∧ b is the constructor for the And operation. .

      Lean, line 31
          · exact Or.inl ⟨hlt, hm⟩

      targets/erdos-257/nodes/spec-5e2e0890--h2/Proof.lean, line 31 at b45cc74b68bb ↗

    2. hT_sub.s2 case

      Leaves m ∈ {m_1 : ℕ | m_1 < m} ∩ T ∪ {m_1 : ℕ | m < m_1}, with hnS : m ∈ S, hnT : m ∉ T, hagree : ∀ m_1 < m, m_1 ∈ S ↔ m_1 ∈ T, hgap : ∑' (k : ℕ), g (m + (1 : ℕ) + k) < g m, hL : {m_1 : ℕ | m_1 < m} ∩ S = {m_1 : ℕ | m_1 < m} ∩ T.

      Uses library absurd Anything follows from two contradictory hypotheses. .

      Lean, line 32
          · exact absurd hm hnT

      targets/erdos-257/nodes/spec-5e2e0890--h2/Proof.lean, line 32 at b45cc74b68bb ↗

    3. hT_sub.s3 case

      Leaves m ∈ {m : ℕ | m < n} ∩ T ∪ {m : ℕ | n < m}, with hgt : n < m.

      Uses library Or.inr Or.inr is "right injection" into an Or. .

      Lean, line 33
          · exact Or.inr hgt

      targets/erdos-257/nodes/spec-5e2e0890--h2/Proof.lean, line 33 at b45cc74b68bb ↗

  4. hS_sup have {m : ℕ | m < n} ∩ S ∪ {n} ⊆ S

    Leaves ∑' (m : (↑T : Type)), g (↑m : ℕ) < ∑' (m : (↑S : Type)), g (↑m : ℕ), with hS_sup : {m : ℕ | m < n} ∩ S ∪ {n} ⊆ S.

    Lean, lines 34–39
      have hS_sup : ({m | m < n} ∩ S) ∪ {n} ⊆ S := by
    intro m hm
    rcases hm with ⟨_, hm⟩ | hm
    · exact hm
    · rw [Set.mem_singleton_iff] at hm
      exact hm ▸ hnS

    targets/erdos-257/nodes/spec-5e2e0890--h2/Proof.lean, lines 34–39 at b45cc74b68bb ↗

    1. hS_sup.s1 case

      Leaves m ∈ S, with left✝ : m ∈ {m : ℕ | m < n}, hm : m ∈ S.

      Lean, line 37
          · exact hm

      targets/erdos-257/nodes/spec-5e2e0890--h2/Proof.lean, line 37 at b45cc74b68bb ↗

    2. hS_sup.s2 case printed form did not read back: shown as its Lean lines only
          · rw [Set.mem_singleton_iff] at hm
      exact hm ▸ hnS

      targets/erdos-257/nodes/spec-5e2e0890--h2/Proof.lean, lines 38–39 at b45cc74b68bb ↗

  5. htail have ∑' (m : (↑{m : ℕ | n < m} : Type)), g (↑m : ℕ) = ∑' (k : ℕ), g (n + (1 : ℕ) + k)

    Leaves ∑' (m : (↑T : Type)), g (↑m : ℕ) < ∑' (m : (↑S : Type)), g (↑m : ℕ), with htail : ∑' (m : (↑{m : ℕ | n < m} : Type)), g (↑m : ℕ) = ∑' (k : ℕ), g (n + (1 : ℕ) + k).

    Uses library Subtype.mk, Set.mem_setOf_eq Alias of Set.mem_ofPred_eq. , Subtype.ext, Equiv.tsum_eq.

    Lean, lines 40–52
      have htail : ∑' m : {m | n < m}, g m = ∑' k : ℕ, g (n + 1 + k) := by
    let e : ℕ ≃ {m : ℕ | n < m} :=
      { toFun := fun k => ⟨n + 1 + k, by simp only [Set.mem_setOf_eq]; omega⟩
        invFun := fun m => m.1 - (n + 1)
        left_inv := fun k => by simp only; omega
        right_inv := fun m => by
          apply Subtype.ext
          have := m.2
          simp only [Set.mem_setOf_eq] at this
          simp only
          omega }
    rw [← Equiv.tsum_eq e]
    rfl

    targets/erdos-257/nodes/spec-5e2e0890--h2/Proof.lean, lines 40–52 at b45cc74b68bb ↗

    1. htail.this have printed form did not read back: shown as its Lean lines only
                have := m.2

      targets/erdos-257/nodes/spec-5e2e0890--h2/Proof.lean, line 47 at b45cc74b68bb ↗

  6. hmono have ∀ (U V : Set ℕ), U ⊆ V → ∑' (m : (↑U : Type)), g (↑m : ℕ) ≤ ∑' (m : (↑V : Type)), g (↑m : ℕ)

    Leaves ∑' (m : (↑T : Type)), g (↑m : ℕ) < ∑' (m : (↑S : Type)), g (↑m : ℕ), with hmono : ∀ (U V : Set ℕ), U ⊆ V → ∑' (m : (↑U : Type)), g (↑m : ℕ) ≤ ∑' (m : (↑V : Type)), g (↑m : ℕ).

    Uses library Set A set is a collection of elements of some type α. , Summable.tsum_le_tsum_of_inj, Set.inclusion inclusion is the "identity" function between two subsets s and t, where s ⊆ t , Set.inclusion_injective, le_rfl A version of le_refl where the argument is implicit .

    Lean, lines 53–56
      have hmono : ∀ U V : Set ℕ, U ⊆ V → ∑' m : U, g m ≤ ∑' m : V, g m := by
    intro U V hUV
    exact Summable.tsum_le_tsum_of_inj (Set.inclusion hUV) (Set.inclusion_injective hUV)
      (fun c _ => hg0 c) (fun i => le_rfl) (hsum U) (hsum V)

    targets/erdos-257/nodes/spec-5e2e0890--h2/Proof.lean, lines 53–56 at b45cc74b68bb ↗

  7. hdisj1 have Disjoint ({m : ℕ | m < n} ∩ T) {m : ℕ | n < m}

    Leaves ∑' (m : (↑T : Type)), g (↑m : ℕ) < ∑' (m : (↑S : Type)), g (↑m : ℕ), with hdisj1 : Disjoint ({m : ℕ | m < n} ∩ T) {m : ℕ | n < m}.

    Uses library Disjoint Two elements of a lattice are disjoint if their inf is the bottom element. , Set A set is a collection of elements of some type α. , Set.disjoint_left, Set.mem_setOf_eq Alias of Set.mem_ofPred_eq. .

    Lean, lines 57–61
      have hdisj1 : Disjoint ({m | m < n} ∩ T : Set ℕ) {m | n < m} := by
    rw [Set.disjoint_left]
    rintro m ⟨hlt, _⟩ hgt
    simp only [Set.mem_setOf_eq] at hlt hgt
    omega

    targets/erdos-257/nodes/spec-5e2e0890--h2/Proof.lean, lines 57–61 at b45cc74b68bb ↗

  8. hdisj2 have Disjoint ({m : ℕ | m < n} ∩ S) {n}

    Leaves ∑' (m : (↑T : Type)), g (↑m : ℕ) < ∑' (m : (↑S : Type)), g (↑m : ℕ), with hdisj2 : Disjoint ({m : ℕ | m < n} ∩ S) {n}.

    Uses library Disjoint Two elements of a lattice are disjoint if their inf is the bottom element. , Set A set is a collection of elements of some type α. , Set.disjoint_left, Set.mem_singleton_iff, Set.mem_setOf_eq Alias of Set.mem_ofPred_eq. .

    Lean, lines 62–67
      have hdisj2 : Disjoint ({m | m < n} ∩ S : Set ℕ) {n} := by
    rw [Set.disjoint_left]
    rintro m ⟨hlt, _⟩ hm
    rw [Set.mem_singleton_iff] at hm
    simp only [Set.mem_setOf_eq] at hlt
    omega

    targets/erdos-257/nodes/spec-5e2e0890--h2/Proof.lean, lines 62–67 at b45cc74b68bb ↗

  9. s9 calc ∑' (m : (↑T : Type)), g (↑m : ℕ) ≤ ∑' (m : (↑({m : ℕ | m < n} ∩ T ∪ {m : ℕ | n < m}) : Type)), g (↑m : ℕ)

    Closes the goal.

    Lean, line 68
      calc ∑' m : T, g m ≤ ∑' m : ↥(({m | m < n} ∩ T) ∪ {m | n < m}), g m := hmono _ _ hT_sub

    targets/erdos-257/nodes/spec-5e2e0890--h2/Proof.lean, line 68 at b45cc74b68bb ↗

  10. s10 calc ∑' (m : (↑({m : ℕ | m < n} ∩ T ∪ {m : ℕ | n < m}) : Type)), g (↑m : ℕ) = ∑' (m : (↑({m : ℕ | m < n} ∩ T) : Type)), g (↑m : ℕ) + ∑' (m : (↑{m : ℕ | n < m} : Type)), g (↑m : ℕ)

    Closes the goal.

    Uses library Summable.tsum_union_disjoint.

    Lean, lines 69–70
        _ = ∑' m : ↥({m | m < n} ∩ T), g m + ∑' m : {m | n < m}, g m :=
        Summable.tsum_union_disjoint hdisj1 (hsum _) (hsum _)

    targets/erdos-257/nodes/spec-5e2e0890--h2/Proof.lean, lines 69–70 at b45cc74b68bb ↗

  11. s11 calc

    Closes the goal.

    Lean, line 71
        _ = ∑' m : ↥({m | m < n} ∩ T), g m + ∑' k : ℕ, g (n + 1 + k) := by rw [htail]

    targets/erdos-257/nodes/spec-5e2e0890--h2/Proof.lean, line 71 at b45cc74b68bb ↗

  12. s12 calc routine: linarith

    Closes the goal.

    Lean, line 72
        _ < ∑' m : ↥({m | m < n} ∩ T), g m + g n := by linarith

    targets/erdos-257/nodes/spec-5e2e0890--h2/Proof.lean, line 72 at b45cc74b68bb ↗

  13. s13 calc

    Closes the goal.

    Uses library Set A set is a collection of elements of some type α. , tsum_singleton.

    Lean, lines 73–74
        _ = ∑' m : ↥({m | m < n} ∩ S), g m + ∑' m : ({n} : Set ℕ), g m := by
        rw [hL, tsum_singleton]

    targets/erdos-257/nodes/spec-5e2e0890--h2/Proof.lean, lines 73–74 at b45cc74b68bb ↗

  14. s14 calc printed form did not read back: shown as its Lean lines only
        _ = ∑' m : ↥(({m | m < n} ∩ S) ∪ {n}), g m :=
        (Summable.tsum_union_disjoint hdisj2 (hsum _) (hsum _)).symm

    targets/erdos-257/nodes/spec-5e2e0890--h2/Proof.lean, lines 75–76 at b45cc74b68bb ↗

  15. s15 calc ∑' (m : (↑({m : ℕ | m < n} ∩ S ∪ {n}) : Type)), g (↑m : ℕ) ≤ ∑' (m : (↑S : Type)), g (↑m : ℕ)

    Closes the goal.

    Lean, line 77
        _ ≤ ∑' m : S, g m := hmono _ _ hS_sup

    targets/erdos-257/nodes/spec-5e2e0890--h2/Proof.lean, line 77 at b45cc74b68bb ↗

The proof in Lean (Proof.lean)

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

Proof.lean — its sha256 is the artifact_hash of the attestation below, so these are the bytes the gate checked. Rendered from targets/erdos-257/nodes/spec-5e2e0890--h2/Proof.lean, sha256 615a5d292dea.
import Mathlib
import Nodes.«spec-5e2e0890--h2».Context

/-! 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 spec_5e2e0890__h2 : ∀ (A B : Set ℕ),
  (0 : ℕ) ∉ A →
    (0 : ℕ) ∉ B →
      ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) =
          ∑' (n : (↑B : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) →
        ∀ (g : ℕ → ℝ),
          Summable g →
            (∀ (m : ℕ), (0 : ℝ) ≤ g m) →
              ∀ (S T : Set ℕ),
                ∀ n ∈ S,
                  n ∉ T →
                    (∀ m < n, m ∈ S ↔ m ∈ T) →
                      ∑' (k : ℕ), g (n + (1 : ℕ) + k) < g n →
                        ∑' (m : (↑T : Type)), g (↑m : ℕ) < ∑' (m : (↑S : Type)), g (↑m : ℕ) := by
  intro A B hA hB h
  intro g hg hg0 S T n hnS hnT hagree hgap
  have hsum : ∀ U : Set ℕ, Summable (fun m : U => g m) := fun U => hg.subtype U
  have hL : ({m | m < n} ∩ S : Set ℕ) = {m | m < n} ∩ T := by
    ext m
    simp only [Set.mem_inter_iff, Set.mem_setOf_eq]
    exact and_congr_right (hagree m)
  have hT_sub : T ⊆ ({m | m < n} ∩ T) ∪ {m | n < m} := by
    intro m hm
    rcases lt_trichotomy m n with hlt | rfl | hgt
    · exact Or.inl ⟨hlt, hm⟩
    · exact absurd hm hnT
    · exact Or.inr hgt
  have hS_sup : ({m | m < n} ∩ S) ∪ {n} ⊆ S := by
    intro m hm
    rcases hm with ⟨_, hm⟩ | hm
    · exact hm
    · rw [Set.mem_singleton_iff] at hm
      exact hm ▸ hnS
  have htail : ∑' m : {m | n < m}, g m = ∑' k : ℕ, g (n + 1 + k) := by
    let e : ℕ ≃ {m : ℕ | n < m} :=
      { toFun := fun k => ⟨n + 1 + k, by simp only [Set.mem_setOf_eq]; omega⟩
        invFun := fun m => m.1 - (n + 1)
        left_inv := fun k => by simp only; omega
        right_inv := fun m => by
          apply Subtype.ext
          have := m.2
          simp only [Set.mem_setOf_eq] at this
          simp only
          omega }
    rw [← Equiv.tsum_eq e]
    rfl
  have hmono : ∀ U V : Set ℕ, U ⊆ V → ∑' m : U, g m ≤ ∑' m : V, g m := by
    intro U V hUV
    exact Summable.tsum_le_tsum_of_inj (Set.inclusion hUV) (Set.inclusion_injective hUV)
      (fun c _ => hg0 c) (fun i => le_rfl) (hsum U) (hsum V)
  have hdisj1 : Disjoint ({m | m < n} ∩ T : Set ℕ) {m | n < m} := by
    rw [Set.disjoint_left]
    rintro m ⟨hlt, _⟩ hgt
    simp only [Set.mem_setOf_eq] at hlt hgt
    omega
  have hdisj2 : Disjoint ({m | m < n} ∩ S : Set ℕ) {n} := by
    rw [Set.disjoint_left]
    rintro m ⟨hlt, _⟩ hm
    rw [Set.mem_singleton_iff] at hm
    simp only [Set.mem_setOf_eq] at hlt
    omega
  calc ∑' m : T, g m ≤ ∑' m : ↥(({m | m < n} ∩ T) ∪ {m | n < m}), g m := hmono _ _ hT_sub
    _ = ∑' m : ↥({m | m < n} ∩ T), g m + ∑' m : {m | n < m}, g m :=
        Summable.tsum_union_disjoint hdisj1 (hsum _) (hsum _)
    _ = ∑' m : ↥({m | m < n} ∩ T), g m + ∑' k : ℕ, g (n + 1 + k) := by rw [htail]
    _ < ∑' m : ↥({m | m < n} ∩ T), g m + g n := by linarith
    _ = ∑' m : ↥({m | m < n} ∩ S), g m + ∑' m : ({n} : Set ℕ), g m := by
        rw [hL, tsum_singleton]
    _ = ∑' m : ↥(({m | m < n} ∩ S) ∪ {n}), g m :=
        (Summable.tsum_union_disjoint hdisj2 (hsum _) (hsum _)).symm
    _ ≤ ∑' m : S, g m := hmono _ _ hS_sup

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
import Nodes.«spec-5e2e0890--h2».Context

/-! 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 spec_5e2e0890__h2 : ∀ (A B : Set ℕ),
  (0 : ℕ) ∉ A →
    (0 : ℕ) ∉ B →
      ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) =
          ∑' (n : (↑B : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) →
        ∀ (g : ℕ → ℝ),
          Summable g →
            (∀ (m : ℕ), (0 : ℝ) ≤ g m) →
              ∀ (S T : Set ℕ),
                ∀ n ∈ S,
                  n ∉ T →
                    (∀ m < n, m ∈ S ↔ m ∈ T) →
                      ∑' (k : ℕ), g (n + (1 : ℕ) + k) < g n →
                        ∑' (m : (↑T : Type)), g (↑m : ℕ) < ∑' (m : (↑S : Type)), g (↑m : ℕ) := 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 fable-1020-e257-a, drafted with claude-fable-5-1, 2026-10-20; no one has read it against the Lean and signed it.

Draft · drafted, by the model named above

$\displaystyle g \ge 0 \text{ summable}, \sum_{k \ge 0} g(n+1+k) < g(n), n \in S \setminus T, S \cap [0,n) = T \cap [0,n) \implies \sum_{T} g < \sum_{S} g$

Split both sums at $n$: the parts below $n$ agree, the $S$ side has $g(n)$ in addition, and the rest of the $T$ side is a tail bounded by the gap.

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

Rendered from targets/erdos-257/nodes/spec-5e2e0890--h2/Statement.lean. Origin: compiler-derived.

Attestation: pass, 7 of 7 checks

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

Verdict pass, from attestations/000787.json.

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

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

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/erdos-257/nodes/spec-5e2e0890--h2/Witness.lean, sha256 ea39d4b030d5.
import Mathlib

theorem witness : ∃ (A : Set ℕ) (B : Set ℕ) (g : ℕ → ℝ) (S : Set ℕ) (T : Set ℕ) (n : ℕ),
  (0 : ℕ) ∉ A ∧
    (0 : ℕ) ∉ B ∧
      ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) =
          ∑' (n : (↑B : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) ∧
        Summable g ∧
          (∀ (m : ℕ), (0 : ℝ) ≤ g m) ∧ n ∈ S ∧ n ∉ T ∧ (∀ m < n, m ∈ S ↔ m ∈ T) ∧ ∑' (k : ℕ), g (n + (1 : ℕ) + k) < g n := by
  refine ⟨∅, ∅, fun m => if m = 0 then 1 else 0, {0}, ∅, 0, by simp, by simp, rfl, ?_, ?_, by simp, by simp, ?_, ?_⟩
  · exact summable_of_ne_finset_zero (s := {0}) (fun m hm => by simp_all)
  · intro m; dsimp only; split_ifs <;> norm_num
  · intro m hm; omega
  · 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 →