# Proof status for all dimensions

## Bottom line

As of 25 July 2026, the sources assembled here cover every integer dimension
in the standard statement of Dittert's conjecture, namely `n >= 2`. There is no
remaining dimension gap:

- peer-reviewed historical papers prove `n=2` and `n=3`;
- original local proof packages cover `n=4,5` and `n=8` through `n=16`;
- an attributed reconstruction of Lu's pinned source argument covers `n=6,7`;
  and
- Pang's June 2026 preprint proves every `n >= 17`.

It is therefore accurate to call this a **complete assembled working proof
chain**. It is not a self-contained proof developed wholly in this repository:
the local original arguments cover 11 of the 13 dimensions in the finite gap
`4 <= n <= 16`, while the remaining links import the sources identified
above. It is also not yet accurate to call the result a peer-reviewed or
community-settled theorem. The new local arguments, Lu's source argument, and
the recent preprint still need independent expert review. The `n=6,7` link is
an attributed reconstruction, not an unrelated independent discovery.

The [`unified`](unified/README.md) package is now the recommended mathematical
entry point. It reduces the finite range to a single scaling functional
`Psi(u) = M (1-u)^n - gamma_n + Delta(u)`, whose quadratic form gives one
closed-form margin that is positive on 293 of the 295 Hall cuts of
`8 <= n <= 16`. The two open rows are the marginal cuts of dimensions `8` and
`9`, and they close with the same functional and a sharper deficit bound. This
materially reduces the visible case split, but does not alter the provenance
or review status summarized here.

The convention in the literature starts at `n=2`. If `n=1` is included, the
only admissible matrix is `[1]`, and both sides of the asserted inequality are
equal to `1`.

## Coverage and provenance

| Range | Source used in the assembled chain | Status |
| --- | --- | --- |
| `n=2` | R. Sinkhorn, *A problem related to the van der Waerden permanent theorem*, [DOI 10.1080/03081088408817620](https://doi.org/10.1080/03081088408817620) | Peer-reviewed, 1984 |
| `n=3` | S.-G. Hwang, *On a Conjecture of E. Dittert*, [DOI 10.1016/0024-3795(87)90032-2](https://doi.org/10.1016/0024-3795(87)90032-2) | Peer-reviewed, 1987 |
| `n=4` | [`n4`](n4/README.md) exact certificate and three readers | Local working proof; a peer-reviewed [2024 structural result](https://doi.org/10.1515/spma-2024-0006) shows that any `K_4` maximizer is fully indecomposable, but does not settle `n=4` |
| `n=5` | [`n5`](n5/README.md) exact certificate | Local working proof |
| `n=6,7` | Hongyuan Lu's [source commit `56397b7`](https://github.com/lueluelue2006/dittert-n7-extension/tree/56397b70299278b338a286b90361180833dbf983), reconstructed and audited in [`n6-n7`](n6-n7/README.md) | Attributed working proof; two exact implementations; analytic layer under review |
| `n=8,9,10` | [`n8`](n8/README.md), [`n9`](n9/README.md), and [`n10`](n10/README.md) | Local working proofs with separate exact audits |
| `n=11,12,13` | [`n11-n13`](n11-n13/README.md) | Local working proof with independent exact audit |
| `n=14,15,16` | [`n14-n16`](n14-n16/README.md) | Local working proof with independent exact audit |
| `n >= 17` | Z. Pang, *Proof of Dittert's conjecture for dimensions n >= 17*, [arXiv:2606.01531v1](https://arxiv.org/abs/2606.01531v1) | Public preprint, 2026 |

Boris Kafidov's [independent `n=16` preprint](https://arxiv.org/abs/2607.19439v1)
is not needed to fill the range, but it provides a useful independent check at
the boundary between the finite packages and Pang's theorem.

The 1987 Hwang paper used for the `n=3` row is distinct from Hwang's 1986
positive-support paper cited in the finite-dimension proof notes. The
publisher's abstract for the 1986 paper explicitly lists, as its first result,
that a positive maximizing matrix must be the uniform matrix; see
[DOI 10.1016/0024-3795(86)90212-0](https://doi.org/10.1016/0024-3795(86)90212-0).
The 1987 paper instead proves the support-stationarity condition and settles
`n=3`. Thus the finite packages' `Hwang1986` attribution is intentional and
specific, even though Cheon--Wanless summarize Hwang's results collectively
under both papers.

## Audit performed on 25 July 2026

The post-merge tree at commit `ecc40ddfb62d2f1bc67f410673a3592040061a7d`
was checked with Python 3.12.11 and the exact dependency versions in
[`requirements-audit.txt`](requirements-audit.txt). The audit found no failed
certificate, missing enumerated case, checksum mismatch, optimized-mode
difference, or adversarial-test regression.

The successful checks included:

- every checksum manifest from `n4` through `n14-n16`;
- all primary exact verifiers and all separately implemented audits;
- the `n=6,7` verifier in ordinary and optimized mode;
- all 18 `n=6,7` package tests, including omitted-case and deep-certificate
  mutations;
- the package tests for `n=5`, `n=8`, `n=9`, and `n=10`; and
- the CI Ruff check for the attributed `n=6,7` package
  (`ruff check n6-n7`, on the Python 3.12 leg).

For Pang's large-dimension endpoint, the proof structure and cited hypotheses
were compared with the primary preprint and the Cheon--Wanless theorem it
uses. The unexpanded base calculation in Pang's Lemma 5 was recomputed with
exact rational arithmetic. With
`gamma_n = n! / n^n` and
`m_n = (n-2)! ((n-2) / (n-1)^2)^(n-2)`, the threshold margin at `n=17` is

```text
m_17 - gamma_17 - (3/4) * 17^3 * m_17^2 > 0.
```

The exact value has positive numerator
`11548021080448624744295835681397535132576763051329778264484827011759206465125`.
This confirms the finite threshold calculation; it is not a substitute for
external refereeing of Pang's complete analytic proof.

## What the software proves—and what it does not

The verification programs decide the finite algebraic obligations exactly:
certificate identities, rational comparisons, polynomial positivity,
Bernstein subdivisions, Sturm counts, and case enumerations. No
floating-point approximation is used as a correctness decision in those
checks.

The all-dimensions theorem also depends on human mathematics that is not
formalized in a proof assistant:

1. the published structural and permanent-minimization theorems cited in the
   dimension-specific notes;
2. the analytic reductions from an arbitrary boundary maximizer to the finite
   polynomial families;
3. Lu's dimension-six and dimension-seven Hall, stationarity, entropy, and
   two-level reductions; and
4. Pang's analytic argument for the infinite range.

The local notes spell out these dependencies, and the exact programs provide
strong reproducibility evidence for the computational layer. They do not turn
an under-review manuscript into a formally verified or peer-reviewed theorem.

Among the original local proofs, the `n=8` and `n=9` reductions deserve the
closest continuing human review. Their exact programs certify the reduced
polynomial and rational obligations, but do not independently validate every
stationarity, support, and cut-optimization step used to derive those
obligations. The `n=6,7` analytic layer remains a separate external trust
boundary because it is reconstructed from Lu's pinned source argument.

## Recommended wording

Use:

> This repository assembles a complete, reproducible working proof chain for
> Dittert's conjecture in every dimension. The new local and preprint portions
> have not yet completed external peer review.

Avoid an unqualified claim that the conjecture is “formally verified,”
“peer-reviewed,” or “universally settled.” When discussing `n=6,7`, cite Lu's
source argument as well as this reconstruction. When discussing the infinite
range, cite Pang's preprint directly.