PC
plain-language theorem explainer
The propagation-completeness condition requires that every nonempty subset of input variables admits a constraint mentioning exactly one variable from the subset and fixing its value under the reference assignment. Researchers proving completeness of backpropagation in hybrid CNF-XOR solvers cite this property when uniqueness of solutions is already established. The definition is a direct universal quantification over input subsets with no auxiliary lemmas or tactics.
Claim. Let $I$ be a finite set of input variables, $a$ a reference boolean assignment, $C$ a CNF formula, and $X$ an XOR system over the same variables. The condition holds when for every nonempty $Usubseteq I$ there exists a constraint $K$ drawn from the clauses of $C$ together with the equations of $X$, and a variable $v in U$, such that $K$ mentions $v$ but no other member of $U$ and $K$ fixes the value of $v$ under $a$.
background
Constraints in the module are formed either as CNF clauses or as XOR parity checks. InputSet n is the finite collection of designated input variables expressed as a Finset. Assignment n is a total function from variables to boolean values that serves as the reference solution. CNF n packages a list of clauses while XORSystem n supplies the parity constraints; constraintsOf concatenates the two families into a single list.
proof idea
The definition is a direct encoding of the stated universal property. It expands the forall over nonempty subsets U of inputs, asserts membership of K in the collected constraint list, isolates a unique v inside U via the mentionsVar predicate, and requires that determinesVar holds for the reference assignment. No lemmas are applied; the body is the literal formalization of the doc-comment.
why it matters
The definition supplies the hypothesis for backprop_succeeds_from_PC, which concludes that backpropagation succeeds once uniqueness of the XOR solution is given. It is also the key assumption in the inductive construction of peeling results inside buildPeelingResult and in the definition of ForcedArborescenceWitness. Within the Recognition framework the property articulates a completeness condition that supports inference steps on encoded logical structures and feeds into claims about forced arborescences.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.