pc_implies_peeling
plain-language theorem explainer
Propagation-completeness for inputs under a reference assignment implies existence of a peeling witness ordering variables by locally determining constraints drawn from CNF clauses or XOR checks. Researchers analyzing constraint propagation in SAT encodings would cite the implication when reducing global consistency to local determination steps. The proof is a term-mode wrapper that calls the inductive builder on the full input set and repackages the output structure directly into the witness.
Claim. Let $I$ be a finite set of input variables, $a$ a reference Boolean assignment, $F$ a CNF formula, and $H$ an XOR system. If for every nonempty $Usubseteq I$ there exists a constraint $K$ and $v in U$ such that $K$ mentions $v$, mentions no other element of $U$, and determines the value of $v$ under $a$, then a peeling witness exists for $I$, $a$, $F$, and $H$.
background
InputSet denotes the finite collection of designated input variables. The PC condition states that every nonempty subset $U$ of inputs admits a constraint $K$ (from the CNF or XOR system) that isolates exactly one variable $v in U$ and fixes its value relative to the reference assignment. PeelingWitness is the proposition that a PeelingData structure exists, consisting of an ordered list of variables together with their determining constraints and auxiliary well-formedness fields such as nodup and cover.
proof idea
The term proof introduces the PC hypothesis, invokes buildPeelingResult on the full input set with the trivial subset proof, and constructs the witness by extracting vars, constrs, nodup, len_eq, cover (with symmetry adjustment), and step from the returned PeelingResult.
why it matters
The result supplies the missing direction from PC to PeelingWitness, which the downstream theorem pc_implies_forcedArborescence immediately identifies with ForcedArborescence. It therefore closes the local-to-global determination step inside the SAT encoding layer of the monolith, supporting the broader claim that propagation-complete constraint systems admit an arborescence of forced implications.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.