Convergents and limits of a boundary family of polynomial continued fractions, and a census application

The paper studies the continued fractions b(0) + Kn>=1 a(n)/b(n) with a(n) = -n^2 + (1-m)n + a0 and b(n) = s(2n+m), s = +1 or -1 ("family H"). This is the boundary case d1^2 + 4*c1 = 0 of polynomial continued fractions with linear denominators, which Nörlund's hypergeometric formula, as quoted in a recent paper, does not cover. The convergents have an explicit closed form in Pochhammer symbols. From it the paper reads off termination, the value of terminating fractions, convergence to the larger root of x^2 - (m-1)x - a0 when D = (m-1)^2 + 4*a0 > 0, logarithmic convergence when D = 0, and divergence when D < 0. The main contribution is an application to a frozen census of 144 such fractions: every one is classified, the 40 stored limits that are quadratic irrationals are checked, 26 slow families are examined, and an earlier closed-form hypothesis is shown to be wrong on 4 terminating rows. The paper also gives a short proof of the known value 6/(3*pi - 8) for 4 + K n^2/4, and a Lean 4 formalization of part of the theorem. Novelty: we make no novelty claim for the convergent formula or for the value 6/(3*pi - 8), and no claim that the Lean formalization is the first. The convergent formula was not found in the sources we consulted (listed in the paper); it is possibly known in the classical literature (Perron, Wall, Lorentzen-Waadeland, Cuyt et al. were not consulted). Status of the claims (fixed; not to be read more strongly):- T0, T0', T1, T2 (as stated in Lean): PROVEN in Lean 4 (v4.30.0, Mathlib c5ea00351c28e24afc9f0f84379aa41082b1188f, no sorry, standard axioms only). This certifies the Lean statements; their fidelity to the prose was checked by two AI models, not by a human. It is not human-refereed.- T2' (convergence rate), T3 (D = 0), T4 (D < 0): proved on paper, checked by agents and two independent AI readers, not machine-checked. T2' is conditional on a Stirling-type statement that is not source-checked.- 6/(3*pi - 8): proved on paper, one AI reading with no error found, five analytic steps not independently checked. The value is known.- Census application: computed by scripts from frozen files. The scripts in the zip are new re-implementations, not the research project's registered instruments; agreement with the original census is a consistency check, not independent verification. The project's rule asks for a second numerical method for a headline numerical claim; only one was available for family H, so the numerical gate was not passed.- No human mathematician has read any proof in this paper. AI use: the paper, its proofs, the scripts and the Lean files were produced by AI models (Claude Sonnet 5.5 through GitHub Copilot CLI as author and preparer of this deposit; claude-haiku-5.5 and Claude Sonnet 5 as second readers), under the direction of a human operator who set the research questions and the rules of the project, authorised changes, and decides what is deposited. The operator was assisted by a further AI model (Claude Opus 5.5) that reviewed the results, helped set the project's rulings and checked the Lean statements against the prose. The operator has not refereed the mathematics. Readers should treat every non-Lean result as unrefereed. Files: boundary-family-pcf-census.pdf (the paper, 14 pages, CC BY 4.0) and artifact.zip (Lean 4 project without the .lake build folder, four Python check scripts, four frozen CSV files, recorded outputs, MANIFEST.sha256 of every file; MIT licence). To rebuild the Lean project: install elan, run "lake exe cache get" then "lake build" in artifact/lean (toolchain pinned in lean-toolchain). The Lean build record in the zip was transcribed from the research log; the build was not re-run while preparing this deposit. Python checks: "python -B run_all.py" in artifact/python. Contact: ppapanokechi@gmail.com. Author listed under the pseudonym Papanokechi.