Real positive-definite counterexamples to extended q-permanent monotonicity

Dev D. Goyal

Real positive-definite counterexamples to extended q-permanent monotonicity

Dev D. Goyal · 2026 · Research preprint, not externally peer reviewed

Problem and result

Problem: Da Fonseca's q-permanent (μ-permanent) monotonicity conjecture
Posed in: Da Fonseca (2010), Conjecture 1; restated as Conjecture 2 in Da Fonseca (2018)
Status: Disproved
Result: A real symmetric positive-definite 5×5 matrix has q-permanent 8,968,822,249 at q = 14 and 7,441,960,000 at q = 15; for each real q₀ > 1 a positive-definite matrix (size depending on q₀) has negative derivative at q₀.

Abstract

For every real parameter q>1, a real symmetric positive-definite matrix has a negative q-permanent derivative at q. An explicit matrix of order five decreases from q=14 to q=15. Correlation matrices with no zero entries and integer-entry examples are also obtained. The dimension can depend on q. The real-symmetric question on [−1,1] remains outside the result.

Details

Year: 2026
Discipline: Mathematics
Area: Matrix theory
Subject: Matrix theory
Result type: Counterexample and all-parameter extension
Formal proof: Shared Lean library
Family: q-permanent
Keywords: q-permanent, permanent monotonicity, positive definite matrices, Da Fonseca conjecture, correlation matrices, matrix permanents

Statement and scope

Result summary. The catalogue summary repeats the abstract above, including its stated limits. The formally checked statements are listed under Formal proof.

A Lean check establishes only the formal statement that is checked. It does not establish novelty, historical priority or a faithful transcription of an external source. Known gaps are listed in UNFINISHED.md; the authorship disclosure describes how the results were produced.

Manuscript

PDF on this site: manuscript.pdf 314 KB
PDF on GitHub: papers/mathematics/q-permanent/paper.pdf
LaTeX source: papers/mathematics/q-permanent/paper.tex
Bibliography: papers/mathematics/q-permanent/references.bib

Formal proof

The selected theorems of this result are proved in the shared Lean 4 library of the repository. Its Comparator configuration checks each one against the matching statement in the Challenge module and permits only the axioms propext, Classical.choice and Quot.sound.

Proof module: lean/MathAndTheory/Mathematics/QPermanent/GeneralInteger.lean
Family sources: lean/MathAndTheory/Mathematics/QPermanent/
Challenge: lean/Challenges/Mathematics/QPermanent/Main.lean
Solution interface: lean/Solutions/Mathematics/QPermanent/Main.lean
Comparator file: lean/comparator/mathematics/q-permanent.json
Statement guide: lean/docs/mathematics/q-permanent.md
Toolchain: leanprover/lean4:v4.35.0

Checked theorems

Namespace MathAndTheory.QPermanent

QPermanentProblem.finite_counterexample
QPermanentProblem.extended_conjecture_false
QPermanentProblem.negative_derivative_at_every_parameter
QPermanentProblem.dense_correlation_counterexamples
QPermanentProblem.integer_counterexamples

Reproduce

The commands below are quoted from papers/mathematics/q-permanent/verification/README.md, which gives their context and working directory.

python3 papers/mathematics/q-permanent/verification/scripts/verify.py

README: papers/mathematics/q-permanent/README.md
Verification guide: papers/mathematics/q-permanent/verification/README.md
Repository guide: verification/README.md
Unfinished proofs: UNFINISHED.md

Source and prior work

Original problem. Da Fonseca, 2010, Conjecture 1; 2018, Conjecture 2.

Questions and answers

Is Da Fonseca's q-permanent monotonicity conjecture true?

No, for real symmetric positive-definite matrices: an explicit order-five matrix has P₁₄(A) > P₁₅(A), refuting the 2010 Conjecture 1 and the 2018 Conjecture 2. For every real q₀ > 1 there is a counterexample with negative derivative at q₀, though the dimension may depend on q₀.

Does this settle the Bapat–Lal question on [−1,1]?

No. Real-symmetric monotonicity on [−1,1] remains outside the result. Kitamura's public Lean formalization gives an order-144 complex Hermitian disproof on that interval, and Mitchell (2020) discussed positive semidefinite rank-one failures at negative parameters.

Is the proof formally verified?

Yes. Lean 4 proves the order-five example, the theorem for every parameter above one, and the dense correlation-matrix and integer-entry consequences. The witness dimension is not claimed to be minimal.

Cite

Citation file papers/mathematics/q-permanent/citation.bib. For the whole collection, use CITATION.cff or CITATION.bib.

@misc{goyal2026qpermanent,
  author = {Dev D. Goyal},
  title = {Real positive-definite counterexamples to extended q-permanent monotonicity},
  year = {2026},
  month = oct,
  howpublished = {Preprint},
  version = {1.0.0},
  url = {https://github.com/dvgyl/math-and-theory/tree/main/papers/mathematics/q-permanent},
  note = {Preprint, 26 October 2026. Not peer reviewed. Includes a Lean 4.35.0 formalization. See the collection's authorship disclosure for the autonomous research process.}
}