PeelingResult
plain-language theorem explainer
PeelingResult bundles ordered lists of variables and constraints that realize successive unique determinations under the propagation-completeness condition for a given input set, reference assignment, CNF, and XOR system. Researchers formalizing unit propagation or resolution in mixed SAT encodings cite it when they need an explicit inductive witness. The definition simply packages six invariants (length equality, nodup, exact cover, and per-step mentions-plus-determination) that buildPeelingResult populates by Finset induction.
Claim. Let $n$ be a natural number, $I$ an input set (Finset of variables), $a$ a reference assignment, $C$ a CNF formula, $H$ an XOR system, and $U$ a subset of $I$. A PeelingResult records lists $v$ and $K$ of equal length such that the variables in $v$ are distinct, cover exactly $U$, and for each position $k$ the constraint $K_k$ mentions $v_k$, mentions none of the later variables, and determines $v_k$ under $a$.
background
Constraints are defined as either CNF clauses or XOR checks. InputSet is the Finset of input variables for which the PC property is stated. The PC condition (from the InputSet doc-comment) asserts that every nonempty subset of inputs admits a constraint mentioning exactly one variable from the subset and determining that variable relative to the reference assignment. Upstream, Assignment is a total map from variables to Bool (both the CNF and RSatEncoding versions), CNF is a list of clauses, and Var is Fin n.
proof idea
This is a structure definition whose six fields directly encode the required invariants of a peeling sequence. No lemmas or tactics are invoked inside the declaration; the inductive construction that supplies concrete data is performed separately by buildPeelingResult via Finset induction on cardinality.
why it matters
PeelingResult is the return type of buildPeelingResult, the central construction that realizes the PC hypothesis by explicit induction. It supplies the concrete witness needed for any downstream argument that propagation completeness holds for the mixed CNF-XOR systems used in the Recognition Science complexity module. No open questions or scaffolding are closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.