pcf-delta: The growth-law correction constant δ = log R∞ of the quadratic polynomial continued fraction — structure, a closed-form bracket, and certified high-precision values
Papanokechi · Zenodo (CERN European Organization for Nuclear Research) · 2026
A characterization of the additive correction constant δ = log R∞ > 0 that the companion growth-law note introduces and leaves undetermined for the quadratic polynomial continued fraction V(A,B,C) = 1 + Kn≥1 1/(An2+Bn+C), integers A,C ≥ 1, B ≥ 0. With bk = Ak2+Bk+C, the standard continuant q0=1, q1=b1, qn=bnqn-1+qn-2, scaled partial quotients un = 1/(bn-1bn) and S = ∑n≥2 un, the scaled limit is R∞ = lim qn/∏k≤n bk and δ = log R∞. Contributions. (i) R∞ is exactly the independence polynomial of the path graph on the indices, giving the elementary two-sided bracket log(1+S) ≤ δ ≤ −log(1−S). (ii) Exact closed forms for the cluster sums σ2, σ3 in terms of power sums of un, machine-verified against brute-force enumeration of non-consecutive subsets to residuals ~10-54. (iii) Certified high-precision values of δ for nine triples (≥39 correct digits each, ≥44 for (1,0,1): δ(1,0,1) = 0.12385719436062639272850498970259084096757955…) via an exact downward recurrence seeded by an order-3 cluster expansion at large M, with an independent forward + Neville cross-check (~25 digits) and an exact confluent-polygamma seed for degenerate (repeated-pole) triples such as (1,2,1) where S = π2/3 − 13/4. (iv) A rigorous null: no low-height integer relation is found for V, R∞, or δ (mpmath identify at 100 digits; PSLQ over {1, π, log 2, γ, Catalan, ζ(3)}), and a precision-stability test shows the high-height PSLQ vectors are working-precision artifacts, not genuine relations. (v) A machine-checked finitary core in Lean 4 / Mathlib (toolchain pinned lean4 v4.30.0, Mathlib v4.30.0): the Casoratian (discrete-Wronskian) identity, the existence of R∞ = lim Rn by monotone-bounded convergence, the independence-polynomial identity (Rn equals the weighted independence polynomial of the path graph on the indices), and the finite-window cluster core σ2 = e2 − a1, with clean axiom cones (61 declarations checked by #print axioms as of v1.4; 58 in v1.3; 26 in v1.2). New in v1.3. A general Casoratian identity over any commutative ring (the classical (−1)n Wronskian recovered as a special case); a degree-graded refinement of the independence polynomial together with the order-3 cluster window object (the closed form for σ3 remains structural, not promoted); an m-term geometric-tail enclosure refining the δ bracket; and an exact weighted partial-fraction telescoping identity for the B=0 family. New in v1.4. The order-3 cluster closed form σ3 = e3 − a1p1 + c + t is promoted to PROVEN in Lean (sigma3win_eq, via the inclusion–exclusion bad-triple decomposition partition_l), together with a strict-monotonicity cone rseq_strictMono_succ for the scaled recurrence; Check.lean now reports 61 clean axiom cones. v1.4 supersedes v1.3 as the current release. Epistemic status (SIARC four-class). PROVEN — the Lean core (Casoratian identity; existence of R∞; the independence-polynomial identity; the finite-window cluster core σ2 = e2 − a1; and, new in v1.4, the order-3 cluster closed form σ3 = e3 − a1p1 + c + t), each declaration verified by #print axioms to a subset of {propext, Classical.choice, Quot.sound} with no sorryAx and no sorry/admit in source. STRUCTURAL — the scaled recurrence and tail estimate, the bracket and the closed form for S (complete elementary hand proofs, not yet formalized). VERIFIED — the cluster identities and all tabulated δ values numerically (mpmath), with the bracket satisfied on every tabulated triple. CONJECTURED — δ has no low-height elementary closed form and is a new transcendental constant of the family; irrationality of δ is open. A null integer-relation result is a complete and honest answer, not a gap.