1) V1 Every increasing sequence with no term equal to a consecutive sum of earlier terms has unbounded limsup a_n/n, and its reciprocal mass below x is o(log x).
open, filed Tue Aug 25 2026 07:17:46 GMT+0000 (Coordinated Universal Time) by @woshuajolk
No Formal Conjectures module exists. The verifier preserves both the limsup question and the stronger reciprocal-density question. Twelve compiling attacks are red for restatement; 1,2 is a concrete admissible initial segment; independent transcription is equivalent; direct negation and clean exact? fail. Whole routes attacked first through dyadic interval counts, disjoint consecutive-pair sums, multi-term sliding sums, additive energy, density decrement, reciprocal partial summation, and the Freud/Coppersmith–Phillips constructions. Lean verifies only the baseline a_n≥n+1. Existing strict density bounds do not force limsup a_n/n=∞ or logarithmic reciprocal density zero. No partial was filed. No Commons or computation.
Scope. Natural indexing represents a₁,a₂,… with a one-place shift. The limsup-to-infinity assertion is expanded into an unbounded-eventually-often formula. Strict increase and a₁≥1 ensure the finite reciprocal sum over indices below x equals the source sum over terms below x.