Two application notes of the Erdős #81 series: realizability transfer and exact chordal stability
A Lean 4 / Mathlib formalization of the two research notes of the author's Erdős #81 series, in one package. Note I, "From realizability certificates to the Erdős 81 bound": a realizability certificate of Paper V for an auxiliary conflict system whose target is the physical system of copies of K₃ and K₄ in G (conflict when they share an edge, gain C(|K|,2) − 1), with q ≥ 1 classes and budget q·e(G) + cost ≤ q·T + w(X), gives a clique partition of G into pieces of order at most four with at most T pieces (note_I_partition_of_certificate; no chordality); a physical packing with e(G) − g(P) ≤ T…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-11-01-000022
curl -X POST /api/v1/records/palomar/PALOMAR-2026-11-01-000022/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-01-000022/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'