Shao–Zhao cycle Italian-domination recurrence

P. Shao and C. Zhao, Counting Weight-k Italian Dominating Sets on Trees and Cycles, arXiv:2610.00108v1, §9 (verbatim):

Several directions remain open for future work: … • Deriving a complete linear recurrence for the total count Σ_k d_I(C_n, k) using the transfer matrix formulation (the observed limiting ratio ≈ 2.7843 is the dominant eigenvalue of the corresponding transfer matrix).

The preregistered issue is #12435. The settled statement is that, for every natural n ≥ 3, the total count a(n) satisfies a(n+5) = 2a(n+4) + 2a(n+3) + a(n+2) − a(n+1) − a(n), with a(3), …, a(7) = 23, 60, 167, 467, 1297.

The source leaves the transfer-matrix recurrence open. The frozen declaration D5/S3/Combinatorics/Graph/CycleItalianDominationRecurrence.result resolves that named question for labelled cycles and supplies the initial values needed to determine every later count.

Before this module, the source's complete constant-coefficient recurrence and its determining initial values were absent from the repository. The source's other §9 directions, including unimodality and closed forms for d_I(C_n, 2n−j), remain outside this settlement.

Represent a function on Fin n by its consecutive value pairs in Fin 3 × Fin 3. The Italian condition is exactly the admissibility condition on each transition of the nine-state transfer matrix T. The closed-walk equivalence gives a(n) = trace(T^n). Grouping rows into the five classes {(0,0)}, {(1,0)}, {(2,0)}, {(*,1)}, and {(*,2)} gives T = R S and S R = Q. The exact identity Q^5 − 2Q^4 − 2Q^3 − Q^2 + Q + I = 0 and trace cyclicity yield the displayed recurrence; direct traces give the five initial values.

A counterexample would be a natural n ≥ 3 for which the integer recurrence fails, one of the five initial values differs, or the closed-walk correspondence fails for an Italian function or a closed transfer-matrix walk. The Lean theorem result checks the universal statement and the initial values in the kernel.

• Proved: result in D5/S3/Combinatorics/Graph/CycleItalianDominationRecurrence.lean proves the recurrence and all five initial values with the standard three axioms.
• Computed: exhaustive enumeration for n = 3..14 gives 23, 60, 167, 467, 1297, 3612, 10058, 28003, 77970, 217095, agreeing with the recurrence.
• Computed: Hankel ranks of the enumerated sequence give rank five and exclude orders at most four; the characteristic polynomial is irreducible over ℚ and its dominant root is 2.7843303…, matching the source's observed ratio.
• Computed: the weighted transfer matrix Q(w) = diag(1,1,1,w,w²) Q yields the weighted recurrence recorded in the implementation probe.

proved for the named §9 recurrence task.

What the settlement shows

• Proved: the unweighted total count on every labelled cycle C_n, n ≥ 3, is generated by an order-five constant-coefficient recurrence with the five displayed initial values.
• Computed: order five is minimal for the computed sequence; the irreducible characteristic polynomial has dominant root 2.7843303…, explaining the source's observed limiting ratio.
• Computed: the same transfer-matrix argument gives the weighted recurrence for D_I(C_n, w) with Q(w) = diag(1,1,1,w,w²) Q.
• Open: unimodality of the weight distribution and closed forms for d_I(C_n, 2n−j) are not settled here.

The result supplies the missing total-count recurrence while leaving those weight-refined questions available for separate work.

The literature search and the claim that no later publication resolves the source's §9 bullet are bounded by the surfaces recorded in issue #12435. The numerical minimality, irreducibility, dominant-root and weighted statements are supporting computations; only the unweighted recurrence and its initial values are the kernel-checked settlement in this dossier.