# Exact certificate checkers for Erdős Problem 1186

This directory contains five independent Rust gates:

1. `check-ap-bound` verifies constructive periodic **upper bounds** for general
   `k`.
2. `check-sdp-lower` and `check-box-sos-lower` verify exact
   positive-semidefinite/Bell certificates for **lower bounds on `δ_3`**.
3. `check-interval-beads` verifies continuous equal-bead **upper bounds on
   `δ_3`**.
4. `check-continuum-rlt` verifies the exact 548-cell RLT certificate matching
   the lower and upper bounds and hence **determining `δ_3`**.

All use integer arithmetic only and share no source with their generators.

## Pinned-down convention

For `k >= 3`, a nontrivial `k`-term arithmetic progression in `[n]` is uniquely
represented by integers `(a,d)` with

```text
1 <= a,  1 <= d,  a + (k-1)d <= n.
```

For a coloring `c : [n] -> {0,1}`, let `A_k(c)` be the number of such pairs for
which all `c(a+jd)`, `0 <= j < k`, agree.  Set

```text
m_k(n) = min_c A_k(c),
delta_k = liminf_{n -> infinity} m_k(n)/n^2.
```

Thus any family of colorings with `A_k(c_n) <= (B+o(1))n^2` certifies
`delta_k <= B`.  Defining the extremal constant by `liminf` avoids silently
assuming that the limit exists.  Positive common difference excludes constant
progressions; each progression is counted once, not in both orientations.

This exactly spells out the convention implicit in `problem.md`.  Lower-bound
computer steps are proof certificates, not sampled searches: their exact
matrix identities are independently checked in Rust and Python, while F-014
and F-016 kernel-check the Bell/SOS and RLT certificate schemas in Lean.

### Statement fidelity

- `APParams` is `(start,step)` and `FitsIn n k` is exactly
  `1 ≤ start`, `0 < step`, `start+(k-1)step ≤ n`.
- `IsMonochromaticAP` checks all indices `0,…,k-1` against the first color.
- For the sharp `k=3` lower bound, the PRS identity is applied to every coloring
  after a fixed 548-cell macroscopic partition.  Cell variables are color
  proportions in `[0,1]`; no periodicity, measurability regularity, block-count
  bound, antisymmetry, or slow-alternation hypothesis is imposed.
- Replacing `n` by cell lengths with floors changes only `O(n)` pairs because
  the partition size is fixed.  Hence the result controls the same extremal
  `liminf`, without assuming an ordinary limit exists.
- Constant progressions are excluded and each positive-difference AP is counted
  once.  The separate ordered-endpoint normalization in the bead checker is
  converted explicitly by its factor `1/4`.

Thus the final matching lower and upper bounds concern exactly the `δ_3` in
`problem.md`.

## Certificate format

A UTF-8/ASCII file has exactly six lines:

```text
AP_PERIODIC_V1
k K
period Q
colors BITSTRING
claimed_mono_pairs M
claimed_bound NUM/DEN
```

`BITSTRING` has exactly `Q` bytes, all `0` or `1`.  It defines the coloring of
all positive integers by `c(x)=BITSTRING[(x-1) mod Q]`.  The checker independently
enumerates every pair `(alpha,r)` in `(Z/QZ)^2` and counts it when

```text
c(alpha) = c(alpha+r) = ... = c(alpha+(K-1)r).
```

It rejects unless this count is exactly `M` and `NUM/DEN` is exactly

```text
M / (2 (K-1) Q^2).
```

Fractions need not initially be reduced.  A conservative work cap rejects
resource-exhaustion inputs.  Exit status 0 means `PASS`; every malformed or
incorrect certificate exits nonzero with `FAIL: ...`.

## Why the checked quantity is a valid asymptotic bound

There are `n^2/(2(k-1)) + O_k(n)` admissible positive-difference `k`-APs in
`[n]`.  Fixing any residue pair `(a mod Q,d mod Q)` selects

```text
n^2/(2(k-1)Q^2) + O_{k,Q}(n)
```

