`peeling_implies_arborescence`

proved

show as: view math explainer →

module: IndisputableMonolith.Complexity.SAT.PC
domain: Complexity
line: 245 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Complexity.SAT.PC on GitHub at line 245.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 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. -/
 260theorem peeling_iff_arborescence {n}
 261  (inputs : InputSet n) (aRef : Assignment n) (φ : CNF n) (H : XORSystem n) :
 262  PeelingWitness inputs aRef φ H ↔ ForcedArborescence inputs aRef φ H := by
 263  unfold ForcedArborescence
 264  exact Iff.rfl
 265
 266/-- PC ⇒ ForcedArborescence. -/
 267theorem pc_implies_forcedArborescence {n}
 268  (inputs : InputSet n) (aRef : Assignment n) (φ : CNF n) (H : XORSystem n) :
 269  PC inputs aRef φ H → ForcedArborescence inputs aRef φ H := by
 270  unfold ForcedArborescence
 271  exact pc_implies_peeling inputs aRef φ H
 272
 273end SAT
 274end Complexity
 275end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.