{"id":"palomar/PALOMAR-2026-09-14-000009","url":"https://github.com/williamjblair/inflation-termination/tree/898300ebc92a15d89adc1e16d084081a0f78fca5","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-14-000009-v2.json","repo":"https://github.com/williamjblair/inflation-termination","tags":["quant-ph","math.ST","msc:81P13","msc:62A09","msc:68Q17","msc:60E15","msc:05C90","causal-inference","lean","quantum-networks"],"score":0,"title":"Termination of the classical inflation hierarchy on pair-source networks","trust":"high","domain":"quant-ph","source":"palomar","authors":["William Blair"],"reviews":0,"subject":"quant-ph","summary":"Machine-checked Lean 4 proofs of two theorems about the classical inflation hierarchy. The headline theorem, TriangleInflation.Graph.classification_NW, classifies the scenarios on which the hierarchy terminates: for a pair-source scenario with binary observations, some finite Navascués–Wolfe order characterizes compatibility iff every connected component is a double-star, and then order two suffices. A pair-source scenario is a finite simple graph without isolated vertices, one binary observed variable per vertex and one independent latent source per edge; a double-star is a tree of diameter…","category":"research","comments":0,"disputed":false,"division":"physics","mentions":0,"verified":true,"discussed":0,"published":"2026-09-17","reactions":{},"formalized":true,"formalizes":[{"title":"Inflation for Classical Pair-Source Networks: Termination and Quantitative Obstructions","identifier":"paper/main.pdf (this repository; not yet posted to arXiv)","relationship":"formalizes"}]}