CubicPathwidth.Alg.Plan2

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

import CubicPathwidth.Alg.Spec2

/-!
# Plan interfaces for Stage 2 (NOT part of the approval surface)

Statements used to split the Stage 2 proofs into bounded tasks. They may
be revised during proof work without renewed approval, provided `Spec2.lean` is
unchanged.
-/

noncomputable section

namespace CubicPathwidth.Alg

open Graph

/-! ## 6.1 Layout internals -/

/-- Exact bags of the plain sweep: bag `i` is `order[i]` plus the vertices among the
first `i` that have a neighbour outside them. -/
def PlainLayoutBags : Prop :=
  ∀ G : Graph, G.WF → ∀ Y : Labels,
    (plainLayout G Y).length = G.numNodes ∧
    ∀ i, i < G.numNodes → ∀ v,
      v ∈ (plainLayout G Y).getD i [] ↔
        v = (plainOrder G Y).getD i 0 ∨
          (v ∈ (plainOrder G Y).take i ∧ ∃ x ∈ G.nbrs v, x ∉ (plainOrder G Y).take i)

/-- The components of `Graph.components` are connected (Stage 1 only proved that
they partition the nodes into closed parts). -/
def ComponentsConnected : Prop :=
  ∀ G : Graph, G.WF → ∀ c ∈ G.components, ∀ x ∈ c, ∀ y ∈ c,
    Relation.ReflTransGen G.Adj x y

/-! ## 6.2 Reductions, emptiability, Claims 9 and 10 -/

