{"id":"083fa9a7-c09a-4817-b3dc-c336b5f9a36c","arxiv_id":"2412.03127","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Moessner's process for generating powers by addition is equivalent to a nested summation with index-dependent upper bounds, and this form generalizes to factorials, binomials, Catalan and polygonal numbers.","lead":"This paper recasts Moessner's process, an addition-only procedure that generates integer powers, as a plain nested summation after removing what it calls the dynamic-programming layer. The simplified form yields new nested-sum identities for Catalan, Fibonacci, Euler, and polygonal numbers, and gives a cleaner explanation of why the old theorem works.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 1 is asserted rather than proved; the fractional-index nested-sum identity is the load-bearing step and is only illustrated for n ≤ 5.","rationale":"The reader's weakest assumption points directly at the missing proof of Theorem 1, and the stress-test agrees. The theorem is the load-bearing assertion: it is what turns Moessner's process into an explicit nested-sum identity, and the paper's claimed simplification and its parameterized corollaries depend on it. The text provides only small-n unfoldings and an induction for the constant-bound variant, which is not the same theorem. The promised Coq file is mentioned but not made available, so independent verification is impossible from the preprint. The concern is not that the identity is likely false; small cases and the known Moessner theorem suggest it is true. The concern is that the central claim is presented as a theorem without a proof or a precise derivation from an already-proved theorem. This does not change the reader's CONDITIONAL verdict: acceptance should be contingent on supplying a complete proof or a machine-checked formalization of Theorem 1, or on explicitly deriving it from the classical Moessner theorem with all indexing details filled in.","tokens_in":33961,"tokens_out":9698,"duration_ms":90955,"concrete_test":"Inspect the accompanying .v file (or require it to be posted) and check that the Coq development contains a theorem of the form \"forall x n, <nested sum with upper bounds floor(k*i/(k-1))> = (x+1)^n\" with a completed proof, not merely examples of small n or the constant-bound case. A mismatch or a proof covering only n ≤ 5 would confirm that Theorem 1 is currently unproved in the preprint.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is Theorem 1 (Section 5): for all x,n, the nested sum whose kth upper bound is floor(k·i_{k-1}/(k-1)) equals (x+1)^n. Nothing in the text proves this. Section 3.4 unfolds the definition only for n = 0..5; Section 5 states the general theorem without proof; Section 7.4 contains the only general induction, and it is explicitly for the degenerate constant-filtering case (lambda (j _) x), not for the fractional-index g of Theorem 1. The Coq artifact promised in Appendix B is not supplied, and it is described as formalizing 'part of' the paper, so it cannot be checked. The paper also does not explicitly reduce Theorem 1 to the classical Moessner theorem: it would need a proof that iterating prefix sums with g j x = floor((j+1)x/j) yields exactly the function enumerated by the final stream of Moessner's process for arbitrary n. Without that, the theorem is an unverified assertion, and the paper's headline reformulation is unsupported. If Theorem 1 is meant as a restatement of known results, the reduction must be supplied; if it is meant as a new theorem, a proof is required.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a \"streamless\" reformulation of Moessner's theorem: instead of iterating Moessner's strike-out-and-prefix-sum process on streams, one evaluates a nested summation whose kth upper bound is floor((k+1) i_k / k). The central statement, Theorem 1 in Section 5, claims that this nested sum, and also the equivalent variant with upper bound i_k + floor(i_k/k), equals (x+1)^n for all natural x and n. The paper also gives a Scheme implementation (moessner and its parameterized variants), derives numerous corollaries (binomial coefficients, Catalan numbers, Fibonacci numbers, Euler numbers, factorial numbers, polygonal numbers, etc.), discusses dynamic-programming versions, and includes Appendix C with a new characterization of polygonal numbers. The exposition is lively and the small cases are worked carefully, but the central theorem is not proved in the text: only the cases n ≤ 5 are unrolled, and the only general induction supplied is for a degenerate constant filtering function that does not encode Moessner's strike-out phase.","tokens_in":34131,"tokens_out":3859,"duration_ms":42574,"significance":"If Theorem 1 were fully proved, the paper would provide a genuinely simpler statement of Moessner's theorem, reduce the process to nested summations with index-dependent bounds, and support a clean counting of the number of additions. The pedagogical value is high: the paper makes visible why the upper bounds depend on outer indices, and the corollaries are attractive. The author is also commendably explicit in Appendix C about what the polygonal-number characterization does and does not buy. However, at present the central identity is asserted rather than derived, and the Coq artifact mentioned in Appendix B is not supplied. The significance is therefore conditional on completing the proof and making the formalization available.","major_comments":[{"comment":"Theorem 1 is the load-bearing assertion of the paper, but no proof is given for arbitrary n. Section 3.4 unfolds the streamless process only for n = 0 through 5, and Section 5 states the general equality directly. The equality with (x+1)^n is exactly the content of Moessner's theorem, whose earlier proofs are cited but not re-derived. The author needs either a self-contained proof by induction (or a precise reduction to a cited theorem) that the nested sum with upper bounds floor((j+1)i_j/j) equals the final stream of Moessner's process for all n.","section":"Section 5, Theorem 1"},{"comment":"The only general induction in the paper proves Corollary 14, which treats the constant filtering function (lambda (j _) x), not the elision function g = lambda j x. floor((j+1)x/j) of Definition 1. The text explicitly calls this 'Moessner's theorem without dynamic programming, simpler' and shows that the constant case is a routine induction. This does not license Theorem 1, because the constant case has no index-dependent upper bounds and does not model the strike-out phase. The paper should state clearly that Corollary 14 is a separate, weaker statement.","section":"Section 7.4"},{"comment":"Appendix B says the accompanying .v file contains a Coq formalization of 'part of' the executive summary, Section 5, Section 6, and Section 9, but the artifact is not supplied with the preprint and the text never specifies whether it covers Theorem 1. Since Theorem 1 is the central claim, the absence of the formalization, and even of a precise statement of what was proved, leaves the main result without machine-checked support. If the formalization covers Theorem 1, it should be included or made accessible, and the corresponding statement should be identified.","section":"Appendix B"},{"comment":"The paper does not explicitly prove that iterating prefix sums with the elision function g exactly reproduces the stream process of Moessner for arbitrary n. The unrolling in Section 3.4 is suggestive, but a formal lemma connecting the two formulations is missing. Without such a lemma, Theorem 1 remains a reformulation with the same unproved status as the original theorem; the reader cannot tell whether the equality to powers is being assumed or derived.","section":"Sections 3.4 and 5"}],"minor_comments":[{"comment":"The executive summary uses floor notation, while the main text writes expressions such as 2·i1/1 and 3·i2/2 without an explicit floor. Since Definition 1 uses integer division, the paper should state once that all displayed divisions in nested sums are integer divisions, so that the notation is unambiguous.","section":"Throughout"},{"comment":"The claim that Bickford's Nuprl formalization is 'the first formalization of Moessner's theorem and of its proof' appears to contradict the immediately preceding description of Krebbers, Parlant, and Silva's Coq formalization from 2016. This should be rephrased or qualified.","section":"Section 2.2"},{"comment":"The Euler-number corollary uses upper bounds such as 1 − i_{n−2} and 0 − i_{n−1}, which can be negative for small n and for large inner indices. The paper should specify the convention for summation when the upper bound is less than the lower bound, or state the range of n for which the display is intended.","section":"Executive Summary / Section 5"},{"comment":"Appendix A promises an accompanying .scm file with an implementation and tests, but the file is not part of the visible submission. The paper should state how the reader can obtain the artifact, and should note that the artifact was not available to the reviewer.","section":"Appendix A"}],"recommendation":"major_revision","confidential_remarks":"The paper is charming and the reformulation is potentially valuable, but the central theorem is currently unsupported: the only complete general induction is for the trivial constant-filtering case, and the Coq file is not supplied. I would be positive after the author adds a real proof of Theorem 1 (or an explicit, verifiable reduction to Moessner's theorem) and either includes the formalization or clearly delimits what it proves."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Short version: the paper gives a streamless, nested-sum view of Moessner's theorem, some genuinely new corollaries, and an honest appendix about polygonal numbers. But the central theorem is not proved in the text; it is illustrated for n ≤ 5 and then stated. The only complete general induction covers a degenerate constant-bound case. So the load-bearing identity is inherited from the classical Moessner theorem without an explicit reduction. That is the main thing you need to know.\n\nWhat I like: the unrolling of the process in Section 3.4 makes the fractional-index upper bounds transparent, and the corollaries (binomial, Catalan, Fibonacci, Euler) are nice and check out on small cases. The polygonal-number characterization in Appendix C is genuinely new, and the author says plainly that it doesn't buy much—refreshing. The paper also credits the prior proofs (Perron, Paasche, Long, Kozen–Silva, etc.), and the dynamic-programming framing is a fair way to explain why the process looks magical.\n\nSoft spots. Theorem 1 is the whole article, and it is never proved. The examples for n = 0..5 are not a proof. Section 7.4 proves the trivial constant-filtering variant, which is a useful sanity check but not the theorem. The Coq file in Appendix B is only said to formalize 'part of' the paper, and neither it nor the Scheme file is available, so I cannot check the formal claims. Some corollaries (A125860, A137273) are just matched to OEIS entries; they are probably right but no proof is given. The paper also concedes in Section 7.4 that the striking-out and widening are unnecessary for computing powers, which undercuts the 'essence' framing—but that is an honest concession, not a fatal flaw.\n\nThe right path is straightforward: the author needs to supply a genuine proof of Theorem 1, either by reducing it to Moessner's theorem (show that iterating prefix sums with g j x = floor((j+1)x/j) enumerates exactly the stream produced by the process) or by an independent induction. That reduction is not in the text, and until it is, the reformulation is a conjecture supported by examples.\n\nWho this is for: people working on Moessner's theorem, stream calculi, or nested-sum identities. They will enjoy the clean exposition and the new corollaries. I would send it to a referee with a request to check Theorem 1 and the OEIS corollaries. It deserves peer review, but only with a real proof of the main theorem.\n\nRecommendation: engage with it, but ask for the missing proof and artifacts before accepting.","headline":"A clean reformulation of Moessner's theorem as nested sums, with several new-looking identities, but the central Theorem 1 is asserted rather than proved in the text.","tokens_in":34688,"tokens_out":2129,"would_cite":false,"duration_ms":19211,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["05A10","11B65","11B83"],"pacs":[],"model":"deepseek-v4-flash","headline":"Moessner's theorem reduces to a single nested-sum identity whose index-dependent upper bounds equal $(x+1)^n$, with tuned bounds yielding binomial, Catalan, and factorial numbers.","keywords":["Moessner's theorem","Moessner's process","nested summations","dynamic programming","integral powers","factorial numbers","Catalan numbers","polygonal numbers"],"falsifier":"Directly compute the left-hand nested sum with upper bounds $\\lfloor 2i_1/1 \\rfloor, \\lfloor 3i_2/2 \\rfloor, \\dots, \\lfloor n i_{n-1}/(n-1) \\rfloor$ for $n=6$ and $x=3$: if the value is not $4^6 = 4096$, the identity is false, and the finite computation settles it.","tokens_in":33706,"feed_emoji":"🔢","tokens_out":6736,"duration_ms":60660,"temperature":0.7,"pith_summary":"The paper claims that Moessner's process—the seventy-year-old additive routine that turns the constant stream of ones into the stream of $n$-th powers by repeatedly striking out elements and taking prefix sums—is dynamic programming wrapped around a simpler core of nested summations. The central identity is that for all natural $x$ and $n$, $\\sum_{i_1=0}^{x} \\sum_{i_2=0}^{\\lfloor 2 i_1/1 \\rfloor} \\cdots \\sum_{i_n=0}^{\\lfloor n i_{n-1}/(n-1) \\rfloor} 1 = (x+1)^n$, with the equivalent upper-bound form $i_k + \\lfloor i_k/k \\rfloor$. If this is right, the \"how\" and \"why\" of Moessner's theorem are answered without streams or memoization: the power comes from index-dependent upper bounds, and dynamic programming is only an implementation strategy. The same tuning produces new additive characterizations of factorials, binomial coefficients, Catalan numbers, Fibonacci and Euler numbers, and polygonal numbers.","feed_headline":"Moessner's powers reduce to nested sums","feed_subtitle":"Stripped of dynamic programming, the 70-year-old additive process becomes nested sums that also yield factorials and Catalan numbers.","key_machinery":"The load-bearing object is the elision function $g\\,j\\,x = \\lfloor (j+1)x/j \\rfloor$ (also written $x + \\lfloor x/j \\rfloor$), which encodes the periodical strike-out phase as an index transformation. It supplies the upper bound of each inner sum in the nested-sum identity; iterating it $n$ times produces the \"fractionally increasing upper bounds\" of Theorem 1. The paper's central identity is that the $n$-fold nested sum with these bounds equals $(x+1)^n$, and the same function, parameterized differently, yields its corollaries.","core_discovery":"On the paper's own terms, the discovery is that Moessner's process is a dynamic program, and that removing its memoization infrastructure exposes a streamless statement of Moessner's theorem: an $n$-fold nested prefix sum whose $k$-th inner upper bound is the elision function $g$ applied to the previous index equals $(x+1)^n$. The elision function $g\\,j\\,x = \\lfloor (j+1)x/j \\rfloor$ (equivalently $x + \\lfloor x/j \\rfloor$) reproduces the strike-out phase as an index transformation, so each nested sum is a pure instance of repeated addition. The paper further claims that \"Moessner's magic\"—the dependence of inner upper bounds on outer indices—is exactly what accounts for the transitory rational arithmetic when Catalan numbers are computed this way, and that varying $g$ generates factorials, binomial coefficients, Catalan numbers, Fibonacci and Euler numbers, and a new characterization of polygonal numbers as bounded sums of increasing quotients.","pith_inferences":["Not in the paper: if the central identity holds for all $n$, the same index-dependent upper-bound schema could be tuned against other known sequences to discover new nested-sum characterizations, since Section 7 already finds several by varying $g$.","Not in the paper: the paper's distinction between primitive iteration and primitive recursion suggests a broader claim that any dynamic program with overlapping subcomputations forming a simple lattice can be exactly reverse-engineered into a nested sum.","A testable extension is to replace the fractional upper bound $\\lfloor (j+1)x/j \\rfloor$ by other rational functions of $x$ and $j$ and search for closed forms, as the polygonal-number corollary shows the pattern is fertile."],"forward_implications":["Computing $(x+1)^n$ requires no multiplication: it is $n$ nested summations, each of which is just repeated addition.","Moessner's stream-based process is one particular memoized implementation of a simple recursive summation function; removing the memoization does not change the result.","Tuning the upper bounds yields additive definitions of binomial coefficients, Catalan numbers, factorial numbers, Fibonacci and Euler numbers, and polygonal numbers.","The same machinery re-expresses any finite product $\\prod_{i=0}^{n} f(i)$ as a nested sum, so the slide-rule correspondence becomes a direct identity.","Reintroducing memoization gives a dynamic program computing powers with $x \\cdot n(n+1)/2$ additions instead of $(x+1)^n$ additions."],"supporting_citations":[{"why":"Supplies the original statement of Moessner's process and theorem, the fact being recast without dynamic programming.","marker":"[35]"},{"why":"Provides Perron's induction proof of Moessner's theorem, one source of the equality the paper restates.","marker":"[50]"},{"why":"Gives Paasche's generating-function proof and the observation that the process can start with a stream of ones.","marker":"[46]"},{"why":"Supplies Long's theorems on arithmetic-progression initial streams, which Sections 7.2 and 7.3 recast as instantiations.","marker":"[29]"},{"why":"Offers a calculational proof of Moessner's theorem, a baseline the streamless formulation is meant to simplify.","marker":"[22]"},{"why":"Provides the concrete stream calculus framework and is the cited source for Catalan numbers in the Moessner literature.","marker":"[23]"},{"why":"Gives an algebraic generalization of Moessner's theorem, against which the present nested-sum reading can be compared.","marker":"[26]"},{"why":"Supplies the nested for-loop computation of Catalan numbers that the paper's Corollary 21 rediscovers.","marker":"[21]"},{"why":"Proves Irwin's nested-sum conjecture for sequence A002449 using generating trees, the closest related work for nested-sum characterizations.","marker":"[28]"}],"fun_headline_variants":["Moessner's magic explained by nested sums","Stripping dynamic programming from Moessner's process","Moessner's theorem without DP: nested sums do it","Nested sums unlock Moessner's process and more"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The article assumes that the elision function $g\\,j\\,x = \\lfloor (j+1)x/j \\rfloor$ exactly encodes the strike-out phase and that the nested-sum equality to $(x+1)^n$ holds for every $n$, but the general proof of that equality is not carried out in the text, which illustrates $n=0$ through $5$ and otherwise relies on the original theorem and the accompanying formalization file.","fun_headline_variants_meta":{"raw":{"variants":["Moessner's magic explained by nested sums","Stripping dynamic programming from Moessner's process","Moessner's theorem without DP: nested sums do it","Nested sums unlock Moessner's process and more"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000173,"raw_usage":{"total_tokens":1290,"prompt_tokens":971,"completion_tokens":319,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":587,"completion_tokens_details":{"reasoning_tokens":253}},"tokens_in":587,"tokens_out":319,"duration_ms":3309,"temperature":1.0,"reasoning_tokens":253,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-11T22:44:48.594813+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Directly compute the left-hand nested sum with upper bounds $\\lfloor 2i_1/1 \\rfloor, \\lfloor 3i_2/2 \\rfloor, \\dots, \\lfloor n i_{n-1}/(n-1) \\rfloor$ for $n=6$ and $x=3$: if the value is not $4^6 = 4096$, the identity is false, and the finite computation settles it.","supporting_citations":[{"cited_title":"Aus den Sitzungs- berichten der Bayerischen Akademie der Wissenschaften, Mathematischnaturwissenschaftliche Klasse 29(3), p","cited_arxiv_id":null,"evidence_quote":"Supplies the original statement of Moessner's process and theorem, the fact being recast without dynamic programming."},{"cited_title":"Aus den Sitzungsberichten der Bayerischen Akademie der Wissenschaften, Mathematischnaturwissenschaftliche Klasse 29(4), pp","cited_arxiv_id":null,"evidence_quote":"Provides Perron's induction proof of Moessner's theorem, one source of the equality the paper restates."},{"cited_title":"Aus den Sitzungsberichten der Bay- erischen Akademie der Wissenschaften, Mathematischnaturwissenschaftliche Klasse 30(1), pp","cited_arxiv_id":null,"evidence_quote":"Gives Paasche's generating-function proof and the observation that the process can start with a stream of ones."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Offers a calculational proof of Moessner's theorem, a baseline the streamless formulation is meant to simplify."},{"cited_title":"Journal of Functional Programming 20(5-6), pp","cited_arxiv_id":null,"evidence_quote":"Provides the concrete stream calculus framework and is the cited source for Catalan numbers in the Moessner literature."},{"cited_title":"The American Mathematical Monthly 120(2), pp","cited_arxiv_id":null,"evidence_quote":"Gives an algebraic generalization of Moessner's theorem, against which the present nested-sum reading can be compared."},{"cited_title":"Grimaldi (2012): Fibonacci and Catalan Numbers – An Introduction","cited_arxiv_id":null,"evidence_quote":"Supplies the nested for-loop computation of Catalan numbers that the paper's Corollary 21 rediscovers."},{"cited_title":"In: The On-Line Encyclopedia of Integer Sequences","cited_arxiv_id":null,"evidence_quote":"Proves Irwin's nested-sum conjecture for sequence A002449 using generating trees, the closest related work for nested-sum characterizations."}],"review_version":1}