# Integrated claim for Erdős Problem 1189

## Verification boundary

The four questions are not all asserted at the same epistemic level.

- **Count asymptotic — published theorem plus a checked/internal reduction.**
  BBMST arXiv:1904.04806 supplies the external analytic enumeration. The
  fresh-residue frame theorem, upper injection, finite-fiber division, and
  arbitrary-size delta transfer are Lean-checked. The concrete restriction of
  BBMST's arithmetic-frame choices to distinct supports is proved in the
  self-contained `count_reduction.md`, but its PNT asymptotics remain cited
  mathematics, not Lean code.
- **Maximum largest modulus — unconditional exact Lean theorem.**
- **Minimum largest modulus — unconditional eventual Lean bounds.** This is an
  estimate, not an exact formula: `k+1≤m(k)≤Ck(log k)^6`.
- **Reciprocal maximum — unconditional order estimate in Lean.** This proves
  `Theta(log k)`, not a leading constant.
- **Divisor-set infinitude — unconditional Lean theorem.**

The quantifier-visible wrappers are in `Research/FinalClaims.lean`; complete
source and `#print axioms` output are in
`workspace/shared/erdos1189_lean_source.tar.gz`.

## Results

For the problem's strong notion (every proper subset may choose fresh
residues), let `I(k)`, `m(k)`, `M(k)`, and `R(k)` denote respectively the
number of irreducible `k`-sets, the minimum and maximum possible largest
modulus, and the maximum reciprocal sum.

1. **Count (BBMST + reduction).** With
   `tau = sum_{t>=1} log((t+1)/t)^2`,

   `log I(k) = (4*sqrt(tau)/3+o(1))*k^(3/2)/sqrt(log k)`.

   F-032--F-040 prove distinct arithmetic simple frames strong under fresh
   residues. F-048/F-049 prove the exact conditional finite interfaces. The
   external inputs and distinct-support counting argument are delimited in
   `count_reduction.md`.

2. **Exact maximum (Lean).** For every `k>=5`,

   `M(k)=3*2^(k-3)` (F-029).

3. **Minimum estimate (Lean).** Eventually,

   `k+1 <= m(k) <= 671088640000*k*(Nat.log 2 (k+1)+1)^6`,

   so `m(k)=k^(1+o(1))` (F-031/F-053).

4. **Reciprocal estimate (Lean).** `R(k)=Theta(log k)`. F-030 is the harmonic
   upper bound; F-047 gives a fixed `D>0` and, for every `k>=D`, a size-`k`
   irreducible set with reciprocal sum at least `Nat.log 64 (k/D)/8`.

5. **Infinitude (Lean).** For every odd prime `p`, all nontrivial divisors of
   `2^(p-1)*p` form an irreducible covering set (F-009).

Additionally, exact independently gated counts are
`I(1)=...=I(4)=0` and
`I(5),...,I(11)=1,4,15,65,318,2102,17040`.

The complete mathematical argument is `solution_draft.md`.