of them: this follows by writing `a=alpha+Qu`, `d=r+Qv` in the triangular
region `a+(k-1)d <= n`; changing either residue only translates a fixed lattice
inside that triangle, affecting only `O(n)` boundary points.  Exactly `M` of
the `Q^2` residue pairs are monochromatic for the periodic coloring.  Hence

```text
A_k(c|_[n]) = M n^2/(2(k-1)Q^2) + O_{k,Q}(n),
```

which proves the upper bound printed by the checker.

## Equal-bead interval upper certificates

For `q` equal consecutive cells of `[0,1]`, choose ordered endpoints `x,y`
uniformly and put the midpoint at `(x+y)/2`.  If endpoint cell indices `i,j`
have even sum, the midpoint lies in cell `(i+j)/2` throughout their rectangle;
if their sum is odd, each of the two adjacent midpoint cells occupies exactly
half of the rectangle.  The checker therefore assigns integer weight `2` in
the even case and weight `1` to each half in the odd case, and enumerates all
`q²` endpoint-cell pairs exactly.

If the weighted monochromatic score is `M`, the continuous monochromatic
fraction is `M/(2q²)`.  The total number of positive-difference 3-APs in `[n]`
is `n²/4+O(n)`, while ordered endpoint pairs count each orientation, so the
coefficient in the normalization of `δ_3` is one quarter of the continuous
fraction, namely `M/(8q²)`.

The supplied 548-cell word has run lengths

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

and exact score `128232`, proving the published upper bound

```text
continuous fraction = 117/548,
δ_3 ≤ 117/2192.
```

## SDP lower-bound certificate

### Mathematical reduction

This is the block SDP argument of Parrilo--Robertson--Saracino (PRS08), with a
larger partition and a new exact dual certificate.  Fix an even `L` and split
`[n]`, initially with `L|n`, into `L` equal consecutive blocks.  Let `r_i` be
the number of red points in block `i`, put

```text
x_i = 2r_i/(n/L)-1 ∈ [-1,1],
B_ij = 1  iff  j+1 ≤ 2i ≤ j+L                  (1-based indices),
A = B+Bᵀ.
```

Let `N⁺` be the number of oppositely colored ordered pairs `(a,b)` for which
`2b-a∈[n]`.  All but `L` triangular boundary regions are covered by full block
rectangles.  Each triangle has asymptotic area `n²/(4L²)` (and exactly at most
`floor((n/L)²/4)` lattice points), while a full `(i,j)` rectangle has

```text
r_i(t-r_j)+(t-r_i)r_j = t²(1-x_i x_j)/2,  t=n/L.
```

Since `#supp(B)=L²/2`, this gives

```text
N⁺ ≤ n²/(4L) + n²/4 - n² xᵀAx/(4L²).                 (1)
```

If `A+diag(d_1,…,d_L)` is PSD, then for `|x_i|≤1`,

```text
xᵀAx ≥ -Σ d_i.
```

The standard 3-AP double count is exact up to an `O(n)` diagonal term:
`2M = 2·#AP - N⁺ - T`, where `T` counts bichromatic endpoint pairs of equal
parity and `T≤n²/8+O(n)`.  Combining with (1) yields

```text
δ_3 ≥ 1/16 - 1/(8L) - (Σd_i)/(8L²).                 (2)
```

For nonmultiples of `L`, restrict to the first `L floor(n/L)` points; the lost
`O_L(n)` term vanishes after division by `n²`.  Thus (2) applies to the exact
`liminf` convention above.

### Exact PSD witness format and check

A certificate begins `AP_SDP_LOWER_V1` and provides `L`, a denominator `D`, a
factor scale `R`, integer diagonal numerators `m_i`, and a lower-triangular
integer matrix `P`.  The checker reconstructs `A` from the displayed formula
and computes, with checked signed 128-bit integer arithmetic,

```text
C = D A + diag(m),
Q = R² C - D P Pᵀ.
```

It checks every entry and verifies that `Q` is symmetric diagonally dominant
with nonnegative diagonal.  This is an exact PSD proof because

