The "if" direction of Conjecture 1.4 of arXiv:2111.04468: factorial reduction for the Eq. 6 and Eq. 7 families

Status: PROVED modulo pinned statements (listed in §3, each quoted with theorem/page number from the primary source). Reviewed by independent AI agents only; not yet reviewed by a human expert. Comments welcome. Conjecture 1.4 of Ben David, Nimri, Mendlovic, Manor, De la Cruz Mengual and Kaminer, On the connection between irrationality measures and polynomial continued fractions (arXiv:2111.04468, version 2 of 22 March 2024; Arnold Math. J. 10 (2024)), states that for bn = B(n − x1)(n − x2) with rational B, x1, x2, the polynomial continued fraction with partial numerators bn and partial denominators an has factorial reduction if and only if an belongs to one of two explicit linear families, (Eq. 6) and (Eq. 7). This note proves the “if” direction only: under the standing assumption bn ≠ 0 of that paper, and in the integer form obtained by inflation that the paper describes, every member of the families (Eq. 6) and (Eq. 7) has factorial reduction. The paper's index convention (p−1 = 1, p0 = a0, q−1 = 0, q0 = 1) is kept, and the conjecture is quoted verbatim from version 2. The “only if” direction is not addressed. Method: the exponential generating function of the convergent numerators and denominators is identified with a solution of a Gauss hypergeometric equation at an algebraic ordinary point, and its Taylor coefficients are shown to satisfy Galochkin's condition (G). The proof relies on statements from Y. André, Séries Gevrey de type arithmétique, I, Ann. of Math. 151 (2000), 705–740, namely condition (G) (§1.1, p. 708), Proposition 1.1.1 (p. 709) and its proof (p. 710), Lemme 1.1.2 (p. 710), condition (H) and G-functions (§2.1–2.2, pp. 712–713), the definition of G-operators with the remark that their solutions at ordinary points are G-functions (§3.1, pp. 717–718), Chudnovsky's theorem (Théorème 3.2, p. 718), and the remark on p. 719 following Théorème 3.4 (used only for Theorem A). Each is quoted verbatim in §3 of the note with its location. A separate Theorem A, which the main result does not use, shows that the denominator bound forces the roots of b to be rational. Prior art: a search of later papers by the same group and of papers citing arXiv:2111.04468 (Semantic Scholar, OpenCitations and Crossref, plus arXiv author and keyword queries, run on 5 October 2026; OpenAlex was unavailable; the full texts of 15 candidate papers were searched and the hits read by hand) found no earlier proof of either direction. This is a search result, not a guarantee. Files: the note (PDF and LaTeX source), and an archive with the note, the scripts and their logs, and a SHA-256 manifest. The archive includes a symbolic check of every identity used in the proofs (112 checks), the scripts and logs behind the illustrative numbers of Remark A.1 (not part of any proof), the prior-art search log with its manual review, and a provenance audit tying every number in the note to a log line. Each log begins with the hash of the script that wrote it. AI use: the arguments, scripts and note were developed with AI coding agents (GitHub Copilot CLI; main model claude-opus-5.5; sub-agent reviewers during development claude-sonnet-5 and gpt-5.5). Before deposit, two further AI reviewer agents, run separately from the agent that wrote the note, read it: a mathematical review (self-reported model gpt-5.4) and a review of quotations, references and wording against the primary sources (self-reported as an OpenAI GPT model; exact identifier not reported). Their findings were corrected in this version. No human expert has reviewed the note. The author is responsible for the content. Licences: text and data CC BY 4.0; code (scripts/) MIT.