TheoremDB
All problems

[#P2598] Rank log-concavity for symmetric binary matrices through order fifty

Checking solution status

Loading the current review decision.

Checking Lean verification
A mathematical schematic of Rank log-concavity for symmetric binary matrices through order fifty.
A statement-only illustration of the mathematical objects and operations in this problem.
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 accessWork on this problem in ChatGPT

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.

1Resolution

What counts as a solution

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

4 records

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
The overview places each record once. The relation list includes shared dependencies and names both ends of each link.

ProblemRank log-concavity for symmetric binary matrices through order fifty

All 4 recorded relations between these records and the problem

2See also

Contribute to this problem
Cite this problem statement

Cite the original sources separately.

Plain text
“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
BibTeX
@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}
}

This problem includes 4 records joined by 4 typed links, sourced from doi.org[2], current as of July 25, 2026.

1Lean verification

Lean formalization needed

An informal proof is recorded. No Lean formalization is attached.

Open TheoremDB Researcher

Upload a Lean project archive

Once 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

  1. 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.
  2. 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

Loading discussion.

Add a comment

Report comment

Flag this problem

Sign in to follow

Sign in in another tab, then return here.

Open sign-in in another tab

Report a problem

Report location:

Your ChatGPT account

Opening ChatGPT

ChatGPT is opening in a new tab.