# Verifier for Erdős Problem 320

This is a **proof problem**, not a finite-witness problem.  The only verifier for
a general estimate is Lean 4 + Mathlib.  The Rust executable here is a second,
independent implementation used only to cross-check finite values and the
formal definition.

## Faithful formal object

The pinned definition is in
[`../workspace/experiments/experiment_1_unit_fraction_sums/lean/Research/SubsetSums.lean`](../workspace/experiments/experiment_1_unit_fraction_sums/lean/Research/SubsetSums.lean):

```lean
def reciprocalSubsetSum (A : Finset ℕ) : ℚ :=
  ∑ n ∈ A, (1 : ℚ) / (n + 1)

def reciprocalSubsetSums (N : ℕ) : Finset ℚ :=
  (Finset.range N).powerset.image reciprocalSubsetSum

def S (N : ℕ) : ℕ := (reciprocalSubsetSums N).card
```

Line-by-line correspondence with `problem.md`:

1. `Finset.range N` is `{0,...,N-1}`.
2. Index `n` contributes `1/(n+1)`, so the denominators are exactly
   `{1,...,N}` and zero is never a denominator.
3. `powerset` ranges over **all** subsets, including the empty subset.
4. `image reciprocalSubsetSum` removes duplicate rational values.
5. `Finset.card` therefore counts distinct sums, exactly as required.
6. The codomain is `ℚ`; equality and all sums are exact, not floating point.

The English request “Estimate `S(N)`” does not prescribe a particular error
term or conjectured comparison function.  It cannot honestly be translated
into one arbitrary stronger-looking proposition.  Every proposed result must
therefore state explicit quantified lower/upper functions (the file provides
`EventuallySandwiched`) and its statement must be audited for mathematical
significance against the best bounds recorded in `notebook.md`.  A final claim
counts only if the exact audited theorem builds with no proof escape hatch.

## Final pinned estimate

The final theorem is
`ResearchPNT.exists_two_sided_full_product_estimate` in
`workspace/experiments/experiment_4_lower_analytic_iteration/pnt_lean/ResearchPNT/FinalEstimate.lean`.
It states that positive constants `c,C` eventually sandwich `log S(N)` between
`c` and `C` times

```text
(N / log N) * renewalProduct N (logLogNat N).
```

Here `logLogNat N = log(log N)=log₂N`. `renewalProduct` multiplies `log x` and
recurses on `log x` while `x>exp 3`, so its factors are exactly the stopped
sequence `log₃N, log₄N, …`. F-028 proves height `N` has already passed the
stopping depth. Thus the formal statement is precisely

```text
log S(N) ≍ (N/log N) ∏_{j≥3, stopped} log_j N.
```

Exact final audit:

```bash
check_answer/verify-lean-theorem.sh \
  workspace/experiments/experiment_4_lower_analytic_iteration/pnt_lean \
  ResearchPNT.FinalEstimate \
  ResearchPNT.exists_two_sided_full_product_estimate
```

The script rejects source occurrences of `sorry`, `admit`, custom `axiom`,
`opaque`, and `unsafe`, builds the project, and audits the exact theorem's axiom
closure.

## Independent exact finite checker

Candidate format is one UTF-8 text file containing exactly

```text
N EXPECTED_S_N
```

with optional `#` comments.  The checker supports `0 <= N <= 24`.  It computes
`L = lcm(1,...,N)`, replaces each `1/n` by the integer `L/n`, enumerates all
integer subset sums in a hash set, and compares the exact cardinality.  It
shares no code with research programs.

```bash
cd check_answer
cargo run --release -- --self-test
printf '6 52\n' >/tmp/candidate.txt
cargo run --release -- /tmp/candidate.txt
```

Exit code 0 and a line beginning `PASS` mean acceptance; every parse error,
range violation, or incorrect count exits nonzero with a reason.  The self-test
uses independently published OEIS A072207 values for `S(0),...,S(20)`.
