ForcedArborescence

formal source

 102    - K_i → v_i for the variable determined by K_i
 103
 104    This forms a directed tree rooted at OUTPUT reaching all input variables. -/
 105def ForcedArborescence {n}
 106  (inputs : InputSet n) (aRef : Assignment n) (φ : CNF n) (H : XORSystem n) : Prop :=
 107  PeelingWitness inputs aRef φ H  -- Arborescence IS the peeling structure
 108
 109/-- Forced arborescence witness: for this development we take it to be the same data
 110    as a peeling witness (a spanning, duplicate-free list of vars with matching constraints). -/
 111abbrev ForcedArborescenceWitness {n}
 112  (inputs : InputSet n) (aRef : Assignment n) (φ : CNF n) (H : XORSystem n) : Prop :=
 113  PeelingWitness inputs aRef φ H
 114
 115/-- Program goal (graph-theoretic equivalence to target):
 116    PC ↔ existence of a forced-implication arborescence (to be proven). -/
 117def programGoal_pc_iff_arborescence {n}
 118  (inputs : InputSet n) (aRef : Assignment n) (φ : CNF n) (H : XORSystem n) : Prop :=
 119  (PC inputs aRef φ H) ↔ (ForcedArborescence inputs aRef φ H)
 120
 121/-- Helper to extract one (K, v) pair from PC condition. -/
 122noncomputable def extractFromPC {n : Nat} (inputs : InputSet n) (aRef : Assignment n)
 123    (φ : CNF n) (H : XORSystem n) (hPC : PC inputs aRef φ H)
 124    (U : Finset (Var n)) (hU : U ⊆ inputs) (hne : U.Nonempty) :
 125    { p : Constraint n × Var n //
 126      p.1 ∈ constraintsOf φ H ∧
 127      p.2 ∈ U ∧
 128      mentionsVar p.1 p.2 = true ∧
 129      (∀ w ∈ U, w ≠ p.2 → mentionsVar p.1 w = false) ∧
 130      determinesVar aRef p.1 p.2 } := by
 131  have h := hPC U hU hne
 132  choose K hK using h
 133  choose v hv using hK.2
 134  exact ⟨(K, v), hK.1, hv.1, hv.2.1, hv.2.2.1, hv.2.2.2⟩
 135