/-- Records only depend on the graph up to `SameGraph`. -/
def OpsRecordCongr : Prop :=
  ∀ (F F' R : Graph) (ops : List Op), F.WF → F'.WF → SameGraph F F' →
    OpsRecord F ops R → OpsRecord F' ops R

/-- Records compose. -/
def OpsRecordAppend : Prop :=
  ∀ (F M R : Graph) (ops₁ ops₂ : List Op), F.WF → M.WF →
    OpsRecord F ops₁ M → OpsRecord M ops₂ R → OpsRecord F (ops₁ ++ ops₂) R

/-- Only reductions, no deletions. -/
def RedOnly (ops : List Op) : Prop := ∀ o ∈ ops, ∃ v nb, o = Op.red v nb

/-- Some sequence of reductions removes every vertex (treewidth at most 2). -/
def Emptiable (G : Graph) : Prop := ∃ ops, RedOnly ops ∧ OpsRecord G ops Graph.empty

/-- A legal record restricted to a subgraph: if `G'` is a subgraph of `G` (nodes and
edges) avoiding the deleted vertices, then the reductions of `G` that hit `G'`,
replayed on `G'`, form a legal record ending in a subgraph of the final graph of `G`.
(Without the hypothesis on deletions the statement is false: `G = G' = K₄`,
`ops = [.del 0]`; revised 2026-10-09.) -/
def RecordMono : Prop :=
  ∀ (G G' R : Graph) (ops : List Op), G.WF → G'.WF →
    (∀ v ∈ G'.nodes, v ∈ G.nodes) → (∀ u v, G'.Adj u v → G.Adj u v) →
    (∀ w, Op.del w ∈ ops → w ∉ G'.nodes) →
    OpsRecord G ops R →
    ∃ ops' R', RedOnly ops' ∧ OpsRecord G' ops' R' ∧
      (∀ v ∈ R'.nodes, v ∈ R.nodes) ∧ (∀ u v, R'.Adj u v → R.Adj u v) ∧
      (∀ v ∈ R'.nodes, v ∈ G'.nodes)

/-- Confluence (first part of Claim A.29 (`cl:alg-elim`)): if some sequence of reductions empties
`G`, then so does `reduce_record`. -/
def ReduceConfluent : Prop :=
  ∀ G : Graph, G.WF → Emptiable G → (reduceRecord G).1.numNodes = 0

/-- Claim A.29 (`cl:alg-elim`) and Claim A.30 (`cl:alg-balanced`) in the form `pd_tw2` uses: some elimination
bag of `reduce_record` is a balanced separator. -/
def BalancedElimBag : Prop :=
  ∀ H : Graph, H.WF → 1 ≤ H.numNodes → (reduceRecord H.copy).1.numNodes = 0 →
    ∃ X ∈ elimBags (reduceRecord H.copy).2,
      ∀ c ∈ (H.induced fun v => !X.contains v).components, 2 * c.length ≤ H.numNodes

/-- Invariant (I2) of Lemma 4.5 (`lem:reduction`) for a legal record: every component `C` of
`(F - D) - V(R)` attaches to an empty set, a vertex of `R`, or an edge of `R`, and
`F[C]` can be emptied by reductions. -/
def AttachInvariant : Prop :=
  ∀ (F R : Graph) (ops : List Op), F.WF → R.WF → OpsRecord F ops R →
    ∀ C ∈ (F.induced fun v => !(deletedSet ops).contains v && !R.mem v).components,
      (∀ x ∈ undoAttach F (deletedSet ops) C, x ∈ R.nodes) ∧
      (undoAttach F (deletedSet ops) C).length ≤ 2 ∧
      (∀ a b, undoAttach F (deletedSet ops) C = [a, b] → R.Adj a b) ∧
      Emptiable (F.induced C.contains)

/-- Simulation in the torso world of `T4/ProcessDefs.lean`: a legal record from `F`
(nodes below `n`) to `R` is a `Reach` from the state "every non-node deleted" to the
state (non-deleted vertices, `V(R)`), and the torso of that state is `R`. This gives
access to `T4.Good.attachment_card_le`, `T4.torsoDynamics`, `T4.tdeg_erase_le`. -/
def TorsoSim : Prop :=
  ∀ (n : ℕ) (F R : Graph) (ops : List Op), F.WF → (∀ v ∈ F.nodes, v < n) →
    OpsRecord F ops R →
    let S := F.toSimpleGraph n
    let V0 : Finset (Fin n) := Finset.univ.filter fun x => x.val ∈ F.nodes
    let F1 : Finset (Fin n) := V0.filter fun x => x.val ∉ deletedSet ops
    let B1 : Finset (Fin n) := Finset.univ.filter fun x => x.val ∈ R.nodes
    T4.Good S V0 V0 ∧ T4.Reach S (V0, V0) (F1, B1) ∧
      ∀ x y : Fin n, (T4.tgraph S F1 B1).Adj x y ↔ R.Adj x.val y.val

/-! ## 6.3 Relabelling and labels -/

/-- `S` on `Fin m` is `G` with its nodes renamed by the injection `e`. -/
def IsRelabel (G : Graph) {m : ℕ} (S : SimpleGraph (Fin m)) (e : Fin m → Nat) : Prop :=
  Function.Injective e ∧ (∀ v, v ∈ G.nodes ↔ ∃ i, e i = v) ∧
    ∀ i j, S.Adj i j ↔ G.Adj (e i) (e j)

/-- `ofSimpleGraph S` is `S` renamed by `Fin.val`. -/
def RelabelOfSimpleGraph : Prop :=
  ∀ (n : ℕ) (S : SimpleGraph (Fin n)) [DecidableRel S.Adj],
    IsRelabel (Graph.ofSimpleGraph S) S Fin.val

/-- Every well-formed graph has a relabelling onto `Fin numNodes`. -/
def RelabelExists : Prop :=
  ∀ G : Graph, G.WF → ∃ (S : SimpleGraph (Fin G.numNodes)) (e : Fin G.numNodes → Nat),
    IsRelabel G S e

/-- Degrees are preserved by a relabelling. -/
def DegreeTransfer : Prop := by
  classical
  exact ∀ (G : Graph) (m : ℕ) (S : SimpleGraph (Fin m)) (e : Fin m → Nat),
    G.WF → IsRelabel G S e → ∀ i, S.degree i = G.degree (e i)

/-- Order transfer: an injective real labeling of a relabelling of `G` gives rational
labels on `G`, injective and nonzero on the nodes, whose frontiers at every rational
threshold are frontiers of `y` at some real threshold on the same side of `0`, and
whose level-zero counts are those of `y`. (Rank labels `2·rank - (2ℓ - 1)`.) Inner
thresholds `t < 0` may correspond to `s = 0`; then the inner frontier is `U`, of size
at most `C3.lowerZero S y`. -/
def LabelTransfer : Prop :=
  ∀ (G : Graph) (m : ℕ) (S : SimpleGraph (Fin m)) (e : Fin m → Nat),
    G.WF → IsRelabel G S e → ∀ y : Fin m → ℝ, Function.Injective y →
      ∃ Y : Labels, LabelsInjOn G Y ∧ (∀ v ∈ G.nodes, Y v ≠ 0) ∧
        (∀ t : ℚ, ∃ s : ℝ, (0 < t → 0 < s) ∧
          (outerFr G Y t).length = (C3.outerFrontier S y s).card) ∧
        (∀ t : ℚ, t < 0 → ∃ s : ℝ, s ≤ 0 ∧
          (innerFr G Y t).length = (C3.innerFrontier S y s).card) ∧
        lowerZeroP G Y = C3.lowerZero S y ∧ upperZeroP G Y = C3.upperZero S y

/-! ## 6.4 Deletion process -/

/-- One round of Proposition 9.10 (`prop:deletion`) for the vertex chosen by the algorithm
(Lemma A.34, `lem:alg-deletion`): a variant of `T4.DelX.key_step` in which `w` is given (maximum
torso degree on its torso component `C`, at least `6`, and either `C` is regular or
`w` has a neighbour of smaller degree), `B'` is any maximal reduction of
`(F - w, B - w)`, and some vertex of `C` survives. Non-basicness is not assumed. -/
def KeyStepAt : Prop :=
  ∀ (b : ℕ → ℝ), T4.BootProps b →
    ∀ (n : ℕ) (G : SimpleGraph (Fin n)) (F B C B' : Finset (Fin n)) (w : Fin n),
      T4.Good G F B → (∀ v ∈ B, 3 ≤ T4.tdeg G F B v) → C ∈ T4.tcomps G F B →
      w ∈ C → (∀ v ∈ C, T4.tdeg G F B v ≤ T4.tdeg G F B w) → 6 ≤ T4.tdeg G F B w →
      ((∀ v ∈ C, T4.tdeg G F B v = T4.tdeg G F B w) ∨
        ∃ x, (T4.tgraph G F B).Adj w x ∧ T4.tdeg G F B x < T4.tdeg G F B w) →
      B' ⊆ B.erase w → T4.Reach G (F.erase w, B.erase w) (F.erase w, B') →
      (∀ v ∈ B', 3 ≤ T4.tdeg G (F.erase w) B' v) → (∃ u ∈ B', u ∈ C) →
      1 + T4.psiMinus b G (F.erase w) B' ≤ T4.psiMinus b G F B

end CubicPathwidth.Alg