Problems / erdos-412 / erdos-412--h1
Descent step for sigma orbits (gate-written form)
erdos-412--h1
superseded
Left open by a proof skeleton.
Superseded by erdos-412--h1-v2. Work continues on the replacement; this statement is kept for its history (D-8). The curator's record: superseded by erdos-412--h1-v2 on revision request targets/erdos-412/nodes/erdos-412--h1/revisions/20260917T171641Z-calib-lead-83dd.yaml (other-with-exhibit; D-8)
$\displaystyle \forall m\ge 3:\quad \bigl(\neg\,\exists x,\ 2\le x<m\ \wedge\ \exists k,\ \sigma^{[k]}(x)=m\bigr)\ \Rightarrow\ \exists m',\ 2\le m'<m\ \wedge\ \exists i,j,\ \sigma^{[i]}(m)=\sigma^{[j]}(m')$
For every natural number $m\ge 3$: if no $x$ with $2\le x<m$ reaches $m$ under some iterate of $\sigma$, then there is an $m'$ with $2\le m'<m$ whose forward $\sigma$-orbit meets that of $m$, that is, $\sigma^{[i]}(m)=\sigma^{[j]}(m')$ for some $i,j\ge 0$. Here $\sigma=\sigma_1$ is Mathlib's sum-of-divisors function on $\mathbb{N}$ (ArithmeticFunction.sigma 1, applied through its coercion ⇑(σ 1)) and $\sigma^{[k]}$ its $k$-fold iterate; as written the file imports Mathlib without opening the σ notation's namespace, so the text names σ without that notation in scope.
Lean
theorem erdos_412__h1 : ∀ (m : ℕ),
3 ≤ m →
(¬∃ x, 2 ≤ x ∧ x < m ∧ ∃ k, (⇑(σ 1))^[k] x = m) → ∃ m', 2 ≤ m' ∧ m' < m ∧ ∃ i j, (⇑(σ 1))^[i] m = (⇑(σ 1))^[j] m' := by
sorryWhy 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 is being proved
Superseded.
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
/-! Hole `descent` 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_412__h1 : ∀ (m : ℕ),
3 ≤ m →
(¬∃ x, 2 ≤ x ∧ x < m ∧ ∃ k, (⇑(σ 1))^[k] x = m) → ∃ m', 2 ≤ m' ∧ m' < m ∧ ∃ i j, (⇑(σ 1))^[i] m = (⇑(σ 1))^[j] m' := by
sorryA 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 m\ge 3:\quad \bigl(\neg\,\exists x,\ 2\le x<m\ \wedge\ \exists k,\ \sigma^{[k]}(x)=m\bigr)\ \Rightarrow\ \exists m',\ 2\le m'<m\ \wedge\ \exists i,j,\ \sigma^{[i]}(m)=\sigma^{[j]}(m')$
For every natural number $m\ge 3$: if no $x$ with $2\le x<m$ reaches $m$ under some iterate of $\sigma$, then there is an $m'$ with $2\le m'<m$ whose forward $\sigma$-orbit meets that of $m$, that is, $\sigma^{[i]}(m)=\sigma^{[j]}(m')$ for some $i,j\ge 0$. Here $\sigma=\sigma_1$ is Mathlib's sum-of-divisors function on $\mathbb{N}$ (ArithmeticFunction.sigma 1, applied through its coercion ⇑(σ 1)) and $\sigma^{[k]}$ its $k$-fold iterate; as written the file imports Mathlib without opening the σ notation's namespace, so the text names σ without that notation in scope.
Rendered from gloss/20bf1386c7d5….md · Improve these words →
Rendered from targets/erdos-412/nodes/erdos-412--h1/Statement.lean. Origin: skeleton-hole.
Witness — its slot is open
Not checked — the witness slot is open.
83b3f76974bd./-! The witness slot for a hole (D-29, F07-R6). Replace `sorry` with an instance satisfying this statement's hypotheses; until then the node is blocked. -/ theorem witness : True := by sorry
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
No explainer yet. An explainer is a merged proof written as a journal would print it, so there is nothing to explain until this statement is proved (D-3).