---
id: F-017
title: Exact value of the minimum monochromatic 3-AP density
tier: gate
polarity: positive
depends_on: [F-015, F-016]
supersedes: []
verifier: cd verified_math/F-017_delta3-exact/checker && /root/.cargo/bin/cargo build --release && ./target/release/check-continuum-rlt tests/continuum-rlt-548.txt && python3 tests/crosscheck_continuum_rlt.py && cd ../lean && /root/.elan/bin/lake update && /root/.elan/bin/lake exe cache get && /root/.elan/bin/lake build && ! grep -R -E '\b(sorry|admit)\b' Research Research.lean
date: 2026-07-12
---

## Statement

Let `M_3(n,c)` count pairs `(a,d)` with `1≤a`, `1≤d`, `a+2d≤n` whose three
terms have one color, and put

```text
δ_3 = liminf_{n→∞} min_c M_3(n,c)/n².
```

Then

```text
                       δ_3 = 117/2192.
```

This determines the constant asked for in Erdős Problem 1186 at `k=3` and
settles the Parrilo--Robertson--Saracino conjecture, including unrestricted and
rapidly alternating colorings.

## Proof / verification

### Quadratic lower-bound reduction

For a spin coloring write

```text
D={(u,v)∈[0,1]²:0≤2u-v≤1},
Q(x)=2∫∫_D x(u)x(v)dudv.
```

The exact PRS three-role identity has one endpoint-pair term whose leading
coefficient is a sum of the squared red/blue parity imbalances, hence is
nonnegative.  The other two roles give `Q`; equivalently

```text
M_3(n,c)/n² ≥ 1/16+Q(x)/8+o(1).                    (1)
```

A fixed 548-cell macroscopic partition makes this uniform for every discrete
coloring: full lattice rectangles give products of cell color proportions,
partial boundary polygons obey the same one-sided bounds, and the fixed number
of boundaries contributes only `O(n)`.  There is no block-count or regularity
assumption.

### Expansion around the twelve-block candidate

Let `s` have alternating run lengths

```text
28,6,28,37,59,116,116,59,37,28,6,28.
```

It is balanced and exact enumeration gives `Q(s)=-10/137`.  Write any other
coloring as `x=s(1-2p)` with `p∈{0,1}`.  Complementing `p` negates `x`, so
assume its measure is at most `1/2`.  If `h=Ks`, `a=-sh`, expansion gives

```text
[Q(x)-Q(s)]/4=∫ap+∫∫s(u)s(v)K(u,v)p(u)p(v)dudv.     (2)
```

For each of the 548 cells let `p_i∈[0,1]` be its flipped proportion.  The gate
uses exact prefix sums to prove the scaled field `548a` in cell `i` is uniformly
distributed on `[m_i,m_i+c_i]`, with integer `m_i≥0` and
`c_i∈{1,2,3}`.  The bathtub inequality therefore gives
`m_i p_i+c_i p_i²/2`.  It independently classifies every kernel cell rectangle
as full, empty, or partial.  Full rectangles are exact; on partial rectangles
same-candidate-color terms are discarded and opposite-color terms are bounded
by the containing full rectangle.  Thus

```text
548²[Q(x)-Q(s)]/4 ≥ f(p)
 =mᵀp+pᵀ(C+diag(c/2))p,    0≤p_i≤1, Σp_i≤274.      (3)
```

### Exact RLT certificate

The 1.2MB witness supplies nonnegative rational `N,R,η` and a PSD `P`, with

```text
P=H-N+(R+Rᵀ)/2+(η1ᵀ+1ηᵀ)/2,
H=C+diag(c/2),
R1+274η≤m.
```

With `ell=m-R1-274η`, Lean-verified RLT algebra rewrites

```text
f(p)=pᵀPp+pᵀNp+Σ_ij R_ij p_i(1-p_j)
    +Σ_iη_i p_i(274-Σ_jp_j)+ellᵀp ≥0.              (4)
```

The Rust verifier reconstructs every coefficient rather than trusting supplied
`m,c,C`: all 548 field distributions, all cell-pair classifications, all RLT
budgets, and the candidate score.  It verifies the symmetric and antisymmetric
274-dimensional sectors of `P` with integer factors plus exact symmetric
diagonally-dominant residuals.  An independent Python implementation repeats
every check with arbitrary-precision integers.  F-016 is a sorry-free Lean
proof of the RLT nonnegativity schema.

Equations (1)--(4) give

```text
δ_3≥1/16-(10/137)/8=117/2192.
```

The same gate independently enumerates weighted midpoint cells for `s`, finding
score `128232` and hence the matching upper construction
`δ_3≤117/2192` (F-015).  Therefore equality holds.
