ForcedArborescence
plain-language theorem explainer
ForcedArborescence is defined to coincide exactly with PeelingWitness, supplying an abstract graph view of forced reachability from output to inputs via determining constraints. Researchers analyzing propagation completeness in SAT encodings for complexity reductions would cite the equivalence when moving between peeling orders and arborescence trees. The definition is a direct one-line alias with no separate proof obligations.
Claim. Let $I$ be a finset of input variables, $a$ a reference assignment, $C$ a CNF formula, and $H$ an XOR system over $n$ variables. The predicate ForcedArborescence$(I,a,C,H)$ holds if and only if a peeling witness exists, i.e., there is a sequence of variables and locally determining constraints that successively fixes every element of $I$ under $a$.
background
The module treats constraints as either CNF clauses or XOR checks. InputSet $n$ is the finset of designated input variables used to articulate the propagation-completeness condition. PeelingWitness asserts the existence of PeelingData, which packages an ordered list of variables together with the constraints that determine them one by one. Upstream, Assignment (from both CNF and RSatEncoding) supplies the Boolean maps on variables, while the CostAlgebra H supplies the shifted cost function $H(x)=J(x)+1$ used elsewhere in the monolith.
proof idea
The declaration is a one-line wrapper that directly returns PeelingWitness inputs aRef φ H, thereby inheriting the inductive construction of the peeling order already proved in pc_implies_peeling.
why it matters
The definition supplies the graph-theoretic counterpart to the peeling witness, allowing the chain of equivalences peeling_iff_arborescence, arborescence_implies_peeling and pc_implies_forcedArborescence. It therefore sits inside the PC development that links local constraint determination to global forced reachability, a step required for the complexity encodings that feed into the larger Recognition Science monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.