theorem
proved
peeling_implies_arborescence
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Complexity.SAT.PC on GitHub at line 245.
browse module
All declarations in this module, on Recognition.
explainer page
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