To Flatten a Stone with Six Birds: Critical Pairs, Holonomy, and Confluence in Rewriting Systems

Abstract

Confluence says that the order in which rewrite steps are applied does not matter in the end; flatness says that, locally, transport does not depend on the route taken. This paper makes the analogy precise at the local level and tests it computationally. The natural carrier is not the cycle structure of the reduction graph, and we show by small counterexamples that cycle-based notions of graph flatness neither imply nor are implied by confluence. Instead, we record each branching of two one-step rewrites out of a common state, the configuration tested by local confluence. A branching has trivial elementary holonomy when its two branches can be completed to a common descendant, so that its boundary closes up, and nontrivial holonomy when they cannot. With this definition, elementary flatness is exactly local confluence. Under termination, Newman's lemma turns the local statement into a global one: confluence, elementary flatness, and uniqueness of normal forms coincide. These results hold for arbitrary abstract rewriting systems and are checked in Lean 4 without finiteness assumptions. In string and term rewriting, the branchings that can fail are the rule overlaps recorded by critical pairs; we work with the concrete critical-pair instances that occur in terms reachable from chosen start terms. An exhaustive enumeration of all 66,066 rewriting relations on one to four labeled states agrees with the theorems and yields smallest counterexamples showing that each hypothesis is needed. Curated string and left-linear term-rewriting examples, including an overlap below the root, show reachable critical-pair defects coinciding with the observed obstructions. Finally, two before-and-after examples read a completion step as holonomy elimination: the added rule leaves the branching in place but supplies the missing filler. Code, data, and Lean sources: https://github.com/ioannist/six-birds-confluence