BKARForestFormula
A Lean 4 / Mathlib formalization of the Brydges-Kennedy-Abdesselam-Rivasseau forest interpolation formula: for a finite vertex set V and a C-infinity function rho on the edge-coupling space of the complete graph on V, the value of rho at the all-ones coupling equals the sum, over all acyclic edge subsets (forests) F, of the integral over the unit cube [0,1]^E(F) of the mixed partial derivative of rho in the edge variables of F, evaluated at the path-minimum interpolation point x^F(u); the empty forest contributes rho(0). The flagship theorem is additionally restated Mathlib-only and…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-09-19-000003
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-19-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-09-19-000003/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'