slug: poncini-rasmussen-2022-transfer-expansion-conjecture-c12
bibkey: poncini2023planar
doi: 10.1088/1742-5468/acdce7
triage: theorem
motivation_gids:
  - D5/S3/StatisticalMechanics/VertexModels/PonciniRasmussenTransferExpansion.result
url: https://arxiv.org/abs/2206.14462v2

The Poncini–Rasmussen central factorial transfer expansion

Problem

Poncini and Rasmussen, Integrability of planar-algebraic models, arXiv:2206.14462v2, Appendix C, page 47, state Conjecture C.12:

For every n ∈ ℕ and all u ∈ F, we have Ť_n(u) = 2 Σ_{k=0}^{n−1} (1 + u²)^{n−k} (2u)^k Σ_{j=0}^{⌊k/2⌋} [n − k − 2 + 2j over 2j]!! (−1)^j m_{k−2j}(h_n)/(k − 2j)!

The domain is $n\ge 1$ and an algebraically closed field $F$ of characteristic zero. The source’s coefficients and ordered operators are (C.9)–(C.15), the Hamiltonian is (C.40), the central factorial polynomials are (C.44), and the double factorial quotient is (C.65). The source note is D5/L/StatisticalMechanics/poncini2023planar. Preregistration: #19637.

Statement echo

The settling namespace is D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion; the scalar namespace is D5.S1.Recurrence.CentralFactorialTransferExpansion.

Motivation

The source establishes membership in the algebra generated by the Hamiltonian and an inverse-Vandermonde interpolation formula. This result supplies the explicit central factorial coefficient formula conjectured in (C.66). It is a settlement of that named assertion; prior-art completeness is not established.

Gap

The central step is the scalar coefficient identity for every $m,l,k\in \mathbb{N}$ with $l,k\le m$, evaluated at the Hamiltonian eigenvalue $m-2l$. The identity must be combined with the transfer matrix built from the literal ordered double row and auxiliary trace, rather than an assumed product formula.

The four-slot escape audit is unfinished under #19685. Its targets are central_spectral_coeff, scalar_settlement, the settling result, and the published owner GVHunter.reverse_word_list. No compiled registration is delivered.

Route

The scalar module proves central_spectral_coeff by central differences, formal binomial series and recurrence identities, and obtains scalar_settlement by polynomial coefficient comparison and homogenization. Its field assumptions are Field and CharZero.

The settling proof reduces the literal double row to commuting adjacent flips. A Walsh matrix simultaneously diagonalizes the flips; its square is a nonzero scalar multiple of the identity. The scalar identity applied at the number of sign changes then proves the full matrix equality. GVHunter.reverse_word_list from D5/S3/Analytic/Hunter/NCHunterPositivity supplies the reversed word; internalFailures from D5/S3/Estimation/DataProcessing/OneCutZeroExcess supplies the sign-change set.

Falsifier

An entrywise discrepancy between the literal transfer matrix and (C.66), a different operator ordering, an incorrectly scoped coefficient, or a nonstandard axiom in the compiled proof would invalidate the claimed formal settlement. Finite computations test the stated ranges only. The public definition of the claim retains all source hypotheses and the full right-hand side.

Evidence

The kernel-checked settling declaration is D5/S3/StatisticalMechanics/VertexModels/PonciniRasmussenTransferExpansion.result; its scalar prerequisites are D5/S1/Recurrence/CentralFactorialTransferExpansion.central_spectral_coeff and .scalar_settlement. The axiom closure of every public declaration is contained in {propext, Classical.choice, Quot.sound}.

Experiment: pinned program and results. Command: /opt/homebrew/bin/python3 /Users/auric/trureturing-experiments/docs/reports/poncini-rasmussen-2022-transfer-matrix-conjecture-c-12/check.py; exit 0; script SHA-256 ef3b4492cedfc2ed5294353d043c93793e2795f83947a3fc1b232b147cfb56c5. The scalar comparison passes for $n=1,\dots ,40$ and the literal matrix comparison passes for $n=1,\dots ,4$. These are computed finite cross-checks, separate from the universal Lean proof.

Triage

What the settlement shows

Proved in Lean: central_spectral_coeff identifies the coefficient of $t^k$ in $(1+t{)}^{m-l}(1-t{)}^l$ with the double factorial sum at $x=m-2l$. scalar_settlement gives the scalar eigenvalue identity at every allowed index and spectral parameter. result lifts this to the literal transfer matrix for every length in the claim.

Explanation: the central difference recurrence and formal binomial substitution produce the double factorial quotient. Multiplying the finite coefficient identity by the homogeneous weights produces a polynomial identity, so the proof imposes no condition $1+u^2\ne 0$. The Walsh square identity allows matrix cancellation in characteristic zero. These identities describe the decisive mechanism; they are not numerical extrapolations.

Computed: the finite experiment checks exactly the scalar and matrix ranges stated in Evidence. Open: extensions to positive characteristic, other boundary coefficients or different vertex weights, and any claim of prior-art completeness. No sharp quantitative estimate is asserted by this equality.

Proved in prose: the explicit equality supplies the polynomial-algebra membership (C.45) directly. It gives explicit coefficients for the same transfer matrix addressed by the source’s interpolation formula. No additional dependent source result is claimed formally here.

Declaration judgement

The supporting scalar module has admission basis escape-witness. The modified existing owner retains admission basis escape-witness. The settling module has admission basis open-problem-resolution (#19637; Proved). All three carry utility: none.

ASSUMED-UNVERIFIED

Prior-art completeness remains ASSUMED-UNVERIFIED. The preregistration records that v1 and v2 retain the conjecture, that arXiv:2302.11712 and arXiv:2509.11756 were screened without a settlement, and that Poncini’s thesis and the complete citation coverage were not verified. Literature reports are attributed to the preregistration’s producers. Four-slot registration remains unfinished under #19685; kernel verification does not establish registration completion or source fidelity by itself.