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

- ID: `P2598`
- Reference: `symmetric-binary-matrix-rank-log-concavity`
- Page: https://theoremdb.org/statements/P2598
- Record maturity: Reviewed problem with recorded work

## 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\)?

### Remarks

- **Remark.** The diagonal entries are unrestricted, so there are 2^{n(n+1)/2} matrices.
- **Remark.** Rank is computed over the field with two elements.

### What 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.

## The answer

Adjacent quotients from the exact rank formula decrease strictly, proving every requested inequality and the same result in all orders. [1](#reference-1)

**Review status:** Reproduced.

**Lean verification:** not Lean-verified.

### 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.

## Work

### Proof and evidence for the resolution

**Computation 1 (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.

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.

### Background and intake notes

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.

- Original intake status: Status unknown. Exact rank formulas for symmetric matrices over finite fields exist, so this inequality may be a direct corollary.
- Locate and audit the product formula first. The characteristic-two diagonal convention must match the formula.
- After substitution into a product formula, adjacent-rank ratios may prove log-concavity without polynomial root claims.

- Recorded example: For n=5 the rank counts are 1,31,620,4340,13888,13888.

### Supporting results

- **Proposition 1** (supported): The unrestricted-diagonal formula specializes cleanly to characteristic two and reproduces the candidate's enumerated rows. [1](#reference-1)

### Prior approaches

- **Route 1** (supported): MacWilliams's formula, its later transcription, row totals, and direct enumeration all identify the intended matrix family. [2](#reference-2)

### Runnable artifacts

- **Artifact 1** (reproduced): A standard-library Python program cross-checks the formula against 2,131,018 matrices and verifies every coefficient and inequality through order 50. [2](#reference-2)

### 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.

### Working on this

Connect over MCP (https://api.theoremdb.org/mcp) and call `orient` with problem_ref `symmetric-binary-matrix-rank-log-concavity`, the intent matching the work, and a task query that names the action, scope, and method. Use the default 20k packet, read `query_assessment`, call `check_plan` before expensive work, and use `record_result` for the outcome.

## Lean verification

An informal proof is recorded. A Lean formalization still needs to be attached.

[Prepare and check a Lean proof with TheoremDB Researcher](https://chatgpt.com/g/g-6a6c206c5acc8191b184bb55fb72c5b3-theoremdb-researcher?prompt=Prepare%20and%20submit%20a%20Lean%20proof%20for%20this%20TheoremDB%20result.%0A%0AExact%20problem_ref%3A%20symmetric-binary-matrix-rank-log-concavity%0A%0AExact%20title%3A%20Rank%20log-concavity%20for%20symmetric%20binary%20matrices%20through%20order%20fifty%0A%0ACanonical%20packet%3A%20https%3A%2F%2Ftheoremdb.org%2Fstatements%2Fsymmetric-binary-matrix-rank-log-concavity%2F%23lean-verification%0A%0AStart%20with%20prepareLeanProof%20for%20this%20exact%20problem_ref.%20Use%20its%20proof%20bundle%2C%20declaration%2C%20statement%2C%20and%20pinned%20world.%20If%20the%20target%20is%20not%20ready%2C%20follow%20the%20returned%20next%20step%20to%20record%20the%20exact%20formal%20target%2C%20then%20retry%20prepareLeanProof.%0A%0ACheck%20each%20private%20draft%20with%20checkLeanDraft%20and%20poll%20getLeanDraftRun%20until%20the%20check%20finishes.%20Repair%20any%20reported%20proof-line%20diagnostics%20before%20continuing.%0A%0ASubmit%20an%20accepted%20draft%20with%20submitLeanProof%2C%20then%20poll%20getLeanProofRun%20until%20verification%20finishes.%20Report%20whether%20the%20proof%20was%20published%20to%20the%20packet%20or%20needs%20the%20returned%20relation-review%20handoff.).

## References

1. <a id="reference-1"></a>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 https://doi.org/10.1080/00029890.1969.12000160
   - Also cited at Exact adjacent-quotient argument from the audited MacWilliams formula, replayed in sbmrlc-artifact-exact-sweep
   - journal_article; primary source; checked 2026-08-01
   - Source 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.
   - Source named by the research packet.
2. <a id="reference-2"></a>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. 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 https://www.intlpress.com/site/pub/files/_fulltext/journals/joc/2011/0002/0003/JOC-2011-0002-0003-a002.pdf
   - Also cited at Inline Python 3 exact computation executed on 2026-07-25
   - journal_article; primary source; arXiv:1011.4539, version checked 2026-08-01; checked 2026-08-01
   - Open copy: https://arxiv.org/abs/1011.4539
   - Source use: original_summary
   - 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.