pc_implies_peeling

formal source

 226    4. Return (v :: vs, K :: cs)
 227
 228    Base case: empty U gives ([], []). -/
 229theorem pc_implies_peeling {n}
 230  (inputs : InputSet n) (aRef : Assignment n) (φ : CNF n) (H : XORSystem n) :
 231  PC inputs aRef φ H → PeelingWitness inputs aRef φ H := by
 232  intro hPC
 233  let result := buildPeelingResult inputs aRef φ H hPC inputs (fun _ h => h)
 234  exact ⟨{
 235    vars := result.vars
 236    constrs := result.constrs
 237    nodup := result.nodup
 238    len_eq := result.len_eq
 239    cover := fun v => (result.cover v).symm
 240    step := result.step
 241  }⟩
 242
 243/-- Peeling ⇒ forced arborescence (Prop-level).
 244    Trivial since ForcedArborescence is defined as PeelingWitness. -/
 245theorem peeling_implies_arborescence {n}
 246  (inputs : InputSet n) (aRef : Assignment n) (φ : CNF n) (H : XORSystem n) :
 247  PeelingWitness inputs aRef φ H → ForcedArborescence inputs aRef φ H := by
 248  unfold ForcedArborescence
 249  exact id
 250
 251/-- Arborescence ⇒ peeling (Prop-level).
 252    Trivial since ForcedArborescence is defined as PeelingWitness. -/
 253theorem arborescence_implies_peeling {n}
 254  (inputs : InputSet n) (aRef : Assignment n) (φ : CNF n) (H : XORSystem n) :
 255  ForcedArborescence inputs aRef φ H → PeelingWitness inputs aRef φ H := by
 256  unfold ForcedArborescence
 257  exact id
 258
 259/-- Peeling ↔ Arborescence equivalence. -/