extractFromPC
plain-language theorem explainer
extractFromPC selects one constraint-variable pair satisfying the unique-mention and determination properties inside the propagation-completeness condition for any nonempty input subset. Researchers studying SAT propagation completeness and inductive peeling constructions cite this helper when building ordered extraction sequences. The definition applies the PC hypothesis to U and uses two choice steps to package the witness into the dependent subtype.
Claim. Given an input set $I$, reference assignment $a$, CNF formula $φ$, and XOR system $H$ satisfying propagation completeness, for any nonempty $U ⊆ I$ the function returns a pair $(K, v)$ where $K$ belongs to the combined constraint set, $v ∈ U$, $K$ mentions $v$ but no other element of $U$, and $K$ determines the value of $v$ under $a$.
background
Constraints are an inductive type whose constructors are CNF clauses or XOR constraints. InputSet is an abbreviation for the Finset of designated input variables. The PC predicate asserts that every nonempty $U ⊆ I$ admits a constraint $K$ from the system together with $v ∈ U$ such that $K$ mentions only $v$ inside $U$ and determines $v$ relative to the reference assignment.
proof idea
Apply the PC hypothesis to the supplied $U$ to obtain an existential statement, then use choose to select the constraint $K$ and the variable $v$ from the nested witnesses, finally constructing the subtype element with the collected properties.
why it matters
The helper is called inside buildPeelingResult to support Finset induction that assembles the complete peeling sequence of variables and constraints. It thereby enables formal statements about propagation-complete encodings in the SAT complexity layer of the Recognition Science development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.