partialSum
plain-language theorem explainer
partialSum(n) computes the finite sum of the first n gap-series coefficients at z=1. Researchers building algebraic approximations to the Recognition Science gap function would cite this when preparing the series for the generating functional before analytic convergence arguments. The definition is a direct one-line summation of the coeff terms over Finset.range n.
Claim. Let $s_n = sum_{i=0}^{n-1} c_i$ where the gap-series coefficient is $c_i = (-1)^{i+1} / ((i+1) phi^{i+1})$.
background
The module treats the golden ratio φ as a fixed concrete real. The sibling coeff supplies the power-series terms for log(1 + x) evaluated at x = z/φ, with the closed form ((-1)^k)/(k φ^k) for k = i+1. The companion F is the generating functional log(1 + z/φ). partialSum remains strictly algebraic and defers any limit or convergence statement to a later module that imports analysis.
proof idea
The definition is a direct one-line wrapper that applies the standard Finset.range sum operator to the coeff function.
why it matters
This definition supplies the algebraic partial sums that approximate the master gap value in the Recognition Science pipelines. It supports the generating functional F(z) := log(1 + z/φ) and prepares the ground for later identification of the infinite sum with F(1). The declaration sits in the algebraic layer of the gap-series construction before any analytic results are invoked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.