# Rigorous reduction of BBMST counting to irreducible modulus sets

Let `A(k)` be the number of minimal covering systems counted by Balister--Bollobás--Morris--Sahasrabudhe--Tiba (BBMST), and let `I(k)` be the number in Problem 1189. Put

\[
 f(k)=\frac{k^{3/2}}{\sqrt{\log k}},\qquad
 c=\frac{4\sqrt\tau}{3},\qquad
 \tau=\sum_{t\ge1}\log(1+1/t)^2.
\]

## External inputs, exactly delimited

Only the following published statements/estimates from BBMST are used.

1. **Theorem 1.1:** `log A(k)=(c+o(1))f(k)` for all minimal displayed
   covering systems.
2. **Section 5, Lemmas 5.3 and 5.5 / equations (19)--(21):** the lower
   systems at size
   `n(x)=1+Σ_(p,e)<x (p-1)` are arithmetic simple frames; if `Q(x)` is the
   logarithm of the number of independent predecessor-support choices, then
   `Q(x)=(c+o(1))f(n(x))`,
   `n(x)=(tau+o(1))*x^2/(2 log x)`, and for one layer
   `log D_(p,e)=(tau+o(1))*y_(p,e)/log y_(p,e)` as `y_(p,e)→∞`.
3. **The gap sentence in the proof of Proposition 5.1:** for maximal `x` with
   `n(x)≤k`, `k-n(x)<x=o(k)`.
4. **Lemma 6.2:** prescribed ordered moduli support at most `(k!)^2` minimal
   displayed systems.

The paper also explicitly states after Theorem 1.1 that its lower bound is
proved with distinct moduli.  Below I nevertheless derive that restriction
from item 2, so the bridge does not hide behind that sentence.  Everything
else below is either elementary or one of the cited Lean theorems.  In
particular, the published analytic estimates above are **not** claimed to have
been formalized in Lean; `Erdos1189Final.count_answer_reduction` displays the
exact finite hypotheses at the machine-checked boundary.

## 1. Upper bound

For each irreducible modulus set S choose one witnessing residue cover C(S). It is a minimal covering system in BBMST's ordinary sense: if deleting one displayed class left a cover, then the corresponding proper subset of S would be a covering modulus set (using those displayed residues), contrary to strong irreducibility. If S and T differ, C(S) and C(T) have different modulus multisets. Thus S↦C(S) is injective and

\[
 I(k)\le A(k)=\exp((c+o(1))f(k)).
\]

## 2. Why a distinct arithmetic simple frame is strongly irreducible

For `N=prod_p p^{gamma_p}`, BBMST use digit coordinates

\[
 U=\{(p,e):1\le e\le\gamma_p\},\qquad |X_{(p,e)}|=p.
\]

A simple frame has one axis support U and, for each coordinate u=(p,e), exactly p−1 supports owned by u, one for each non-axis digit value. Every owned support contains u. In the distinct-moduli subfamily all these supports are distinct, because an arithmetic support determines the exponent of every prime and therefore determines the modulus.

Here is the complete fresh-residue argument. Let C be any proper support subfamily and V=union C.

- If U∈C, properness gives
  `|C|<=sum_{u∈U}(|X_u|-1)=Weight(V)`.
- If U∉C, put J=U\V. Besides U, for each u∈J all p_u−1 supports owned by u are absent. These groups are disjoint, so

\[
 |C|\le 1+\sum_{u\in U}(p_u-1)-
          \left(1+\sum_{u\in J}(p_u-1)\right)
      =\sum_{u\in V}(p_u-1).
\]

If arbitrary new values on C covered the digit box, pass to an inclusion-minimal subcover D. Its supports remain a proper subfamily and are distinct. Geometric Simpson gives `|D|>=1+Weight(union D)`, contradicting the preceding inequality. This proof, with dependent coordinate types and minimal-subcover extraction, is the sorry-free Lean theorem F-032; F-033 verifies that the ordered frame actually covers.

An arithmetic support fixes an initial p-digit segment for every p. The base-p/CRT map is a bijection from `Z/NZ` to the digit box, and a residue class modulo d|N pulls back to exactly the hyperplane determined by d's exponent-prefix support. Therefore a fresh residue cover by a proper modulus subset would produce precisely the forbidden fresh-value support cover. F-011 proves this prefix/CRT equivalence and F-040 proves the full prompt-level prime-power frame transport. Hence every distinct arithmetic simple-frame modulus set counted below is strongly irreducible.

## 3. Lower family and multiplicity

BBMST Proposition 5.1 and its proof in Section 5 construct

\[
 L(n)=\exp((c+o(1))f(n))
\]

