PC
plain-language theorem explainer
PC encodes the propagation-completeness property for SAT instances that combine CNF clauses with XOR constraints. Researchers proving backpropagation success from uniqueness in the Recognition Science complexity module cite this definition. It directly states a universal quantification over nonempty input subsets together with an existential witness for an isolating, determining constraint.
Claim. Let $I$ be a finset of input variables, $a$ a reference assignment, $φ$ a CNF formula, and $H$ an XOR system over $n$ variables. The predicate PC$(I,a,φ,H)$ holds if and only if for every nonempty $U ⊆ I$ there exists a constraint $K$ drawn from the combined list of CNF clauses and XOR checks together with a variable $v ∈ U$ such that $K$ mentions $v$, mentions no other element of $U$, and determines the Boolean value of $v$ under $a$.
background
InputSet n is defined as Finset (Var n) where Var n = Fin n. Assignment n maps each variable to Bool. CNF n packages a list of clauses. XORSystem n supplies the XOR constraints. The helper constraintsOf φ H concatenates the mapped CNF clauses with the XOR checks into a single list of Constraint n objects. The module states that constraints are either CNF-clauses or XOR-checks.
proof idea
This is a definition whose body is the direct statement of the universal property. No lemmas are applied; the quantifiers and the three conditions on K and v are written out explicitly.
why it matters
PC is invoked by backprop_succeeds_from_PC to obtain BackpropSucceeds from UniqueSolutionXOR. It is also used by buildPeelingResult to construct a peeling order by repeated extraction of a determining constraint. The definition supplies the missing link between unique solutions and forced implication in the SAT completeness development. It touches the open question of relating abstract step semantics to concrete forcing chains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.