```text
zᵀQz = Σ_i (Q_ii-Σ_{j≠i}|Q_ij|)z_i²
      + Σ_{i<j}|Q_ij|(z_i+sign(Q_ij)z_j)² ≥ 0.
```

Consequently `C=(D/R²)PPᵀ+Q/R²` is PSD, so (2) holds with
`d_i=m_i/D`.  The checker independently recomputes and reduces the claimed
fraction and requires it to strictly exceed the published PRS08 lower bound
`1675/32768`.

The supplied `L=256` certificate has

```text
D = 1,000,000,
Σm_i = 5,445,570,182,
δ_3 ≥ 13,533,214,909 / 262,144,000,000
    = 0.051625117908… > 1675/32768 = 0.051116943359… .
```

This closes `22.4958%` of the previously published gap to the upper bound
`117/2192`.  `tests/crosscheck_sdp.py` is an independent exact Python
implementation of the matrix reconstruction and all diagonal-dominance rows.

## Strengthened box-SOS lower-bound certificate

The diagonal SDP above ignores polynomial relations shared by three block
densities.  For every `u,v,w∈[-1,1]`, the four Bell polynomials

```text
1 + uv + uw + vw,
1 + uv - uw - vw,
1 - uv + uw - vw,
1 - uv - uw + vw
```

are nonnegative: each is multi-affine, so its minimum on the cube is attained
at a vertex, where its value is `0` or `4`.  Let `T_t` be the symmetric matrix
whose quadratic form is the nonconstant part of one such polynomial.

An `AP_BOX_SOS_LOWER_V1` certificate supplies nonnegative rational
multipliers `a_i, λ_t` and a PSD matrix `H` satisfying exactly

```text
A = H - diag(a) + Σ_t λ_t T_t.
```

Consequently, for every `x∈[-1,1]^L`,

```text
xᵀAx + Σ_i a_i + Σ_t λ_t
 = xᵀHx + Σ_i a_i(1-x_i²) + Σ_t λ_t(1+xᵀT_t x) ≥ 0.   (3)
```

The checker reconstructs the matrix identity.  As in the first certificate,
PSD is established without floating point: at common denominator `D` it checks
an integer factor plus a symmetric diagonally-dominant residual.  It also
checks all indices, signs, sums, reduced fractions, and the final PRS formula.

For `L=128`, the supplied 189,384-term exact SOS proves

```text
inf_{[-1,1]^128} xᵀA x ≥ -7,475,832,063 / 6,250,000,
δ_3 ≥ 42,924,167,937 / 819,200,000,000
    = 0.0523976659387207… .
```

This improves PRS08 by `0.0012807225793457…` and closes `56.6950%` of the
published gap to `117/2192`.  The construction is a rigorous level of the
block hierarchy suggested by the human review; it does **not** by itself prove
the conjectured equality.  `crosscheck_box_sos.py` independently reconstructs
all 189,384 Bell terms and the exact integer PSD residual.

## Matching continuum/RLT certificate: determination of `δ_3`

The final certificate proves that the twelve-block coloring is globally
optimal, including against rapidly alternating colorings.  Here is the complete
reduction audited by `check-continuum-rlt`.

### 1. The PRS quadratic and the discrete problem

Write a coloring as a spin `x:[0,1]→{±1}` and let

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

This is the continuum form of the two ordered adjacent-role pair sums in the
PRS identity.  For an arbitrary discrete coloring, the remaining endpoint
pair sum is, up to `O(n)`, a sum of two squares (one for each parity), hence is
nonnegative.  Equivalently, PRS's notation gives

```text
N⁺/n² = 1/4 - Q(x)/4 + o(1),
M_3(n,c)/n² ≥ 1/16 + Q(x)/8 + o(1).                 (4)
```

The fixed 548-cell argument below applies directly to every discrete coloring:
partition `[n]` into 548 consecutive macroscopic cells and use its color
proportions.  Full block rectangles have the stated products exactly up to
`O(n)`, partial boundary polygons only improve the conservative inequalities,
and the fixed number of lattice boundaries contributes `O(n)`.  Thus no
regularity or bounded-alternation assumption is made.

