{"id":"palomar/PALOMAR-2026-09-19-000003","url":"https://github.com/scottnarmstrong/BKARForestFormula/tree/a07f44a534240fe6339558951dd78a19e4ef7c51","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-19-000003-v1.json","repo":"https://github.com/scottnarmstrong/BKARForestFormula","tags":["math-ph","math.PR","msc:82B05","msc:81T15","msc:05C05","statistical-mechanics","probability","lean","graph-theory"],"score":0,"title":"BKARForestFormula","trust":"high","domain":"math-ph","source":"palomar","authors":["Scott Armstrong"],"reviews":0,"subject":"math-ph","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-19","reactions":{},"formalized":true,"formalizes":[{"title":"Mayer expansions and the Hamilton-Jacobi equation","identifier":"doi:10.1007/BF01010398","relationship":"adapts"}]}