{"id":"palomar/PALOMAR-2026-09-01-000010","url":"https://github.com/Arthur742Ramos/Metatheory/tree/ab553544dafba3172cee2d56cf88ebf3065262b5/palomar","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-01-000010-v1.json","repo":"https://github.com/Arthur742Ramos/Metatheory","tags":["cs.LO","msc:68Q42","rewriting-systems","confluence","lean","proof-certificates"],"score":0,"title":"Proof-Carrying Decreasing-Diagram Confluence Certificates","trust":"high","domain":"cs.LO","source":"palomar","authors":["Arthur Freitas Ramos","David Barros Hulak","Ruy J. G. B. de Queiroz"],"reviews":0,"subject":"cs.LO","summary":"A Lean 4.33.0 formalization of a generic soundness theorem for finite, proof-carrying decreasing-diagram certificates. An artifact lists the labeled rewrite steps and explicit decreasing valleys for every local peak; an executable checker validates the finite data, while a separate completeness proof connects that data to the semantic relation. The theorem assumes `WellFounded lt` for the label order and then derives confluence of the unlabeled relation even though the underlying rewrite relation itself need not terminate. The repository includes a nontrivial funnel regression with three…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-09-01","reactions":{},"formalized":true,"formalizes":[{"title":"Confluence by decreasing diagrams","identifier":"https://doi.org/10.1016/0304-3975(92)00023-K","relationship":"formalizes"}]}