extractFromPC
plain-language theorem explainer
extractFromPC selects one constraint-variable pair from the propagation-completeness condition for any nonempty subset of input variables. Researchers formalizing SAT encodings or propagation in complexity would cite it when building inductive peeling orders over variable sets. The definition applies the existential witness supplied by the PC predicate and repackages it as a dependent pair.
Claim. Given an input set $inputs$, reference assignment $aRef$, CNF formula $φ$, XOR system $H$, and the assumption that the system satisfies propagation-completeness, together with nonempty $U ⊆ inputs$, the function returns a pair $(K, v)$ such that $K$ belongs to the constraints of the system, $v ∈ U$, $K$ mentions $v$ but no other element of $U$, and $K$ determines the value of $v$ under $aRef$.
background
InputSet $n$ is the Finset of input variables over which the propagation-completeness condition is stated. The PC predicate requires that every nonempty $U ⊆ inputs$ contains a variable $v$ that is mentioned by exactly one constraint $K$ of the system and whose value is fixed by that constraint relative to the reference assignment. Constraints are defined inductively as either CNF clauses or XOR constraints. The module works with mixed CNF-XOR systems and treats assignments as functions from variables to Bool.
proof idea
The definition applies the PC hypothesis directly to the given $U$, then uses choose twice to extract the constraint $K$ and the variable $v$ from the nested existential quantifiers, finally constructing the dependent pair with the five required properties.
why it matters
The helper feeds the inductive construction in buildPeelingResult, which removes one determined variable at each step to produce a total ordering. It supplies a concrete witness extraction step inside the formalization of propagation-completeness for SAT encodings. The declaration sits in the Complexity domain and does not connect to the core T0-T8 forcing chain or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.