peeling_iff_arborescence
The equivalence asserts that a peeling witness for given inputs, reference assignment, CNF formula and XOR system is identical to the existence of a forced arborescence of locally determining constraints. Workers on propagation-complete SAT encodings cite it when switching between ordered peeling sequences and arborescence reachability. The proof is a one-line term that unfolds the arborescence definition and applies reflexivity of logical equivalence.
claimFor any natural number $n$, finite input set $I$, reference assignment $a$, CNF formula over $n$ variables, and XOR system, the existence of a peeling structure on these data is equivalent to the existence of a directed arborescence of locally determining constraints that reaches every input variable from the output.
background
The module treats constraints as either CNF clauses or XOR checks. An InputSet is the finite collection of input variables used to state the propagation-completeness condition: for every nonempty subset $U$ of inputs there must exist a constraint that mentions exactly one variable from $U$ and determines its value under the reference assignment. A PeelingWitness is the proposition that a nonempty PeelingData exists, where PeelingData encodes an ordered list of variables together with their determining constraints. ForcedArborescence is introduced as the abstract reachability notion of a directed arborescence of such locally determining constraints; the module defines it directly by the PeelingWitness predicate.
proof idea
The proof is a one-line term wrapper. It unfolds the definition of ForcedArborescence, which expands exactly to PeelingWitness, then applies Iff.rfl to obtain the identity equivalence.
why it matters in Recognition Science
This equivalence closes the definitional identification between the concrete peeling witness and the abstract arborescence inside the propagation-completeness development. It supplies the bridge required for any later reasoning that treats forced implications as tree-structured reachability. No downstream theorems are recorded yet, so it remains open whether the arborescence formulation will be used to derive complexity bounds or to interface with the larger Recognition Science encoding pipeline.
scope and limits
- Does not prove existence of a peeling structure for any concrete inputs.
- Does not relate the equivalence to the shifted cost function from the algebra module.
- Does not address satisfiability or derive complexity bounds.
- Does not extend to infinite variable sets or non-Boolean domains.
formal statement (Lean)
260theorem peeling_iff_arborescence {n}
261 (inputs : InputSet n) (aRef : Assignment n) (φ : CNF n) (H : XORSystem n) :
262 PeelingWitness inputs aRef φ H ↔ ForcedArborescence inputs aRef φ H := by
proof body
Term-mode proof.
263 unfold ForcedArborescence
264 exact Iff.rfl
265
266/-- PC ⇒ ForcedArborescence. -/