The Poncini–Rasmussen central factorial transfer expansion

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\ge1$ 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.

| Source clause | Lean counterpart | Fidelity | | --- | --- | --- | | Algebraically closed characteristic-zero field $F$ | claim quantifies over F, Field F, IsAlgClosed F, CharZero F | Full source domain. | | Every positive length and every spectral parameter | claim quantifies over n, its lower bound, and u | No parameter is specialized. | | Two-dimensional tensor basis | Matrices indexed by functions from Fin n to Fin 2 | Coordinates start at zero. | | Four cases of (C.15) | Rcoef | The same equalities, inequalities and coefficients. | | $K^k_j=\bar K^k_j=\delta_{jk}$ | Kcoef, oneSite | The two boundary operators are identity coefficients on their sites. | | Two-site matrix units, (C.9)–(C.10) | twoSite | Row and column entries use $(k,j)=(x(a),y(a))$ and $(m,l)=(x(b),y(b))$; other coordinates agree. | | Ordered double row, (C.12) | preTrace | Descending first row, first boundary, ascending second row, auxiliary boundary. | | Auxiliary partial trace, (C.13) | transfer | Sum over the same appended auxiliary bit in row and column. | | Adjacent flips, (C.40) | hamiltonian | The bounded next-index proof only supplies the final adjacent site. | | $m_r(x)=\prod_{a=0}^{r-1}(x-(r-1-2a))$ | scalar mPoly | The full product, including $m_0=1$. | | $n_1!!/(n_2!!(n_1-n_2)!!)$, (C.65) | scalar dfBinom | Uses Int.toNat and Nat.doubleFactorial, giving $(-1)!!=0!!=1$. Only $-1$ can occur negatively in the claim. | | Both finite sums and all factors of (C.66) | claim | Natural half-index division and truncated subtraction; the summation bounds ensure the intended nonnegative indices. | | The universal equality | result | Proves the whole claim; its Scribe formula expands it in full. |

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.

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.

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.

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.

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,\ldots,40$ and the literal matrix comparison passes for $n=1,\ldots,4$. These are computed finite cross-checks, separate from the universal Lean proof.

| Item | Status | Evidence and scope | | --- | --- | --- | | Mathematical settlement | proved | Kernel-checked PonciniRasmussenTransferExpansion.result proves the full binding claim. | | Independent assessment of proof, prior art, proof shapes and module integration | open | Prior-art completeness and final review admission remain distinct from the kernel theorem. | | Priority or first-proof claim | open | Literature completeness is ASSUMED-UNVERIFIED; no novelty or priority claim is established. | | Review isolation | computed | Direct inspection of the supplied issue and proof route establishes repo-prior-exposed. This is a provenance fact, not a mathematical theorem or numerical experiment. | | Numerical checker | computed | The pinned experiment above exits 0 and reports PASS for scalar $n=1..40$ and literal matrices $n=1..4$ only. | | Binary Krawtchouk mechanism | proved | The generating polynomial on a Walsh eigenvector with $l$ sign changes is $(1+t)^{m-l}(1-t)^l$; its central factorial coefficients are the equality stated by central_spectral_coeff. | | Source's polynomial-algebra conclusion, (C.45) | proved | Each $m_r(h_n)$ is a polynomial evaluation at $h_n$; the finite linear combination in the proved equality is therefore a polynomial in $h_n$. | | Source's interpolation formula, (C.63) | open | The source supplies the interpolation argument; this delivery adds no formal theorem about that formula. |

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\ne0$. 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

