{"id":"palomar/PALOMAR-2026-08-20-000003","url":"https://github.com/catskillsresearch/cardb/tree/d8c1d63052a18db0c43d44c1c77fb10ca8902ed0","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-20-000003-v1.json","repo":"https://github.com/catskillsresearch/cardb","tags":["math.GN","math.CO","msc:54A05","msc:05A15","msc:54A10","general-topology","enumeration","lean-formalization"],"score":0,"title":"catskillsresearch/cardb","trust":"high","domain":"math.GN","source":"palomar","authors":["Lars Warren Ericson"],"reviews":0,"subject":"math.GN","summary":"A Lean formalization of an exact enumeration identity and two consequences: for a finite type α, the number of families B ⊆ Set α that are topological bases equals the sum, over all topologies τ on α, of 2^(|τ| − |M_τ|), where M_τ is the canonical minimal basis of minimal open neighbourhoods (Mathlib's nhdsKer {x} at each point). Kernel-reducible enumeration gives the exact table #(0)=2, #(1)=2, #(2)=10, #(3)=142. A quantitative sandwich then shows that the discrete fiber 2^(2^N − N) dominates: for N ≥ 2 the remaining fibers contribute at most 2^(N(N−1) + 3·2^(N−2)), the ratio to the…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-20","reactions":{},"formalized":true}