A q-permanent inequality for subset-preserving permutations
For $\sigma \in S_n$ let $\operatorname{inv}(\sigma)$ be the number of pairs $i < j$ with $\sigma(i) > \sigma(j)$. For $A = (a_{ij}) \in \mathbb{C}^{n \times n}$ and $q \in [0, 1]$ the $q$-permanent of $A$ is $$P_q(A) = \sum_{\sigma \in S_n} q^{\operatorname{inv}(\sigma)} \prod_{i=1}^n a_{i\sigma(i)},$$ with $0^0 = 1$. For $q = 1$ the inequality below is Lieb's inequality $\operatorname{per}(A) \ge \operatorname{per}(A[S])\operatorname{per}(A[S^c])$ for the principal submatrices on $S$ and its complement. If $S = \{1, \dots, k\}$, its right side is $P_q(A[S])\,P_q(A[S^c])$, and Lal proved it in that case; da Fonseca checked $n = 3$.
Problem. Let $n \ge 2$, let $A = (a_{ij}) \in \mathbb{C}^{n \times n}$ be Hermitian positive semidefinite, and let $q \in [0, 1]$. Is $$P_q(A) \ge \sum_{\substack{\sigma \in S_n \\ \sigma(S) = S}} q^{\operatorname{inv}(\sigma)} \prod_{i=1}^n a_{i\sigma(i)}$$ for every nonempty proper subset $S \subset \{1, \dots, n\}$? Here $\sigma(S) = S$ means that $\sigma$ maps $S$ onto itself, and the inversions on the right are counted in the ordering $1, \dots, n$ of all indices.
Source: Bapat and Lal (1994); see da Fonseca (2018), Conjecture 3.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- FA — Functional Analysis
- Secondary
- CO
- Keywords
- OpenProblemsInNLA, permanents, q-permanents
References
@article{bapat1994,
author = {Bapat, R. B. and Lal, A. K.},
title = {Inequalities for the $q$-permanent},
journal = {Linear Algebra Appl.},
volume = {197/198},
year = {1994},
pages = {397--409},
doi = {10.1016/0024-3795(94)90497-9},
}
@misc{dafonseca2018,
author = {da Fonseca, Carlos M.},
title = {The $\mu$-permanent revisited},
year = {2018},
eprint = {1804.02231},
archivePrefix = {arXiv},
}
@article{lieb1966,
author = {Lieb, Elliott H.},
title = {Proofs of some conjectures on permanents},
journal = {J. Math. Mech.},
volume = {16},
number = {2},
year = {1966},
pages = {127--134},
doi = {10.1512/iumj.1967.16.16008},
}
@misc{openproblemsinnla-mi19,
author = {Townsend, Alex},
title = {{MI-19}: A q-permanent inequality for subset-preserving permutations},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/matrix-inequalities-and-norms/MI-19/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00103.
namespace RegistryProblems.OP_00103
noncomputable section
open scoped BigOperators ComplexOrder
/-- The number of inversions in the full original ordering of `Fin n`.
The paper's index `i + 1` is represented by Lean index `i`. -/
def inversionCount {n : ℕ} (σ : Equiv.Perm (Fin n)) : ℕ :=
((Finset.univ : Finset (Fin n × Fin n)).filter
fun ij => ij.1 < ij.2 ∧ σ ij.2 < σ ij.1).card
/-- The term of the complex `q`-permanent belonging to a permutation.
The natural power retains the convention `0 ^ 0 = 1`. -/
def qPermanentTerm {n : ℕ} (q : ℝ) (A : Matrix (Fin n) (Fin n) ℂ)
(σ : Equiv.Perm (Fin n)) : ℂ :=
(q : ℂ) ^ inversionCount σ * ∏ i : Fin n, A i (σ i)
/-- The `q`-permanent, with all inversions counted in the original ordering. -/
def qPermanent {n : ℕ} (q : ℝ) (A : Matrix (Fin n) (Fin n) ℂ) : ℂ :=
∑ σ : Equiv.Perm (Fin n), qPermanentTerm q A σ
/-- Setwise preservation, not pointwise fixation and not an initial-segment test. -/
abbrev PreservesSubset {n : ℕ} (σ : Equiv.Perm (Fin n)) (S : Finset (Fin n)) : Prop :=
S.image σ = S
/-- The subset-preserving sum. The exponent still uses `inversionCount` on
all `n` positions; it is not a product of smaller `q`-permanents. -/
def restrictedQPermanent {n : ℕ} (q : ℝ) (A : Matrix (Fin n) (Fin n) ℂ)
(S : Finset (Fin n)) : ℂ :=
∑ σ ∈ (Finset.univ : Finset (Equiv.Perm (Fin n))).filter
(fun σ => PreservesSubset σ S), qPermanentTerm q A σ
/-- OP-00103: A q-permanent inequality for subset-preserving permutations -/
def _root_.RegistryProblems.Problem_OP_00103 : Prop :=
∀ n : ℕ, 2 ≤ n → ∀ A : Matrix (Fin n) (Fin n) ℂ, A.PosSemidef →
∀ q : ℝ, 0 ≤ q → q ≤ 1 → ∀ S : Finset (Fin n),
S.Nonempty → S ≠ Finset.univ → restrictedQPermanent q A S ≤ qPermanent q A
end
end RegistryProblems.OP_00103
Formalised by George Stepaniants (Apache-2.0); reviewed by clemens-admin.
Available to match against in: Lean v4.33.1 with Mathlib v4.33.1.
Resolving this problem in Lean
Add the problems package as a dependency, import this problem's module, and prove the constant. Any published revision works.
In lakefile.toml:
[[require]] name = "RegistryProblems" git = "https://github.com/cthalhammer/registry-problems" rev = "753bebc58e3fee845f4fffec7d24e7c8cc2a689a"
In your proof:
import RegistryProblems.OP_00103 theorem resolution : RegistryProblems.Problem_OP_00103 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00103" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00103 := by sorry
You can also write the statement out in full; the verifier checks it matches up to definitional equality. Partial results and reductions are not matched against this statement.
Resolution claims
Proves an actual complex Hermitian positive semidefinite Gram witness, evaluates its full and subset-preserving permutation sums, and refutes the complete original universal inequality by an exact strict gap.
For $A=(a_{ij})\in\mathbb M_n$ and real $q$, let $\operatorname{per}_q(A)=\sum_{\sigma}q^{\ell(\sigma)}\prod_i a_{i\sigma(i)}$, where $\ell(\sigma)$ is the number of inversions, and let $R_{q,S}(A)$ be the same sum restricted to permutations with $\sigma(S)=S$. The note shows that the subset inequality $\operatorname{per}_q(A)\ge R_{q,S}(A)$, asked for Hermitian positive semidefinite $A$ and $0\le q\le1$, is false. The counterexample is a real positive semidefinite matrix of order four and …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, MI-19/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00103, "A q-permanent inequality for subset-preserving permutations", clopen.solutions.