programGoal_pc_iff_arborescence

formal source

 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
 136/-- Bundled result type for peeling construction. -/
 137structure PeelingResult {n : Nat} (inputs : InputSet n) (aRef : Assignment n)
 138    (φ : CNF n) (H : XORSystem n) (U : Finset (Var n)) where
 139  vars : List (Var n)
 140  constrs : List (Constraint n)
 141  len_eq : vars.length = constrs.length
 142  nodup : vars.Nodup
 143  cover : ∀ v, v ∈ vars ↔ v ∈ U
 144  step : ∀ k (hk : k < vars.length),
 145    let v := vars.get ⟨k, hk⟩
 146    let K := constrs.get ⟨k, by omega⟩
 147    mentionsVar K v = true ∧