On the Number of Distinct Topological Bases of a Finite Set of Size $N$

For a finite set $S$ with $\mid S\mid =N$, the number of families $\mathcal{B}\subseteq \mathcal{P}(S)$ that are topological bases is $\mathrm{\#}(N)={\sum }_{\mathcal{T}\in \mathrm{Top}(S)}{2}^{\mid \mathcal{T}\mid -\mid {\mathcal{M}}_{\mathcal{T}}\mid }$, where ${\mathcal{M}}_{\mathcal{T}}$ is the canonical minimal basis of minimal open neighborhoods. The identity is proved in Lean 4 / Mathlib (CARDB.lean): bases generating $\mathcal{T}$ are exactly the sets with ${\mathcal{M}}_{\mathcal{T}}\subseteq \mathcal{B}\subseteq \mathcal{T}$. The small-$N$ table and the discrete-dominance sandwich are proved in CARDB/SmallN.lean and CARDB/Asymptotics.lean.