buildPeelingResult
plain-language theorem explainer
The definition constructs an explicit peeling witness for any subset U of the input variables by inducting on the cardinality of U under the propagation-completeness hypothesis. Researchers analyzing SAT encodings or constraint propagation in complexity reductions would invoke this to obtain a concrete linear order of variable determination from the PC property. The construction proceeds by classical Finset induction: extractFromPC supplies a uniquely determining constraint at each nonempty step, the set is reduced by erasure, and the lists are
Claim. Let $n$ be a natural number, $I$ an input set of variables, $a$ a reference assignment, $φ$ a CNF formula, and $H$ an XOR system. Suppose the propagation-completeness condition holds: for every nonempty $U ⊆ I$ there exists a constraint $K$ mentioning exactly one variable $v ∈ U$ that $K$ determines under $a$. For any $U ⊆ I$, the function returns a structure whose variable list and constraint list have equal length, are duplicate-free, cover exactly $U$, and satisfy the step property that each constraint mentions only its paired variable from the remaining set and determines it.
background
In this module constraints are CNF clauses or XOR checks. The input set is a Finset of variables. The PC condition requires that every nonempty subset $U$ of the inputs admits a constraint mentioning exactly one variable $v$ from $U$ and determining the value of $v$ with respect to the reference assignment. The PeelingResult structure packages a list of such variables, the corresponding list of constraints, and proofs that the lists match in length, the variables are distinct and exhaust $U$, and each constraint satisfies the unique-mention and determination properties at its position in the order.
proof idea
The definition is by induction on the cardinality of $U$. The base case (cardinality zero) returns empty lists with the trivial nodup, cover, and step proofs. In the inductive step extractFromPC produces a constraint $K$ and variable $v$ for the current nonempty $U$; the set is reduced by erasing $v$, the induction hypothesis is applied to the smaller set, and the new lists are formed by prepending $v$ and $K$. The nodup, cover, and step properties are verified by direct list reasoning and case analysis on the index.
why it matters
This supplies the constructive content for the theorem pc_implies_peeling, which states that the propagation-completeness condition implies the existence of a PeelingWitness. Within the Recognition Science framework the construction supplies an explicit determination order inside SAT encodings of physical constraint systems, linking the abstract PC property to the broader complexity analysis in the SAT module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.