peeling_implies_arborescence
plain-language theorem explainer
The implication from a peeling witness to a forced arborescence holds by definition for input sets in mixed CNF-XOR SAT instances. Analysts of propagation completeness or implication reachability in Boolean satisfiability would cite the equivalence to interchange the two structures. The proof is a one-line term that unfolds ForcedArborescence and applies the identity.
Claim. Let $I$ be a finset of input variables, $a$ a reference assignment, $φ$ a CNF formula, and $H$ an XOR system. If a peeling witness exists for $(I, a, φ, H)$, then a forced arborescence exists for the same inputs.
background
The PC module treats constraints as either CNF clauses or XOR checks. InputSet is a finset of designated input variables. PeelingWitness asserts nonempty PeelingData, which encodes an ordered sequence of variables together with locally determining constraints. ForcedArborescence is defined directly as PeelingWitness, thereby encoding a directed arborescence of determining constraints from outputs back to every input.
proof idea
The proof unfolds the definition of ForcedArborescence (which is literally PeelingWitness) and applies the identity function. No lemmas from CostAlgebra or upstream Assignment definitions are invoked.
why it matters
The declaration closes the definitional identification of peeling structures with arborescence reachability inside the propagation-completeness setting. It permits later arguments to treat the two notions interchangeably when analyzing forced implications. No downstream uses appear yet, but the step supports the abstract reachability description given in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.