arborescence_implies_peeling
plain-language theorem explainer
Arborescence implies peeling witness holds for any input set, reference assignment, CNF formula and XOR system. Researchers modeling propagation completeness in mixed CNF-XOR encodings would cite this when establishing structural equivalence between reachability and peeling orders. The proof is a one-line term that unfolds the definition of ForcedArborescence and applies the identity.
Claim. For any natural number $n$, input set $I$, reference assignment $a$, CNF formula $φ$, and XOR system $H$, if a directed arborescence of locally determining constraints reaches every variable in $I$ from the output, then a nonempty peeling data structure exists for the same $I$, $a$, $φ$ and $H$.
background
The module treats constraints as either CNF clauses or XOR checks. An InputSet is a Finset of variables. PeelingWitness asserts Nonempty PeelingData, which encodes a duplicate-free peeling order together with determining constraints. ForcedArborescence is defined verbatim as PeelingWitness, so the two predicates coincide at the Prop level.
proof idea
The term proof unfolds ForcedArborescence to expose the equality with PeelingWitness, then applies the identity function.
why it matters
The declaration supplies one direction of the Peeling ↔ Arborescence equivalence stated in the module comment. It supports abstract modeling of forced-implication reachability inside propagation-completeness arguments, consistent with the framework's use of arborescence structures to capture local determination. No downstream theorems yet reference it, leaving open its integration into larger SAT or complexity results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.