{"id":"palomar/PALOMAR-2026-10-04-000009","url":"https://github.com/thonmay/thesis-lean/tree/c4c2c0fb15adf42b8b584e4fc83d5cbe643d5819","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-04-000009-v2.json","repo":"https://github.com/thonmay/thesis-lean","tags":["cs.DS","math.CO","msc:05C85","msc:68Q25","dynamic-algorithms","graph-algorithms","maximum-cardinality-search","lean-formalization"],"score":0,"title":"Dynamic MCS Ordering Maintenance","trust":"high","domain":"cs.DS","source":"palomar","authors":["Md Thoriqul Islam Thonmay","Gregory Morse"],"reviews":0,"subject":"cs.DS","summary":"A fully-dynamic Maximum-Cardinality-Search (MCS) ordering algorithm that, on a single-edge insertion or deletion into a loop-free undirected graph, scans the affected window between the two endpoints for the first step at which the current ordering's choice stops being a legal MCS pick, and only then regreedies the suffix (probe-then-repair). Correctness - every order produced stays a valid MCS ordering of the updated graph, and in fact equals the from-scratch canonical ordering - is machine-checked in Lean 4 / Mathlib, together with locality (the first position whose choice can change lies…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-10-15","reactions":{},"formalized":true}