Sun Conjecture 4.2(i) absolute-difference permanent congruences

Zhi-Wei Sun, Arithmetic properties of some permanents, arXiv:2108.07723v7, Conjecture 4.2(i), equations (4.3) and (4.4), asks whether for every odd prime $p$ the permanents of the matrices with entries $|j-k|$ and $|j-k+1|$ are congruent to $-1/2$ and $1/2$ modulo $p$, respectively. The integer encoding is $A_s(j,k)=|((j.val:\mathbb Z)+1)-((k.val:\mathbb Z)+1)+s|$ for $j,k : \operatorname{Fin} p$ and $s=0,1$.

Statement echo

The source permanent is the finite sum over permutations of products of row-indexed entries. The Lean claim clears the invertible denominator 2 and states both divisibilities for the same universally quantified odd prime.

The result settles the two explicitly numbered congruences in the source's open-conjecture section and gives a uniform prime-order mechanism for both absolute-difference shifts.

The source left both congruences conjectural. The bounded literature screen in issue #22003 found the Brualdi--Newman prime circulant congruence as the classical ingredient, but no prior proof of this absolute-difference pair. Literature completeness and worldwide priority remain ASSUMED-UNVERIFIED.

For odd prime $p$, alternating row and column signs reduce each absolute- difference matrix modulo $p$ to a circulant. Prime-order conjugation of permutation weights cancels nonfixed orbits in characteristic $p$; the fixed permutations are translations. Fermat's identity evaluates their weights, and the alternating sum over $0,\ldots,2m$ with $p=2m+1$ is $m+s$. Clearing the factor 2 gives the two integer divisibilities.

The settled claim is [ \forall p\in\mathbb N,;p\text{ prime}\to p\text{ odd}\to ((p:\mathbb Z)\mid 2\operatorname{per}(A_0)+1)\land ((p:\mathbb Z)\mid 2\operatorname{per}(A_1)-1). ] Its falsifier would be an odd prime and one failed divisibility.

The kernel-checked declaration is D5/S3/Combinatorics/Permanental/SunAbsoluteDifferenceCongruences.result. The escape audit for this public theorem is unfinished and is tracked in https://github.com/the-omega-institute/trureturing/issues/22464. The finite checks are in the pinned experiment directory. The script is docs/reports/sun-2108-conj42i-permanents/check.py, SHA-256 a549c0f6573ad0e1452dbe7719d51f6d6f7ed11d83e48917650986aed9cc4678. Command python3 -u /tmp/op-sun210842/experiment-rework/check.py, run on the exact script bytes extracted from that commit, exits 0 and reports the exact target checks for odd primes $p=3,5,7,11,13,17,19$, the sign reduction at every odd prime $p\le101$ for shifts $0,1$, and the prime circulant checks at $p=3,5$.

| item | status | evidence | | --- | --- | --- | | Both Conjecture 4.2(i) divisibilities for every odd prime. | proved | Kernel-checked SunAbsoluteDifferenceCongruences.result; the alternating-sign, prime-orbit and telescoping-sum mechanism is the proof route. | | For every prime $p$ and $f : \operatorname{ZMod}(p)\to\operatorname{ZMod}(p)$, the permanent of the circulant equals $\sum_a f(a)$, including $p=2$. | proved | The consumed private permanent_circulant declaration in the settling proof, using prime-order fixed-point counting. This is the Brualdi--Newman ingredient and is not claimed as new mathematics. | | The alternating-sign entry reduction holds at every odd natural order for shifts $s=0,1$. | proved | The consumed private sign_entry declaration. | | The alternating weighted sum over $0,\ldots,2m$ equals $m+s$ for all $m:\mathbb N$ and $s:\mathbb Z$. | proved | The consumed private alternating_sum declaration. | | The odd composite extension fails at $n=9$ for both shifts. | proved in prose | The cyclic-orbit reduction below gives the cleared residues $6$ and $3$ modulo $9$. | | The same entry identity fails at shift $2$. | proved in prose | Direct substitution below gives residues $2$ and $1$ for $p=3$, $i=0$, $j=1$, $s=2$. | | Classification for other shifts, composite moduli and stronger prime-power congruences. | open | No declaration in this delivery settles these neighbouring questions. | | Lean formalization of part (ii)'s reciprocal-sum formula. | open | The screened Jiang--Sun paper addresses that distinct formula; no Lean declaration here addresses it. |