### 2. Expand around the candidate

Let `s` be the balanced 548-cell candidate with the twelve run lengths above.
Its exact bead score gives

```text
Q(s) = -10/137.
```

For any other spin coloring write

```text
x(u)=s(u)(1-2p(u)),  p(u)∈{0,1}.
```

Replacing `p` by `1-p` negates `x` and leaves `Q` unchanged, so assume
`∫p≤1/2`.  If `h=Ks` is the field of the symmetric kernel of `Q` and
`a=-s h`, direct expansion gives

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

### 3. Reduce every measurable perturbation to 548 numbers

Let `p_i∈[0,1]` be the fraction flipped in cell `i`; then
`Σp_i≤274`.  The checker reconstructs the candidate and evaluates the field at
both endpoints and the midpoint of every cell using exact integer prefix sums.
It verifies that, on cell `i`, the distribution of the scaled field
`548a` is exactly uniform on `[m_i,m_i+c_i]`, where

```text
m_i is a nonnegative integer,   c_i∈{1,2,3}.
```

Indeed the field is affine on each half-cell; the checker verifies that the two
halves either form one affine segment or traverse the same interval in opposite
directions.  The rearrangement/bathtub inequality therefore gives, for any
measurable flipped subset of relative measure `p_i`,

```text
548² ∫_{cell i} a p ≥ m_i p_i + (c_i/2)p_i².       (6)
```

For the quadratic term in (5), a cell rectangle is either full, empty, or cut
by one boundary of `D`.  On a full rectangle its contribution depends exactly
on `p_i p_j`.  On a partial rectangle, a same-candidate-color contribution is
nonnegative and may be discarded; an opposite-color contribution is at least
minus the corresponding full-rectangle product because the polygon is a
subset of the rectangle.  The checker independently classifies all pairs by
`r=2i-j` and reconstructs a rational symmetric matrix `C`.  Equations (5)--(6)
give the fully finite lower bound

```text
548²[Q(x)-Q(s)]/4 ≥ f(p)
 := mᵀp + pᵀ(C+diag(c/2))p.                        (7)
```

This is the step that controls arbitrary rapid alternation inside every cell.

### 4. Exact RLT proof that `f(p)≥0`

The certificate supplies nonnegative rational matrices `N,R`, a nonnegative
vector `η`, and a PSD matrix `P` satisfying

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

Consequently, writing `ℓ=m-R1-274η≥0`, exact algebra gives

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

Every term is visibly nonnegative for `0≤p_i≤1` and `Σp_i≤274`.
Reflection symmetry reduces `P` to 274-dimensional symmetric and
antisymmetric sectors.  The checker reconstructs (8) with integer arithmetic,
checks every row budget, and proves both sectors PSD by exact rational factors
plus symmetric diagonally-dominant residuals.  The independently recomputed
minimum residual margins are

```text
999945205470058000000,
999933318992062000000.
```

Combining (4), (7), and (9) proves

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

The verified twelve-block construction gives the reverse inequality, hence

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

`crosscheck_continuum_rlt.py` independently reconstructs all 548 field cells,
all 300,304 matrix entries, both exact PSD residuals, every RLT budget, and the
candidate score using Python arbitrary-precision integers.

## Build and use

```bash
cd check_answer
/root/.cargo/bin/cargo build --release
./target/release/check-ap-bound tests/alternating-k3.txt
./target/release/check-sdp-lower tests/sdp-l256.txt
./target/release/check-box-sos-lower tests/box-sos-l128.txt
./target/release/check-interval-beads tests/interval-beads-q548.txt
./target/release/check-continuum-rlt tests/continuum-rlt-548.txt
./tests/run_tests.sh
```

The test suite includes fixed positive/negative cases, independent Python
cross-checks of random periodic certificates and direct finite counts, a
negative mutation of the SDP certificate, and the full independent Python SDP
cross-check.
