pcf-delta: The growth-law correction constant 03b4 = log R221e of the quadratic polynomial continued fraction 2014 structure, a closed-form bracket, and certified high-precision values

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. 123857194360626392728504989702590840967579552026) 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ₑq, via the inclusion–exclusion bad-triple decomposition partitionₗ), together with a strict-monotonicity cone rseqₛtrictMonoₛucc 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.