programGoal_pc_iff_arborescence
plain-language theorem explainer
The declaration equates the propagation-completeness condition on a mixed CNF-XOR system to the existence of a forced-implication arborescence over the input variables. Researchers studying constraint propagation or SAT encodings would cite it when reducing local determination properties to global reachability structures. It is introduced as a direct biconditional definition between the two predicates.
Claim. Let $PC$ be the predicate that for every nonempty $U$subseteq inputs there exists a constraint $K$ mentioning exactly one $v$ in $U$ such that $K$ determines $v$ under reference assignment $aRef$. Let $ForcedArborescence$ be the predicate that a peeling witness exists (a spanning order of variables with matching determining constraints). Then $PC(inputs, aRef, phi, H) iff ForcedArborescence(inputs, aRef, phi, H)$.
background
The module defines constraints as CNF clauses or XOR checks. InputSet is the finset of designated input variables. PC requires that every nonempty subset U of inputs admits a constraint K mentioning precisely one variable v from U that determines v relative to aRef. ForcedArborescence is defined identically to PeelingWitness, which supplies an ordered list of variables together with their determining constraints.
proof idea
This is a one-line wrapper that directly equates the PC predicate to the ForcedArborescence predicate via a biconditional.
why it matters
This definition states the program goal of the PC module: to establish that propagation-completeness is equivalent to the existence of a forced-implication arborescence. It prepares the reduction of the local PC condition to a graph-theoretic spanning structure witnessed by peeling, aligning with the Recognition Science aim of expressing complexity properties via algebraic or geometric forms. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.