programGoal_pc_iff_arborescence
The declaration defines the program goal as the biconditional between the propagation-completeness predicate PC and the forced-implication arborescence predicate for a fixed input set, reference assignment, CNF formula, and XOR system. Researchers formalizing SAT encodings or graph reductions in complexity would cite this equivalence when moving from local constraint determination to global reachability structure. It is introduced as a direct one-line biconditional definition with no additional proof steps.
claimLet $I$ be a finite set of input variables, $a$ a reference Boolean assignment, $C$ a CNF formula, and $H$ an XOR system over the same variables. The propagation-completeness condition holds if and only if a forced-implication arborescence exists: $PC(I,a,C,H)leftrightarrow ForcedArborescence(I,a,C,H)$.
background
The module treats constraints as either CNF clauses or XOR checks. InputSet is the finite set of designated input variables. The PC predicate states that every nonempty subset $U$ of inputs admits a constraint $K$ mentioning exactly one variable $v$ in $U$ that $K$ determines under the reference assignment. ForcedArborescence is defined to be identical to PeelingWitness, the data of a duplicate-free spanning list of inputs together with their determining constraints.
proof idea
One-line definition that directly equates the PC predicate to the ForcedArborescence predicate by biconditional.
why it matters in Recognition Science
This definition names the central target equivalence of the PC development, connecting the local propagation condition to an arborescence of determining constraints. It prepares the statement whose proof would link constraint systems to graph-theoretic reachability, consistent with the module's focus on CNF and XOR constraints. No downstream uses appear yet, marking it as the open goal statement.
scope and limits
- Does not prove the equivalence; only declares the target proposition.
- Does not construct or enumerate the arborescence beyond the peeling-witness identification.
- Does not restrict the form of constraints beyond CNF clauses and XOR checks.
- Does not address decidability or complexity of verifying the arborescence.
formal statement (Lean)
117def programGoal_pc_iff_arborescence {n}
118 (inputs : InputSet n) (aRef : Assignment n) (φ : CNF n) (H : XORSystem n) : Prop :=
proof body
Definition body.
119 (PC inputs aRef φ H) ↔ (ForcedArborescence inputs aRef φ H)
120
121/-- Helper to extract one (K, v) pair from PC condition. -/