Weighted independent sets in clique-free graphs
A Lean formalization of a weighted independent-set existence bound for finite clique-free graphs. For every integer r at least four, positive real degree weights s, and nonnegative real objective weights a, a K_r-free graph has an independent set whose a-weight is at least c_r times the sum of a_v f(s(N(v))/s_v), where f is Shearer's function. The coefficient is the explicit positive rational c_r = 1/(1 + 1152 B_0 r), with a fixed absolute constant B_0, and has proved upper and lower bounds of order 1/r. The proof combines scalar potentials, a weighted triangle dichotomy, sparse neighborhood…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-11-02-000002
curl -X POST /api/v1/records/palomar/PALOMAR-2026-11-02-000002/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-11-02-000002/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'