PeelingResult
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not assert existence of a PeelingResult for every U.
- Does not encode the selection rule that chooses the next constraint.
- Does not relate the peeling order to any cost function or complexity bound.
- Does not treat the empty-U case beyond the trivial empty lists.
formal statement (Lean)
137structure PeelingResult {n : Nat} (inputs : InputSet n) (aRef : Assignment n)
138 (φ : CNF n) (H : XORSystem n) (U : Finset (Var n)) where
139 vars : List (Var n)
140 constrs : List (Constraint n)
141 len_eq : vars.length = constrs.length
142 nodup : vars.Nodup
143 cover : ∀ v, v ∈ vars ↔ v ∈ U
144 step : ∀ k (hk : k < vars.length),
145 let v := vars.get ⟨k, hk⟩
proof body
Definition body.
146 let K := constrs.get ⟨k, by omega⟩
147 mentionsVar K v = true ∧
148 (∀ w ∈ vars.drop k.succ, mentionsVar K w = false) ∧
149 determinesVar aRef K v
150
151/-- **PROVED**: Build the peeling order via Finset induction.
152 At each step, PC gives constraint K and variable v ∈ U that K uniquely determines.
153 Recursively peel U \ {v} to get (vs, cs), then return (v :: vs, K :: cs). -/