ForcedArborescenceWitness
plain-language theorem explainer
ForcedArborescenceWitness equates the forced arborescence witness for a propagation-complete SAT instance to the peeling witness data. Complexity researchers studying graph reductions of SAT would cite this when linking arborescences to constraint propagation. The definition is a direct one-line abbreviation that reuses the peeling witness proposition for the same inputs, reference assignment, CNF, and XOR system.
Claim. Let $I$ be a finset of input variables, $a$ a reference assignment, $C$ a CNF formula, and $H$ an XOR system. The forced arborescence witness is the proposition that a peeling witness exists for $I$, $a$, $C$, and $H$, where the peeling witness is a spanning duplicate-free list of variables with matching constraints.
background
In the SAT.PC module constraints are CNF clauses or XOR checks. InputSet is the finset of input variables used to state the propagation-completeness condition: for every nonempty $U$ subset of inputs there exists a constraint $K$ and $v$ in $U$ such that $K$ mentions only $v$ from $U$ and determines $v$ under the reference assignment. The PeelingWitness encodes a spanning duplicate-free list of variables together with their matching constraints. Upstream results supply the Assignment type (Boolean functions on variables) from both CNF and RSatEncoding modules, the CNF structure itself, and the H cost function from CostAlgebra that satisfies the shifted RCL identity.
proof idea
The definition is a one-line wrapper that directly reuses the PeelingWitness proposition on the identical parameters. No lemmas are invoked and no tactics are applied beyond the abbreviation.
why it matters
This declaration supplies the witness data for the program goal of showing PC equivalent to existence of a forced-implication arborescence. It identifies the arborescence side with the peeling witness inside the PC module. In the Recognition Science setting it contributes to the complexity analysis of SAT encodings that may later connect to algebraic structures such as the H cost function, though the immediate context remains the PC condition. No downstream theorems are recorded yet, leaving the full equivalence open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.