Neighbouring assertions proved in prose

The following arguments establish the neighbouring claims without using the finite experiment above. They are paper proofs, not additional Lean theorems.

For $s\in{0,1}$ put $f_s(u)=(-1)^u(u+s)$ for the representative $u\in{0,\ldots,8}$, with values in $\mathbb Z/9\mathbb Z$. The odd-order entry identity of sign_entry, together with permanent_sign and permanent_map, identifies the reduction of $\operatorname{per}(A_s)$ at order $9$ with the permanent of the circulant with entries $f_s(x-y)$. Those three helpers require no primality assumption.

Let $t(x)=x+1$ on $\mathbb Z/9\mathbb Z$ and conjugate permutations by $t$. The weight $w(\sigma)=\prod_x f_s(\sigma(x)-x)$ is constant on each orbit. The orbit sizes divide $9$. Orbits of size $9$ contribute zero modulo $9$; the union of the other orbits is exactly the set of permutations commuting with $t^3$. Hence the circulant permanent equals the sum of $w$ over this set.

Every permutation commuting with $t^3$ has a unique description $\sigma(r+3k)=\pi(r)+3(k+a_r)$, with $r,k\in{0,1,2}$, $\pi\in S_3$, and each $a_r\in\mathbb Z/3\mathbb Z$. Conversely every such choice is a commuting permutation. Its weight is $\prod_r f_s(\pi(r)-r+3a_r)^3$, where arguments are reduced modulo $9$. Summing independently over the three $a_r$ reduces the answer to the permanent of the $3\times3$ matrix $B_s(r,q)=b_s(q-r)$, where indices are modulo $3$ and $b_s(d)=\sum_{a=0}^2 f_s(d+3a)^3$.

The six entries are obtained by the explicit integer sums [ \begin{aligned} b_0(0)&=0^3+(-3)^3+6^3\equiv0,& b_0(1)&=(-1)^3+4^3+(-7)^3\equiv-1,& b_0(2)&=2^3+(-5)^3+8^3\equiv-1,\ b_1(0)&=1^3+(-4)^3+7^3\equiv1,& b_1(1)&=(-2)^3+5^3+(-8)^3\equiv1,& b_1(2)&=3^3+(-6)^3+9^3\equiv0 \pmod9. \end{aligned} ] For $B_0$, only the two $3$-cycles contribute, giving $\operatorname{per}(B_0)=2(-1)^3\equiv7\pmod9$. For $B_1$, only the identity and one $3$-cycle contribute, each with weight $1$, giving $\operatorname{per}(B_1)\equiv2\pmod9$. Thus the two cleared expressions are congruent to $2\cdot7+1\equiv6$ and $2\cdot2-1\equiv3$ modulo $9$, respectively. Both are nonzero. This proves failure of the odd-composite extension at order $9$; it makes no claim about other composite orders or exact integer permanent values.

For the shift-$2$ entry identity take $p=3$, $i=0$, $j=1$. Its left side is $(-1)^{0+1}|0-1+2|=-1\equiv2\pmod3$. The representative of $i-j$ is $2$, so the right side is $(-1)^2(2+2)=4\equiv1\pmod3$. The entries are unequal.

What the settlement shows

Proved by result: both absolute-difference permanent congruences hold for every odd prime. The decisive mechanism is the alternating-sign reduction to a prime circulant, cancellation of nonfixed permutation-weight orbits, and the fixed-translation evaluation.

Scope: the entry reduction is proved for odd natural orders and shifts $s=0,1$; the counting step requires primality. The argument does not settle other shifts, composite moduli or prime-power strengthening.

Effect on the source: Conjecture 4.2(i), including (4.3) and (4.4), is settled positively. Part (ii) is a separate assertion addressed by the screened Jiang--Sun paper; its Lean formalization is outside this delivery.

The literature search is bounded by the sources and services recorded in issue #22003. It does not certify exhaustive worldwide priority or completeness.