Metadata

slug: sun210842
bibkey: sun2022arithmeticpermanents
doi: 10.48550/arXiv.2108.07723
url: https://arxiv.org/abs/2108.07723v7
triage: theorem
motivation_gids:
  - D5/S3/Combinatorics/Permanental/SunAbsoluteDifferenceCongruences.result

Sun Conjecture 4.2(i) absolute-difference permanent congruences

Problem

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 . v a l : Z) + 1) - ((k . v a l : Z) + 1) + s ∣$ for $j, k : 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.

Motivation

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.

Gap

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.

Route

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, \dots, 2 m$ with $p = 2 m + 1$ is $m + s$ . Clearing the factor 2 gives the two integer divisibilities.

Falsifier

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.

Evidence

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 \leq 101$ for shifts $0, 1$ , and the prime circulant checks at $p = 3, 5$ .

Triage

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 : ZMod (p) \to 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, \dots, 2 m$ equals $m + s$ for all $m : N$ and $s : 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, \dots, 8}$ , with values in $Z /9 Z$ . The odd-order entry identity of sign_entry, together with permanent_sign and permanent_map, identifies the reduction of $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 $Z /9 Z$ and conjugate permutations by $t$ . The weight $w (σ) = \prod_{x} f_{s} (σ (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 $σ (r + 3 k) = π (r) + 3 (k + a_{r})$ , with $r, k \in {0, 1, 2}$ , $π \in S_{3}$ , and each $a_{r} \in Z /3 Z$ . Conversely every such choice is a commuting permutation. Its weight is $\prod_{r} f_{s} (π (r) - r + 3 a_{r})^{3}$ , where arguments are reduced modulo $9$ . Summing independently over the three $a_{r}$ reduces the answer to the permanent of the $3 \times 3$ 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 + 3 a)^{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 $per (B_{0}) = 2 (- 1)^{3} \equiv 7 (mod 9)$ . For $B_{1}$ , only the identity and one $3$ -cycle contribute, each with weight $1$ , giving $per (B_{1}) \equiv 2 (mod 9)$ . Thus the two cleared expressions are congruent to $2 \cdot 7 + 1 \equiv 6$ and $2 \cdot 2 - 1 \equiv 3$ 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 \equiv 2 (mod 3)$ . The representative of $i - j$ is $2$ , so the right side is $(- 1)^{2} (2 + 2) = 4 \equiv 1 (mod 3)$ . 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.

ASSUMED-UNVERIFIED

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

Keyboard shortcuts

trureturing — Discovering truth