CubicPathwidth.Alg.Proofs.E14Exported

Source file CubicPathwidth/Alg/Proofs/E14Exported.lean of the Lean project (how it is built).

import CubicPathwidth.Alg.Spec

/-!
Tasks E1-E4 of Stage 1: the exported forms on the frozen types.

Each exported statement follows from the bridge `ValidPDBridge` (B1) applied to the valid
decomposition given by the matching algorithm statement, together with the graph facts
`OfSimpleGraphSpec` (B2). For T1 the degree bound `IsSubcubic S` is transferred to
`MaxDegLE 3` on `Graph.ofSimpleGraph S`; the other three do not need it.
-/

namespace CubicPathwidth.Alg

open Graph

namespace E14

/-- Common transfer step: a valid decomposition of `Graph.ofSimpleGraph S` gives the
exported width bound for `S`. -/
theorem transfer (hB : ValidPDBridge) (hS : OfSimpleGraphSpec) (n : ℕ) (S : SimpleGraph (Fin n))
    [DecidableRel S.Adj] (bags : List Bag) (hbags : ValidPD (Graph.ofSimpleGraph S) bags) :
    HasPathwidthAtMost S (pdWidth bags) := by
  obtain ⟨hwf, hnodes, hback, _⟩ := hS n S
  have key := hB n (Graph.ofSimpleGraph S) bags hwf hnodes hbags
  rw [hback] at key
  exact key

end E14

/-- E1: exported form of the Theorem 1 algorithm. -/
theorem algoT1Exported_of (hB : ValidPDBridge) (hS : OfSimpleGraphSpec) (h : AlgoT1Valid) :
    AlgoT1Exported := by
  intro n S inst hsub Y
  obtain ⟨_, _, _, hdeg⟩ := hS n S
  exact E14.transfer hB hS n S _ (h _ (hS n S).1 (hdeg hsub) Y)

/-- E2: exported form of the Theorem 2(a) algorithm. -/
theorem algoT2aExported_of (hB : ValidPDBridge) (hS : OfSimpleGraphSpec) (h : AlgoT2aValid) :
    AlgoT2aExported := by
  intro n S inst Y
  exact E14.transfer hB hS n S _ (h _ (hS n S).1 Y)

/-- E3: exported form of the mixed algorithm. -/
theorem algoMixedExported_of (hB : ValidPDBridge) (hS : OfSimpleGraphSpec) (h : AlgoMixedValid) :
    AlgoMixedExported := by
  intro n S inst lab
  exact E14.transfer hB hS n S _ (h _ (hS n S).1 lab)

/-- E4: exported form of the Theorem 4 algorithm. -/
theorem algoT4Exported_of (hB : ValidPDBridge) (hS : OfSimpleGraphSpec) (h : AlgoT4Valid) :
    AlgoT4Exported := by
  intro n S inst lab
  exact E14.transfer hB hS n S _ (h _ (hS n S).1 lab)

#print axioms algoT1Exported_of
#print axioms algoT2aExported_of
#print axioms algoMixedExported_of
#print axioms algoT4Exported_of
Back to top