Math and TheoryFinite real counterexamples and spectral obstructions for q-permanent monotonicity
Selected result in this collection
Problem and result
- Problem
- Real-symmetric case of the Bapat–Lal q-permanent monotonicity conjecture on [−1,1]
- Posed in
- Bapat and Lal, Linear Algebra Appl. 197–198 (1994); extended by da Fonseca (2010, Conjecture 1; 2018, Conjecture 2)
- Status
- Disproved for real symmetric positive-definite matrices
- Result
- An explicit integer positive-definite matrix of order 896 has a q-permanent that strictly decreases between two explicit rationals in (0,1); counterexamples exist in every order N ≥ 896.
Abstract
An explicit integer Gram matrix B of order 896 and rank three, with row coordinates at most 32 in absolute value, has a negative derivative of its inversion-weighted q-permanent at q = 1, by the exact integer comparison 1000U > 1001·C(896,2)·per(B). The integer matrix A = MB + I is positive definite, its q-permanent decreases between explicit rationals 0 < q₁ < q₂ < 1, and identity padding gives such counterexamples in every order N ≥ 896. This answers the real-symmetric case of the Bapat–Lal monotonicity conjecture on [−1,1] negatively and refutes da Fonseca's conjectures inside the original interval. For bounded-row fixed-rank perturbations I + (t/N)VVᵀ the endpoint derivative is eventually positive for every ordering when tλ_max(Σ) < 1 or tλ₃(Σ) ≤ 1 < tλ₁(Σ), and correlation counterexamples exist with condition number tending to 227.
Details
- Year
- 2026
- Discipline
- Mathematics
- Area
- Matrix theory
- Subject
- Matrix theory
- Result type
- Real-symmetric counterexample with an exact certificate, a Lean reduction and asymptotic obstructions
- Formal proof
- Standalone Lean package
- Family
q-permanent-finite- Keywords
- q-permanent, Bapat–Lal conjecture, permanent monotonicity, positive definite matrices, Da Fonseca conjecture, exact certificate, matrix permanents
Statement and scope
Formal scope. Lean 4.19.0 proves, for the inversion-weighted q-permanent of ordered real matrices, the endpoint identity 2D₁(VVᵀ) = C(n,2)‖f‖² − ‖G‖² for every real n × 3 matrix, soundness of the four-row integer certificate for every type list, the reduction of a negative endpoint to a rational positive-definite matrix with rational 0 < q₁ < q₂ < 1, identity padding, rank three of the frozen witness and the all-orders statement from its certificate inequality; a strict audit covers all 749 project declarations other than code-generation auxiliaries, with no native evaluation. The finite comparison for the 896-row witness is checked outside Lean by two independent exact programs, one of which determines per(B) and the wedge norms through the Chinese remainder theorem. The explicit regularization and the asymptotic and spectral theorems are conventional.
Lean 4.19.0 proves the endpoint identity for every real n × 3 matrix, soundness of the four-row integer certificate for every type list, the reduction of a negative endpoint to a rational positive-definite matrix with rational 0 < q₁ < q₂ < 1, identity padding, rank three of the frozen witness and the all-orders statement from its certificate inequality; a strict audit covers all 749 project declarations other than code-generation auxiliaries, with no native evaluation. The finite comparison for the 896-row witness is checked outside Lean by two independent exact programs. The explicit regularization and the asymptotic and spectral theorems are conventional.
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.pdf558 KB- PDF on GitHub
papers/mathematics/ q-permanent-finite/ manuscript.pdf - LaTeX source
papers/mathematics/ q-permanent-finite/ manuscript.tex - Bibliography
papers/mathematics/ q-permanent-finite/ references.bib
Formal proof
This result has a standalone Lean 4 package, separate from the shared library. Build it with the toolchain and instructions given in its README.
- Proof package
papers/mathematics/ q-permanent-finite/ - Lean project
papers/34 Lean filesmathematics/ q-permanent-finite/ lean/ - Lakefile
papers/mathematics/ q-permanent-finite/ lean/ lakefile.toml - Toolchain
leanprover/lean4:v4.19.0 - Library roots
Reproduce
The commands below are quoted from papers/, which gives their context and working directory.
Lean
bash scripts/verify.sh /tmp/q-permanent-finite-verificationExact certificate
python3 certificate/verify_certificate.py
python3 certificate/verify_certificate.py --recompute --primes 4
python3 certificate/verify_certificate.py --recompute --primes all- README
papers/mathematics/ q-permanent-finite/ README.md - Verification guide
papers/mathematics/ q-permanent-finite/ verification/ README.md - Verification record
papers/mathematics/ q-permanent-finite/ VERIFICATION.md - Authorship
papers/mathematics/ q-permanent-finite/ AUTHORSHIP.md - Repository guide
verification/README.md - Unfinished proofs
UNFINISHED.md
Source and prior work
Prior work. Bapat and Lal, Inequalities for the q-permanent, 1994.90497-9) · da Fonseca, 2010, Conjecture 1. · da Fonseca, 2018, Conjecture 2. · Kitamura, Lean disproof of the complex Hermitian case. · MI-18 problem record.
Questions and answers
Is the Bapat–Lal q-permanent conjecture true for real symmetric matrices?
No. An explicit integer Gram matrix B of order 896 and rank three has a negative q-permanent derivative at q = 1 by an exact integer comparison; A = MB + I is positive definite and P_{q₂}(A) < P_{q₁}(A) for explicit rationals 0 < q₁ < q₂ < 1. Adding an identity block gives counterexamples in every order N ≥ 896. Kitamura had earlier disproved the complex Hermitian case with a matrix of order 144.
How does this relate to da Fonseca's conjectures?
Da Fonseca's 2010 Conjecture 1 and 2018 Conjecture 2 assert monotonicity for real symmetric positive-definite matrices on intervals that contain [−1, ∞). The companion preprint refuted them for q > 1; this result gives failures inside (0,1). The minimum counterexample order and the negative half-interval remain open.
Is the proof formally verified?
Partly. Lean 4 proves the endpoint identity, the soundness of the integer certificate, the reduction to rational positive-definite counterexamples, identity padding and rank three, using only the standard axioms and no native evaluation. The final integer comparison for the 896-row input is checked by two independent exact programs, not in Lean; the explicit regularization and the asymptotic theorems are conventional.
Cite
Citation file papers/. For the whole collection, use CITATION.cff or CITATION.bib.
@misc{goyal2026qpermanentfinite,
author = {Goyal, Dev D.},
title = {Finite Real Counterexamples and Spectral Obstructions for {$q$}-Permanent Monotonicity},
year = {2026},
month = nov,
note = {Preprint. Fully autonomous agentic research; publication responsibility: Dev D. Goyal},
url = {https://github.com/dvgyl/math-and-theory/tree/main/papers/mathematics/q-permanent-finite}
}