A Fredholm-determinant representation of the pcf-delta growth constant: finite identity, entire order and genus

Let b(k)=A k^2 + B k + C be a positive quadratic and u_n = 1/(b(n-1) b(n)) for n>=2. The pcf-delta growth constant of the running family (A,B,C)=(1,0,1) is delta = log R_inf(1), where R_inf(lambda) is the weighted independence (sparse-subset) polynomial of the half-infinite path carrying vertex weight lambda u_i. This note gives a self-contained account of the Fredholm-determinant representation delta = (1/2) log det(I + T^2), where T is the edge-weighted path operator with off-diagonal sqrt(u_{j+1}). Two contributions are machine-checked in Lean 4 / Mathlib with a clean axiom cone (subset of {propext, Classical.choice, Quot.sound}, no sorryAx): the finite tridiagonal determinant identity det A_M = c_M (Theorem 1) and its combinatorial reading c_M = R_M (Theorem 2). The Fredholm representation itself is confirmed numerically to 65 significant digits by two independent channels and is stated as a conjecture, with the operator limit carried as an analytic hypothesis. We determine the entire order and genus of R_inf: it is entire of order rho = 1/(2d) (with d=2, so rho = 1/4) and genus 0, with Hadamard product R_inf(lambda)^2 = prod_k (1 + lambda s_k^2) and no exponential factor (Proposition 7). The order is bracketed by elementary by-hand bounds and confirmed by two independent numerical routes (coefficient decay and eigenvalue convergence exponent). We also give a clean telescoping bound S = sum_{n>=2} u_n =1, B>=0 this gives S = 80) with SHA-256 output hashes; the Lean project ships with a pinned toolchain (lean4 v4.30.0, Mathlib v4.30.0) and a verbatim #print axioms audit. Four-class status discipline (PROVEN / STRUCTURAL / VERIFIED / CONJECTURED) is applied throughout: PROVEN is reserved for the two Lean-formalized theorems only.