| Declaration | proof_shape | escape_witness | Live consumer(s) | | --- | --- | --- | --- | | GVHunter.reverse_word_list | bind-only | none | count_reverse, word_eval_reverse, preTrace_eq_path | | D5.S1.Recurrence.CentralFactorialTransferExpansion.mPoly | bind-only | none | central_spectral_coeff, scalarExpansion, scalar_settlement, claim, centralCoeff, centralCoeff_central_difference, centralCoeff_one, centralCoeff_one_succ, centralCoeff_two_step, centralCoeff_zero, mPoly_central_difference, mPoly_comp_add_one, mPoly_comp_sub_one, mPoly_shift_succ, mPoly_shift_succ_right, mPoly_two_step, mPoly_zero, claim_of_spectral_obligations | | D5.S1.Recurrence.CentralFactorialTransferExpansion.dfBinom | bind-only | none | central_spectral_coeff, scalarExpansion, scalar_settlement, claim, dfBinom_choose, dfBinom_step, dfBinom_zero, claim_of_spectral_obligations | | D5.S1.Recurrence.CentralFactorialTransferExpansion.scalarEigenvalue | bind-only | none | scalar_settlement, claim_of_scalar_identity, claim_of_spectral_obligations, transfer_walsh | | D5.S1.Recurrence.CentralFactorialTransferExpansion.mPoly_zero | bind-only | none | centralCoeff_zero | | D5.S1.Recurrence.CentralFactorialTransferExpansion.mPoly_shift_succ | bind-only | none | mPoly_comp_sub_one, mPoly_two_step | | D5.S1.Recurrence.CentralFactorialTransferExpansion.mPoly_shift_succ_right | bind-only | none | mPoly_comp_add_one, mPoly_two_step | | D5.S1.Recurrence.CentralFactorialTransferExpansion.mPoly_two_step | bind-only | none | centralCoeff_two_step | | D5.S1.Recurrence.CentralFactorialTransferExpansion.mPoly_comp_add_one | bind-only | none | centralCoeff_one_succ, mPoly_central_difference | | D5.S1.Recurrence.CentralFactorialTransferExpansion.mPoly_comp_sub_one | bind-only | none | mPoly_central_difference | | D5.S1.Recurrence.CentralFactorialTransferExpansion.mPoly_central_difference | bind-only | none | centralCoeff_central_difference | | D5.S1.Recurrence.CentralFactorialTransferExpansion.dfac_step_nat | bind-only | none | dfac_step | | D5.S1.Recurrence.CentralFactorialTransferExpansion.dfac_cast_ne_zero | bind-only | none | dfBinom_zero | | D5.S1.Recurrence.CentralFactorialTransferExpansion.dfac_step | bind-only | none | dfBinom_step | | D5.S1.Recurrence.CentralFactorialTransferExpansion.dfBinom_zero | bind-only | none | dfBinom_choose | | D5.S1.Recurrence.CentralFactorialTransferExpansion.dfBinom_step | bind-only | none | dfBinom_choose | | D5.S1.Recurrence.CentralFactorialTransferExpansion.centralCoeff | bind-only | none | central_spectral_coeff, centralCoeff_central_difference, centralCoeff_one, centralCoeff_one_succ, centralCoeff_two_step, centralCoeff_zero, centralCoeff_zero_recurrence, centralSeries, centralSeries_central_difference, centralSeries_one, centralSeries_zero_ode, centralTransform_constantCoeff, centralWeighted_coeff, centralWeighted_coeff_even, coeff_transferSubst_trunc | | D5.S1.Recurrence.CentralFactorialTransferExpansion.centralCoeff_zero | bind-only | none | centralSeries_central_difference, centralSeries_one, centralSeries_zero_ode, centralSeries_zero_square, centralTransform_constantCoeff | | D5.S1.Recurrence.CentralFactorialTransferExpansion.centralCoeff_one | bind-only | none | centralSeries_zero_ode | | D5.S1.Recurrence.CentralFactorialTransferExpansion.centralCoeff_two_step | bind-only | none | centralCoeff_zero_recurrence | | D5.S1.Recurrence.CentralFactorialTransferExpansion.centralCoeff_central_difference | bind-only | none | centralSeries_central_difference | | D5.S1.Recurrence.CentralFactorialTransferExpansion.centralSeries | bind-only | none | centralSeries_central_difference, centralSeries_one, centralSeries_zero_ode, centralSeries_zero_square, centralTransform, centralTransform_constantCoeff, centralTransform_difference, centralTransform_one, centralTransform_zero, coeff_transferSubst_trunc | | D5.S1.Recurrence.CentralFactorialTransferExpansion.centralSeries_central_difference | bind-only | none | centralTransform_difference | | D5.S1.Recurrence.CentralFactorialTransferExpansion.halfBinomial | bind-only | none | central_spectral_coeff, centralTransform_constantCoeff, centralTransform_difference, centralTransform_difference_nat, centralTransform_nat, centralTransform_neg_nat, centralTransform_neg_one, centralTransform_one, centralTransform_zero, centralWeighted_coeff, centralWeighted_coeff_even, coeff_transferSubst_trunc, halfBinomial_add, halfBinomial_constantCoeff, halfBinomial_even_coeff, halfBinomial_mul_shift, halfBinomial_nat_mul, halfBinomial_nat_step, halfBinomial_odd_coeff, halfBinomial_two, halfBinomial_zero, inverseSqrt_square, transferSubst, transferSubst_X | | D5.S1.Recurrence.CentralFactorialTransferExpansion.halfBinomial_add | bind-only | none | centralTransform_difference_nat, centralWeighted_coeff, halfBinomial_mul_shift, halfBinomial_nat_mul, halfBinomial_nat_step, inverseSqrt_square | | D5.S1.Recurrence.CentralFactorialTransferExpansion.halfBinomial_zero | bind-only | none | centralTransform_nat, centralTransform_neg_nat, halfBinomial_nat_mul, inverseSqrt_square | | D5.S1.Recurrence.CentralFactorialTransferExpansion.halfBinomial_two | bind-only | none | centralTransform_difference_nat, halfBinomial_nat_step, inverseSqrt_square | | D5.S1.Recurrence.CentralFactorialTransferExpansion.halfBinomial_even_coeff | bind-only | none | centralWeighted_coeff_even, halfBinomial_constantCoeff | | D5.S1.Recurrence.CentralFactorialTransferExpansion.halfBinomial_odd_coeff | bind-only | none | centralWeighted_coeff_even | | D5.S1.Recurrence.CentralFactorialTransferExpansion.halfBinomial_constantCoeff | bind-only | none | centralTransform_zero | | D5.S1.Recurrence.CentralFactorialTransferExpansion.inverseSqrt_square | bind-only | none | centralTransform_zero | | D5.S1.Recurrence.CentralFactorialTransferExpansion.centralCoeff_zero_recurrence | bind-only | none | centralSeries_zero_ode | | D5.S1.Recurrence.CentralFactorialTransferExpansion.centralSeries_zero_ode | bind-only | none | centralSeries_zero_square | | D5.S1.Recurrence.CentralFactorialTransferExpansion.centralSeries_zero_square | content | centralSeries_zero_square | centralTransform_zero | | D5.S1.Recurrence.CentralFactorialTransferExpansion.centralCoeff_one_succ | bind-only | none | centralSeries_one | | D5.S1.Recurrence.CentralFactorialTransferExpansion.centralSeries_one | bind-only | none | centralTransform_one | | D5.S1.Recurrence.CentralFactorialTransferExpansion.transferSubst | bind-only | none | centralTransform, centralTransform_constantCoeff, centralTransform_difference, centralTransform_one, centralTransform_zero, coeff_transferSubst_trunc, transferSubst_X | | D5.S1.Recurrence.CentralFactorialTransferExpansion.transferSubst_X | bind-only | none | centralTransform_difference, centralTransform_one, centralTransform_zero | | D5.S1.Recurrence.CentralFactorialTransferExpansion.centralTransform | bind-only | none | central_spectral_coeff, centralTransform_constantCoeff, centralTransform_difference, centralTransform_difference_nat, centralTransform_nat, centralTransform_neg_nat, centralTransform_neg_one, centralTransform_one, centralTransform_zero, centralWeighted_coeff, centralWeighted_coeff_even, coeff_transferSubst_trunc | | D5.S1.Recurrence.CentralFactorialTransferExpansion.centralTransform_difference | bind-only | none | centralTransform_nat, centralTransform_neg_nat, centralTransform_neg_one | | D5.S1.Recurrence.CentralFactorialTransferExpansion.centralTransform_constantCoeff | bind-only | none | centralTransform_zero | | D5.S1.Recurrence.CentralFactorialTransferExpansion.centralTransform_zero | content | centralTransform_zero | centralTransform_nat, centralTransform_neg_nat, centralTransform_neg_one, centralTransform_one | | D5.S1.Recurrence.CentralFactorialTransferExpansion.centralTransform_one | content | centralTransform_one | centralTransform_nat, centralTransform_neg_one | | D5.S1.Recurrence.CentralFactorialTransferExpansion.centralTransform_neg_one | content | centralTransform_neg_one | centralTransform_neg_nat | | D5.S1.Recurrence.CentralFactorialTransferExpansion.halfBinomial_mul_shift | bind-only | none | centralTransform_nat, centralTransform_neg_nat | | D5.S1.Recurrence.CentralFactorialTransferExpansion.second_order_power | bind-only | none | centralTransform_nat, centralTransform_neg_nat | | D5.S1.Recurrence.CentralFactorialTransferExpansion.halfBinomial_nat_step | bind-only | none | centralTransform_nat, centralTransform_neg_nat | | D5.S1.Recurrence.CentralFactorialTransferExpansion.centralTransform_nat | content | centralTransform_nat | centralTransform_difference_nat | | D5.S1.Recurrence.CentralFactorialTransferExpansion.centralTransform_neg_nat | content | centralTransform_neg_nat | centralTransform_difference_nat | | D5.S1.Recurrence.CentralFactorialTransferExpansion.centralTransform_difference_nat | content | centralTransform_difference_nat | central_spectral_coeff | | D5.S1.Recurrence.CentralFactorialTransferExpansion.halfBinomial_nat_mul | bind-only | none | centralWeighted_coeff | | D5.S1.Recurrence.CentralFactorialTransferExpansion.coeff_transferSubst_trunc | bind-only | none | centralWeighted_coeff | | D5.S1.Recurrence.CentralFactorialTransferExpansion.centralWeighted_coeff | bind-only | none | centralWeighted_coeff_even | | D5.S1.Recurrence.CentralFactorialTransferExpansion.sum_even_residual | bind-only | none | centralWeighted_coeff_even | | D5.S1.Recurrence.CentralFactorialTransferExpansion.centralWeighted_coeff_even | bind-only | none | central_spectral_coeff | | D5.S1.Recurrence.CentralFactorialTransferExpansion.choose_shift_step | bind-only | none | dfBinom_choose | | D5.S1.Recurrence.CentralFactorialTransferExpansion.dfBinom_choose | bind-only | none | central_spectral_coeff | | D5.S1.Recurrence.CentralFactorialTransferExpansion.central_spectral_coeff | content | central_spectral_coeff | scalar_settlement | | D5.S1.Recurrence.CentralFactorialTransferExpansion.spectralPolynomial | bind-only | none | spectralPolynomial_degree, spectralPolynomial_eval_sum | | D5.S1.Recurrence.CentralFactorialTransferExpansion.spectralPolynomial_degree | bind-only | none | spectralPolynomial_eval_sum | | D5.S1.Recurrence.CentralFactorialTransferExpansion.spectralPolynomial_eval_sum | bind-only | none | scalar_settlement | | D5.S1.Recurrence.CentralFactorialTransferExpansion.homogeneous_term | bind-only | none | scalar_settlement | | D5.S1.Recurrence.CentralFactorialTransferExpansion.scalarExpansion | bind-only | none | scalar_settlement, claim_of_scalar_identity, claim_of_spectral_obligations | | D5.S1.Recurrence.CentralFactorialTransferExpansion.scalar_settlement | content | central_spectral_coeff | result | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.Rcoef | bind-only | none | twoSite, Rcoef_decomposition, Rcoef_swap, twoSite_factor, twoSite_swap | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.Kcoef | bind-only | none | oneSite, oneSite_eq_one | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.twoSite | bind-only | none | preTrace, operatorWord, operatorWord_cons, operatorWord_cons_cons, operatorWord_eq_path, preTrace_eq_path, twoSite_factor, twoSite_flip_covariance, twoSite_quad_covariance, twoSite_square, twoSite_swap | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.oneSite | bind-only | none | preTrace, oneSite_eq_one, preTrace_eq_path | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.preTrace | bind-only | none | transfer, preTrace_eq_path, transfer_product | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.transfer | bind-only | none | claim, claim_of_spectral_obligations, transfer_product, transfer_walsh | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.hamiltonian | bind-only | none | claim, claim_of_spectral_obligations, hamiltonian_eq_sum_flip, hamiltonian_walsh | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.claim | bind-only | none | result, claim_of_scalar_identity, claim_of_spectral_obligations | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.oneSite_eq_one | bind-only | none | preTrace_eq_path | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.Rcoef_swap | bind-only | none | twoSite_swap | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.Rcoef_decomposition | bind-only | none | twoSite_factor | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.twoSite_swap | bind-only | none | preTrace_eq_path | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.bitSign | bind-only | none | bitChar, bitChar_orthogonal, bitChar_rev, bitSign_mul, flipEigenvalue, flipEigenvalue_pair, flipOp_walsh | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.bitChar | bind-only | none | bitChar_orthogonal, bitChar_rev, flipOp_walsh, walsh, walsh_square | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.walsh | bind-only | none | adjacentQuad_walsh, claim_of_spectral_obligations, flipOp_walsh, hamiltonian_walsh, quadOp_walsh, transfer_walsh, walsh_right_cancel, walsh_square | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.bitChar_orthogonal | bind-only | none | walsh_square | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.walsh_square | bind-only | none | walsh_right_cancel | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.bitChar_rev | bind-only | none | flipOp_walsh | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.flipEquiv | bind-only | none | auxLift_flip_pair, auxLift_quad_pair, auxTrace_lift_mul_flip, auxTrace_lift_mul_quad, flipEquiv_apply, flipOp_apply, flipOp_comm, flipOp_square, flipOp_walsh, hamiltonian_eq_sum_flip, hamiltonian_walsh, quadOp, quadOp_walsh, swap_flip_comm, swap_flip_pair_general, twoSite_factor, twoSite_flip_covariance, twoSite_quad_covariance, twoSite_square | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.flipEquiv_apply | bind-only | none | flipOp_apply, flipOp_comm, flipOp_square, hamiltonian_eq_sum_flip, swap_flip_pair_general, twoSite_factor | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.flipEigenvalue | bind-only | none | adjacentQuad_walsh, adjacentValue, adjacentValue_ofFn, adjacentValue_product_closed, flipEigenvalue_pair, flipOp_walsh, hEigenvalue, hEigenvalue_succ, hamiltonian_walsh, quadOp_walsh, transfer_walsh | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.flipOp_walsh | bind-only | none | hamiltonian_walsh, quadOp_walsh | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.swapConfig_eq_iff | bind-only | none | twoSite_factor | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.rev_eq_iff_ne | bind-only | none | flipConfig_pair_eq_iff | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.flipConfig_pair_eq_iff | bind-only | none | hamiltonian_eq_sum_flip | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.flipConfig_swap_eq_iff | bind-only | none | twoSite_factor | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.twoSite_factor | bind-only | none | twoSite_flip_covariance, twoSite_square | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.equivMatrix_apply | bind-only | none | flipOp_apply, flipOp_comm, flipOp_square, swapOp_square, swap_flip_pair_general | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.flipConfig_comm | bind-only | none | flipOp_comm | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.flipConfig_involutive | bind-only | none | flipOp_square | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.flipOp_comm | bind-only | none | twoSite_flip_covariance | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.flipOp_square | bind-only | none | twoSite_square | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.swapOp_square | bind-only | none | twoSite_square | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.swap_flip_pair_general | bind-only | none | swap_flip_comm, twoSite_flip_covariance | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.swap_flip_comm | bind-only | none | twoSite_square | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.quadOp | bind-only | none | adjacentQuad, adjacentQuad_walsh, auxLift_adjacentQuad, auxLift_quad_pair, auxTrace_lift_mul_quad, operatorWord_cons, operatorWord_cons_cons, operatorWord_eq_path, pathQuad, pathQuad_eq_adjacentQuad_last, quadOp_walsh, transfer_product, twoSite_quad_covariance, twoSite_square | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.twoSite_flip_covariance | bind-only | none | twoSite_quad_covariance | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.twoSite_square | bind-only | none | operatorWord_cons, operatorWord_eq_path | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.twoSite_quad_covariance | bind-only | none | operatorWord_cons_cons, operatorWord_eq_path | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.flipOp_apply | bind-only | none | auxLift_flip_pair | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.operatorWord | bind-only | none | operatorWord_cons, operatorWord_cons_cons, operatorWord_eq_path | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.pathQuad | bind-only | none | operatorWord_eq_path, pathQuad_eq_adjacentQuad_last, preTrace_eq_path, transfer_product | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.operatorWord_cons | bind-only | none | operatorWord_cons_cons | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.operatorWord_cons_cons | bind-only | none | operatorWord_eq_path | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.operatorWord_eq_path | content | operatorWord_eq_path | preTrace_eq_path | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.preTrace_eq_path | content | preTrace_eq_path | transfer_product | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.auxLift | bind-only | none | auxLift_add, auxLift_adjacentQuad, auxLift_apply, auxLift_flip_pair, auxLift_mul, auxLift_one, auxLift_quad_pair, auxLift_smul, auxLift_snoc, auxTrace_lift, auxTrace_lift_mul_flip, auxTrace_lift_mul_quad, transfer_product | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.auxLift_apply | bind-only | none | auxLift_snoc, auxTrace_lift_mul_flip | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.auxLift_snoc | bind-only | none | auxLift_flip_pair, auxTrace_lift | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.auxLift_one | bind-only | none | auxLift_adjacentQuad, auxLift_quad_pair | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.auxLift_add | bind-only | none | auxLift_quad_pair | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.auxLift_smul | bind-only | none | auxLift_quad_pair | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.auxLift_mul | bind-only | none | auxLift_adjacentQuad | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.auxTrace | bind-only | none | auxTrace_add, auxTrace_lift, auxTrace_lift_mul_flip, auxTrace_lift_mul_quad, auxTrace_smul, transfer_product | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.auxTrace_add | bind-only | none | auxTrace_lift_mul_quad | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.auxTrace_smul | bind-only | none | auxTrace_lift_mul_quad | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.auxTrace_lift | bind-only | none | auxTrace_lift_mul_quad | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.auxTrace_lift_mul_flip | bind-only | none | auxTrace_lift_mul_quad | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.auxTrace_lift_mul_quad | bind-only | none | transfer_product | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.flipConfig_cast_snoc | bind-only | none | auxLift_flip_pair | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.auxLift_flip_pair | bind-only | none | auxLift_quad_pair | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.auxLift_quad_pair | bind-only | none | auxLift_adjacentQuad | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.adjacentQuad | bind-only | none | adjacentQuad_walsh, auxLift_adjacentQuad, pathQuad_eq_adjacentQuad_last, transfer_product, transfer_walsh | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.pathQuad_eq_adjacentQuad_last | bind-only | none | transfer_product | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.auxLift_adjacentQuad | bind-only | none | transfer_product | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.transfer_product | content | transfer_product | transfer_walsh | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.adjacentValue | bind-only | none | adjacentQuad_walsh, adjacentValue_ofFn, transfer_walsh | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.quadOp_walsh | bind-only | none | adjacentQuad_walsh | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.adjacentQuad_walsh | bind-only | none | transfer_walsh | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.adjacentValue_ofFn | bind-only | none | transfer_walsh | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.bitSign_mul | bind-only | none | flipEigenvalue_pair | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.flipEigenvalue_pair | bind-only | none | adjacentValue_product_closed, hEigenvalue_succ | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.adjacentValue_product_closed | bind-only | none | transfer_walsh | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.transfer_walsh | content | transfer_walsh | claim_of_scalar_identity | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.aeval_intertwiner | bind-only | none | claim_of_spectral_obligations | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.hamiltonian_eq_sum_flip | bind-only | none | hamiltonian_walsh | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.hEigenvalue | bind-only | none | claim_of_spectral_obligations, hEigenvalue_count, hEigenvalue_succ, hamiltonian_walsh | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.hamiltonian_walsh | bind-only | none | claim_of_spectral_obligations | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.hEigenvalue_succ | bind-only | none | hEigenvalue_count | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.hEigenvalue_count | bind-only | none | claim_of_spectral_obligations | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.signChanges_le | bind-only | none | claim_of_spectral_obligations | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.walsh_right_cancel | bind-only | none | claim_of_spectral_obligations | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.claim_of_spectral_obligations | bind-only | none | claim_of_scalar_identity | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.claim_of_scalar_identity | content | transfer_walsh | result | | D5.S3.StatisticalMechanics.VertexModels.PonciniRasmussenTransferExpansion.result | content | central_spectral_coeff | none (settling result) |

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.

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.