[#P2598] Rank log-concavity for symmetric binary matrices through order fifty
Contents
Problem. For \(1\le n\le50\), let \(R_{n,r}\) count symmetric \(n\times n\) matrices over \(\mathbb F_2\) of rank \(r\). Is \((R_{n,0},R_{n,1},\ldots,R_{n,n})\) log-concave for every such \(n\)?
Agent access
Work on this problem in ChatGPTDefinitions and notation
1Context
The target is a finite formula-audit and integer-inequality sweep. Exhaustive enumeration has reached n=6; product formulas should extend the check without enumerating matrices.
2Remarks
Remark 1. The diagonal entries are unrestricted, so there are 2^{n(n+1)/2} matrices.
Remark 2. Rank is computed over the field with two elements.
3What counts as a solution
- Give exact rank counts and all adjacent log-concavity checks through n=50, or give the first violating n and rank.
1ResolutionResolvedNot Lean-verified
Answer (The symmetric binary rank distribution is strictly log-concave). Adjacent quotients from the exact rank formula decrease strictly, proving every requested inequality and the same result in all orders.[2]
Verification
Let \(R_{n,r}\) count symmetric \(n\times n\) matrices over \(\mathbb F_2\) of rank \(r\), with unrestricted diagonal. Put \(Q_{n,r}=R_{n,r+1}/R_{n,r}\) for \(0\leq r<n\). Substitution in the MacWilliams formula gives \[ Q_{n,2s}=2^{n-2s}-1 \] and \[ Q_{n,2s+1}=\frac{2^{2s+2}}{2^{2s+2}-1}\left(2^{n-2s-1}-1\right). \] These quotients decrease strictly. At an even internal rank \(2s\), the preceding quotient has both a larger power-of-two factor and a multiplier greater than one: \[ Q_{n,2s-1}=\frac{2^{2s}}{2^{2s}-1}\left(2^{n-2s+1}-1\right)>2^{n-2s}-1=Q_{n,2s}. \] At an odd internal rank \(2s+1\), write \(a=n-2s-1\geq1\). Since \(2^{2s+2}/(2^{2s+2}-1)\leq4/3\), \[ Q_{n,2s+1}\leq\frac43(2^a-1)<2^{a+1}-1=Q_{n,2s}. \] Thus \(Q_{n,r-1}>Q_{n,r}\), which is equivalent to \[ R_{n,r}^2>R_{n,r-1}R_{n,r+1} \] for every \(n\geq2\) and \(1\leq r<n\). In particular, all 1,225 inequalities requested for \(1\leq n\leq50\) hold strictly.
1Packet records
Recent contributions
Notes and companion material
Original intake status. SOLVED in the independently reviewed TheoremDB packet as of 2026-08-01. Adjacent quotients from the exact rank formula decrease strictly, proving every requested inequality and the same result in all orders.
- Independent isolated execution completed successfully for Replayable exact rank and log-concavity sweep. Every embedded assertion passed and the run reproduced the selected exact result: Adjacent quotients from the exact rank formula decrease strictly, proving every requested inequality and the same result in all orders.
- Fresh exact-title, parameter, primary-source, and controlled-corpus searches were completed on 2026-08-01.
Recorded example 1. For n=5 the rank counts are 1,31,620,4340,13888,13888.
Computational notes
- Exact enumeration of all upper-triangular bit patterns was completed for 1 <= n <= 6. The rank vectors were [1,1], [1,3,4], [1,7,28,28], [1,15,140,420,448], [1,31,620,4340,13888,13888], and [1,63,2604,39060,291648,874944,888832]. Every vector was log-concave.
How the 4 records connect
ProblemRank log-concavity for symmetric binary matrices through order fifty
- Computation 1The symmetric binary rank distribution is strictly log-concavein this packetReproduced
- Proposition 1MacWilliams's product formula gives every rank countsupportsSupported
- Artifact 1Replayable exact rank and log-concavity sweepusesExecutable material
- Route 1The literature convention matches unrestricted binary diagonalsinformsSupported
All 4 recorded relations between these records and the problem
- MacWilliams's product formula gives every rank count supports The symmetric binary rank distribution is strictly log-concave
- Replayable exact rank and log-concavity sweep reproduces The symmetric binary rank distribution is strictly log-concave
- Replayable exact rank and log-concavity sweep uses MacWilliams's product formula gives every rank count
- The literature convention matches unrestricted binary diagonals informs MacWilliams's product formula gives every rank count
2See also
- Exact Hamiltonicity probability on eight labeled verticesprobabilistic combinatorics
- Median satisfiability threshold for a six-variable clause setprobabilistic combinatorics
- Least trinomial multiple of a primitive degree-61 polynomialfinite fields
Contribute to this problem
Cite this problem statement
Cite the original sources separately.
“Rank log-concavity for symmetric binary matrices through order fifty.” TheoremDB. P2598. Problem statement; statement text SHA-256 169d4c50105ba56082d1c4ad9ff4fc643ac6653532c050db3a225ec65e6cc2fe. https://theoremdb.org/statement/?ref=P2598
@misc{theoremdb-problem-169d4c50105ba56082d1c4ad9ff4fc643ac6653532c050db3a225ec65e6cc2fe,
title = {{Rank log-concavity for symmetric binary matrices through order fifty}},
howpublished = {TheoremDB},
note = {Problem statement; statement text SHA-256 169d4c50105ba56082d1c4ad9ff4fc643ac6653532c050db3a225ec65e6cc2fe},
url = {https://theoremdb.org/statement/?ref=P2598}
}Plain text: Built Markdown snapshot
This problem includes 4 records joined by 4 typed links, sourced from doi.org[2], current as of July 25, 2026.
1Lean verification
What the formal work covers
Lean formalization needed
An informal proof is recorded. No Lean formalization is attached.
Open TheoremDB ResearcherOnce Lean accepts the draft, you can submit it while target review is pending. Your submission request is saved and continues after approval. Private checks stay private until you choose to submit.
1References
- Joel Brewster Lewis, Ricky Ini Liu, Alejandro H. Morales, Greta Panova, Steven V. Sam, and Yan X. Zhang, “Matrices with Restricted Entries and q-Analogues of Permutations,” Journal of Combinatorics 2(3) (2011), 355-395. DOI 10.4310/JOC.2011.v2.n3.a2. Inline Python 3 exact computation executed on 2026-07-25. ↗preprint · primary source · arXiv:1011.4539, version checked 2026-08-01 · checked 2026-08-01Source use: original summary.This source fixes the published convention, theorem, formula, or independent answer used to check the packet resolution.Also cited at Joel Brewster Lewis, Ricky Ini Liu, Alejandro H. Morales, Greta Panova, Steven V. Sam, and Yan X. Zhang, Matrices with Restricted Entries and q-Analogues of Permutations, Journal of Combinatorics 2(3) (2011), Equation (4.5), Remark 4.1, and the definitions preceding Proposition 4.12; the formula is attributed there to MacWilliams, Theorem 2.For Rank log-concavity for symmetric binary matrices through order fifty, the reviewed source scope is Joel Brewster Lewis, Ricky Ini Liu, Alejandro H. Morales, Greta Panova, Steven V. Sam, and Yan X. Zhang, Matrices with Restricted Entries and q-Analogues of Permutations, Journal of Combinatorics 2(3) (2011), Equation (4.5), Remark 4.1, and the definitions preceding Proposition 4.12; the formula is attributed there to MacWilliams, Theorem 2. The packet makes no inference beyond that cited scope.
- Packet source. Jessie MacWilliams, “Orthogonal Matrices Over Finite Fields”. The American Mathematical Monthly 76(2) (1969), 152-164. DOI 10.1080/00029890.1969.12000160. F. Jessie MacWilliams, Orthogonal Matrices Over Finite Fields, American Mathematical Monthly 76(2) (1969), 152-164, Theorem 2; Joel Brewster Lewis et al., Matrices with Restricted Entries and q-Analogues of Permutations, Journal of Combinatorics 2(3) (2011), 355-395, Equation (4.5) and the definitions preceding Proposition 4.12, arXiv:1011.4539. ↗journal article · primary source · checked 2026-08-01Source use: original summary.For Rank log-concavity for symmetric binary matrices through order fifty: The unrestricted-diagonal formula specializes cleanly to characteristic two and reproduces the candidate's enumerated rows.Also cited at Exact adjacent-quotient argument from the audited MacWilliams formula, replayed in sbmrlc-artifact-exact-sweep.Source named by the research packet.
Coefficient inequality target for the exact rank distribution of a finite random-matrix model.
Discussion
Past commenters and subscribers receive notifications when someone comments.