arithmetic simple-frame minimal systems on their dense sequence `n=n(x)`.
The exact additional restriction needed here is explicitly recorded
immediately after their Theorem 1.1 (p. 3):

> “we will prove the lower bound under the additional restriction that the
> moduli are distinct”.

Section 5 also states that Proposition 5.1 counts only systems corresponding
to arithmetic simple frames. One can see directly that imposing distinct
supports does not change its exponent. For a layer `(p,e)`, let `D_{p,e}` be
the number of available arithmetic predecessor supports. In the notation of
their proof,

\[
 \log D_{p,e}=\sum_{(q,f)<(p,e),\ q\ne p}\log\frac{f+1}{f}
  =(\tau+o(1))\frac{y_{p,e}}{\log y_{p,e}}.
\]

Thus `D_{p,e}/p→∞` as `y_{p,e}→∞`. Instead of making `p-1` independent
choices, choose an injection of the `p-1` owner values into these supports.
For all but finitely many layers `D_{p,e}≥2(p-1)`, and

\[
 (D_{p,e})_{p-1}\ge(D_{p,e}/2)^{p-1}.
\]

Here are all details of the exceptional cases and the loss. First,
`D_{p,e}≥p-1` for every layer. For `p=2` this is trivial. For `p≥3`, the binary
coordinates `(2,f)`, `1≤f≤p-2`, all precede `(p,e)`, because

\[
 \log(1+1/e)\le\log2
 <(p-1)\log(1+1/(p-2))
 \le(p-1)\log(1+1/f).
\]

The strict middle inequality follows from Bernoulli:
`(1+1/(p-2))^(p-1)>2`. The `p-1` possible initial lengths of this binary
prefix already give `p-1` supports. Thus each of the finitely many layers
below a fixed large `y_0` can be assigned one fixed injection.

For `y_{p,e}≥y_0`, take `y_0` so large that `D_{p,e}≥2(p-1)+2`. Then

\[
 \log (D_{p,e})_{p-1}
 \ge(p-1)(\log D_{p,e}-\log2).
\]

Summing the losses `(p-1)log 2` gives at most `(n(x)-1)log2`. The finitely many
fixed early layers discard only a constant contribution to `Q`. The only
owned support that can equal the full axis is a support of the last owner;
for that owner use the same estimate with one support forbidden,
`(D-1)_{p-1}≥(D/2)^{p-1}`. Supports with different owners are automatically
distinct, since a later support contains its owner while every earlier
support is contained in the earlier-coordinate initial segment.

Consequently, if `L_x` is the number of these distinct-support systems, then

\[
 Q(x)-O(n(x))-O(1)\le\log L_x\le Q(x).
\]

Since (20)--(21) give `Q(x)=Theta(x^3/(log x)^2)` and
`n(x)=Theta(x^2/log x)`, the loss is `o(Q(x))`. Hence the Section 5 count still
has exponent `Q-o(Q)` after requiring all supports, and therefore all moduli,
to be distinct. This also independently
explains the paper's explicit distinct-modulus assertion. By Section 2 above,
all modulus sets in this lower subfamily are strong irreducible sets.

Several displayed systems can have one modulus set because their shifts may
differ. Sort the `k` distinct moduli canonically. BBMST Lemma 6.2 says that for
any prescribed ordered moduli `d_1,...,d_k`, at most `(k!)^2` minimal systems
use them. Therefore the number of different strong modulus sets represented
by the lower family is at least

\[
 \frac{L(k)}{(k!)^2}.
\]

Stirling gives `2 log(k!)=O(k log k)=o(f(k))`; explicitly,
`k log k / f(k)=(log k)^{3/2}/sqrt(k)→0`. Thus division leaves the leading constant c unchanged.

## 4. Every intermediate size

BBMST first have sizes n(x) and prove that, if x is maximal with n(x)≤k, then
`t=k-n(x)<x=o(n(x))`. No new frame argument is needed: apply the delta map

\[
\delta(S)=\{2\}\cup\{2n:n\in S\}
\]

t times. F-027 proves in Lean that delta preserves the prompt's strong
irreducibility (including fresh residues), and F-031 proves that it is
injective on admissible sets and induces `I(j)≤I(j+1)`. Iteration therefore
injects every size-n(x) lower-family modulus set into a distinct size-k set.

Finally `t=o(n)` implies `n(x)/k→1`, and direct substitution gives `f(n(x))/f(k)→1`. Hence

\[
 I(k)\ge\exp((c+o(1))f(k)).
\]

Combining with Section 1 proves

\[
\boxed{I(k)=\exp\!\left(\left(\frac{4\sqrt\tau}{3}+o(1)\right)
\frac{k^{3/2}}{\sqrt{\log k}}\right).}
\]
