catskillsresearch/cardb
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-08-20-000003
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-20-000003/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-20-000003/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'