# Exact finite-witness checker for Erdős Problem 1189

This directory is the independent acceptance gate for **finite examples** used
in the investigation.  It does not purport to answer the four open-ended
questions by itself; general formulae, bounds, or infinitude claims must
ultimately be proved in Lean.  The checker certifies the exact assertion:

> the listed, strictly increasing moduli form a covering set, witnessed by the
> listed residues, and no proper subset of those moduli is a covering set even
> after its residues are allowed to change.

## Candidate format

A whitespace-separated text file contains

```text
k
n_1 a_1
n_2 a_2
...
n_k a_k
```

with `1 < n_1 < ... < n_k` and canonical residues `0 <= a_i < n_i`.
There may be arbitrary whitespace but no comments or trailing tokens.

Example (`fixtures/classic_k5.txt`):

```text
5
2 0
3 0
4 1
6 5
12 7
```

## Build and run

```bash
cd check_answer
cargo test
cargo run --release -- fixtures/classic_k5.txt
```

Exit status 0 and a line beginning `PASS:` mean acceptance.  Every malformed,
unsupported, inconclusive, non-covering, or reducible input exits nonzero and
prints `FAIL:` with a reason.  The optional exact-search budget is increased as
follows (budget exhaustion still fails):

```bash
cargo run --release -- candidate.txt --max-nodes 500000000
```

## Exhaustive small census mode

After the Lean-proved universal bound `n_k ≤ 2^(k-1)`, the checker can
independently enumerate the complete ranges through `k=5`:

```bash
cargo run --release -- --verify-small-census
```

This tests every `k`-subset of `{2,…,2^(k-1)}`.  For each set it exactly decides
whether fresh residues can cover; for a covering set it repeats the decision
for every one-modulus deletion.  It exits successfully only if the recomputed
answer is empty for `k≤4` and exactly `{2,3,4,6,12}` for `k=5`.  The next mode
extends the same exhaustive computation through all 736,281 size-six
candidates and also verifies the exact extrema:

```bash
cargo run --release -- --verify-k6-census
```

For `k=7`, the stronger Lean theorem F-018 says all members divide one common
multiple `L≤64`.  The corresponding mode enumerates and deduplicates every
seven-element subset of the nontrivial divisors of every `1≤L≤64` (378
candidates rather than hundreds of millions):

```bash
cargo run --release -- --verify-k7-census
```

The same common-multiple method certifies all 7,443 candidates at `k=8`; its
65-set expected list is archived in `fixtures/k8_expected.txt`:

```bash
cargo run --release -- --verify-k8-census
```

A Rayon-parallel run similarly certifies all 159,225 common-multiple candidates
at `k=9`; its 318-set list is `fixtures/k9_expected.txt`:

```bash
cargo run --release -- --verify-k9-census
```

At `k=10`, the gate additionally applies the formal Simpson weight condition to
the actual LCM, reducing the exhaustive common-multiple search to 28,457
candidates; the 2,102-set result is `fixtures/k10_expected.txt`:

```bash
cargo run --release -- --verify-k10-census
```

At `k=11`, canonical exact-LCM enumeration gives 343,875 candidates. The gate
compares all 17,040 accepted sets with `fixtures/k11_expected.txt` and checks
minimum/maximum largest modulus `36/768` and reciprocal maximum `28/15`:

```bash
cargo run --release -- --verify-k11-census
```

For the Simpson-filtered modes, each set is generated exactly once at its
actual LCM; common multiples whose weight is already too large are skipped
before subset materialization.

Before constructing an LCM, all modes apply the rigorous exact rational union
bound `Σ1/n<1`; this safely rejects the vast majority of large-period
candidates. Search-budget exhaustion, period overflow on any remaining case,
or any mismatch is a failure, never an omitted case. This census implementation
is independent of the research generator in
`workspace/experiments/experiment_1_verifier_and_census/`.

## Why the checks match the definition

1. The parser enforces `1 < n_1 < ... < n_k` and one canonical residue per
   modulus.
2. Every listed progression is periodic modulo
   `L = lcm(n_1,...,n_k)`.  The checker examines all `x=0,...,L-1`, so accepting
   the displayed union is equivalent to covering every integer.
3. Covering is monotone under adding moduli.  Consequently a set is
   irreducible iff each subset obtained by deleting one modulus is
   non-covering.
4. For every such deletion the checker allows **new residues**.  It first uses
   the rigorous union bound `sum L/n_i < L` when applicable.  Otherwise it runs
   a complete depth-first decision procedure.  Translation invariance fixes
   the first residue to zero.  At any partial assignment it picks an uncovered
   point `x`; every completing cover must assign some unused modulus the unique
   residue `x mod n`, so branching over those moduli is exhaustive.  A capacity
   bound prunes only impossible branches.
5. Arithmetic overflow is checked.  Instances with common period above
   20,000,000, more than 128 moduli, or an exhausted DFS budget are rejected,
   never accepted.

The distinction in step 4 is important: merely showing that every displayed
congruence is essential would be weaker than irreducibility of the *modulus
set*, because a subset might cover after choosing different residues.

In census mode the same exact cover decision is applied first to the full bare
modulus set and then separately to every deletion.  Enumerating only deletions
is sufficient because covering is monotone under adding moduli.

## Cross-validation

`cross_validate.py` is a deliberately separate Python implementation for small
instances.  It enumerates all normalized residue assignments for every
one-modulus deletion, rather than using the Rust DFS.  Run:

```bash
python3 check_answer/cross_validate.py check_answer/fixtures/classic_k5.txt
bash check_answer/test.sh
```

The Python checker is exponential and intended only as an independent audit of
small fixtures.  The Rust source shares no code with candidate generators in
`workspace/`.

## Scope of the overall problem

The original prompt asks for the number of irreducible sets of each size, the
extreme largest modulus, the maximum reciprocal sum, and an infinitude result
for divisor sets.  A finite PASS establishes one data point only.  Any claimed
complete answer must state all quantifiers faithfully in Lean and build without
`sorry` or `admit`; no extrapolation from a census is accepted as a theorem.
