CubicPathwidth.Alg.Plan2Deletion

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

import CubicPathwidth.Alg.Plan2

/-!
# Plan interfaces for Tier 3 of Stage 2: the deletion process (task D0)

NOT part of the approval surface (`Spec2.lean`); like `Plan2.lean`, these statements
may be revised during proof work. Nothing is proved here and nothing is assumed.

## Task signatures (Tier 3)

Every task writes ONE file `CubicPathwidth/Alg/Proofs2/<File>.lean` importing
`CubicPathwidth.Alg.Plan2Deletion` (plus Stage 1 proofs and `T4.*` modules as needed),
and proves EXACTLY the theorem(s) below in namespace `CubicPathwidth.Alg`. Stage 1
results (`wfBasics`, `removeNodeSpec`, `inducedSpec`, `componentsSpec`, `unionAllSpec`,
`concatValid`, `plainLayoutValid`, `reduceRecordSpec`, `undoValid`, `t4InitInv`,
`t4LoopPreserves`, `ofSimpleGraphSpec`, `algoT4Exported`, the helpers of
`Proofs/T3LoopPreserves.lean`, ...) and the T4 / T3 theorems (`T4.seqClaim_h`,
`T4.torsoDynamics`, `T4.psiClaim`, `T4.coeff_le`, `T3.goodLabelsCount5_step`, ...) are
imported, never assumed. Stage 2 results are hypotheses with exactly these names.

```
-- D2d  Proofs2/OpsRecordFrame.lean                                  (M, Sonnet)
theorem opsRecordFrame : OpsRecordFrame

-- D6   Proofs2/TorsoLocal.lean                                      (S/M, Sonnet)
theorem torsoLocal : TorsoLocal

-- D3   Proofs2/TorsoBridge.lean                                     (M, Sonnet)
theorem torsoPotentialBridge : TorsoPotentialBridge
theorem psiPortFacts : PsiPortFacts

-- D2a1 Proofs2/T4LoopInit.lean                                      (M, Sonnet)
theorem t4LoopInvInit_of (hMax : ReduceRecordMaximal) (hConn : ComponentsConnected)
    (hCongr : OpsRecordCongr) : T4LoopInvInit

-- D2a2 Proofs2/T4LoopStep.lean                                      (L, Opus)
theorem t4LoopInvStep_of (hMax : ReduceRecordMaximal) (hConn : ComponentsConnected)
    (hCongr : OpsRecordCongr) (hApp : OpsRecordAppend) (hFrame : OpsRecordFrame) :
    T4LoopInvStep

-- D2b  Proofs2/CommitBound.lean                                     (L, Opus)
theorem commitBound_of (hKey : KeyStepAt) (hSim : TorsoSim) (hLoc : TorsoLocal)
    (hBr : TorsoPotentialBridge) (hMax : ReduceRecordMaximal)
    (hConn : ComponentsConnected) (hCongr : OpsRecordCongr) : CommitBound

-- D2c  Proofs2/T4LoopRun.lean                                       (M, Sonnet)
theorem t4LoopRun_of (hStep : T4LoopInvStep) (hCommit : CommitBound) : T4LoopRun

-- D5   Proofs2/DeletionBound.lean                                   (M, Sonnet)
theorem deletionProcessBound_of (hRun : T4LoopRun) (hInit : T4LoopInvInit)
    (hMax : ReduceRecordMaximal) : DeletionProcessBound
theorem t4FinalFacts_of (hRun : T4LoopRun) (hInit : T4LoopInvInit) : T4FinalFacts

-- N4   Proofs2/AlgoT4NoFallback.lean                                (M, Sonnet)
theorem algoT4NoFallback_of (hR1 : ReduceRecordNoFallback) (hD4 : T4LoopNoFallback)
    (hU3 : UndoNoFallback) (hRun : T4LoopRun) (hInit : T4LoopInvInit) : AlgoT4NoFallback

-- U5   Proofs2/ThinComponentWidth.lean   (revised: needs the thin-entry facts)  (S/M)
theorem thinComponentWidth_of (hU4 : UndoWidth) (hRun : T4LoopRun)
    (hInit : T4LoopInvInit) : ThinComponentWidth

-- K4a  Proofs2/SweepBound.lean                                      (M, Sonnet)
theorem sweepComponentBound_of (hL2 : PlainLayoutWidth) (hX2 : RelabelExists)
    (hX3 : DegreeTransfer) (hX4 : LabelTransfer) : SweepComponentBound

-- K4b  Proofs2/AlgoT4Internal.lean                                  (M/L, Opus)
theorem algoT4InternalBound_of (hSw : SweepComponentBound) (hA3 : AlgoT4Width)
    (hU5 : ThinComponentWidth) (hD5 : DeletionProcessBound) (hN4 : AlgoT4NoFallback)
    (hFin : T4FinalFacts) (hPsi : PsiPortFacts) (hX1 : RelabelOfSimpleGraph)
    (hX3 : DegreeTransfer) : AlgoT4InternalBound

-- K4c  Proofs2/AlgoT4Thm4.lean                                      (S, Haiku)
theorem algoT4RealizesTheorem4_of (h : AlgoT4InternalBound) : AlgoT4RealizesTheorem4

-- K5   Proofs2/AlgoT4Cor5.lean                                      (M, Sonnet)
theorem algoT4RealizesCorollary5_of (h : AlgoT4InternalBound) : AlgoT4RealizesCorollary5
```

DAG (leaves first; no cycles):
`D2d, D6, D3` (no Stage 2 hypotheses) → `D2a1, D2a2` (with R2, L3, R3, D2d) and
`D2b` (with D1, R4, D6, D3, R2, L3, R3) → `D2c` → `D5`, `N4` (with R1, D4, U3), `U5`
(with U4) → `K4b` (with K4a, A3, D3, X1, X3) → `K4c`, `K5`.

Routes.
* D2d: induction on `ops`, generalizing `K` and `M`; `redStep` of `M` and of `K` have
  the same nodes/adjacency up to `L` (`M.nbrs v` and `K.nbrs v` have the same elements,
  so the same length; `[a, b]` vs `[b, a]` gives the same `addEdge`).
* D6: `components G U` and `attachment G B T` only read `G` on `U`, `B ∪ T ⊆ F`.
  `Reach` by induction (steps keep `B ⊆ F` and shrink `F`).
* D3: `tcomps` are the node sets (closed, connected via `ReflTransGen`); `tdeg` =
  `J.degree` (the torso neighbours of `x ∈ J` are its `J`-neighbours, `nbrs` nodup);
  then `T4.psiMinus_eq_sum`. `PsiPortFacts`: `T4.runMin_le_self`,
  `T4.runMin_le_incr_three`, `T4.incr_three`.
* D2a1: Stage 1 `t4InitInv`; `OpsRecord G0.copy ops0 H` from R2, moved to `G0` by R3;
  `SameGraph H (unionAll (componentGraphs H).reverse)`; pieces by R2, L3.
* D2a2: four cases. Dump, finalize and thin: the graph list is permuted (Stage 1
  `T4Inv_perm`; `OpsRecord` only sees `R` up to `SameGraph`). Thin record: R2 on
  `J.copy.removeNode w`, R3 to `J.removeNode w`, final graph has no nodes. Commit:
  Stage 1 `commit_inv`; `OpsRecord M tops M'` by D2d with `K = J`,
  `L = unionAll (rest ++ finals)`, then R3-append; new pieces by R2, L3.
* D2b: `n` above every node of `J`, `S := J.toSimpleGraph n`, `V0` its node set.
  R4 with `ops = []` gives `Good S V0 V0` and the torso `J`; R4 on
  `J.removeNode w` (graph `S'`) with ops `red`, moved to `S` by D6 (`S`, `S'` agree on
  `V0.erase w`), gives the `Reach` and the torso `red.1`. D3 turns degrees, `tcomps`
  and `psiMinus` into port quantities; D1 at `C = V0` (regularity disjunction: a
  connected non-regular `J` has a maximum-degree vertex with a smaller neighbour, so
  `good ≠ []`); `T4.seqClaim_h.1` for `BootProps sigma`.
* D2c: induction on `fuel`; commit: `deletedSet` grows by one (`reduceRecordSpec`:
  only reductions), `List.Perm.sum_eq`, `CommitBound`.
* D5: `DeletionProcessBound` from D2c at the initial state, start value
  `∑ ψ⁻(components of H) ≤ ψ(H) ≤ ψ(G0) = ψ(G)` (`runMin ≥ 0`, R2 degrees,
  `σ 0 = 0` for isolated vertices, `σ` monotone and `≥ 0`).
* K4b: width `≤ D + max_e w_e + 3 log₂ n₀ + 1` (A3); sweep `w_e ≤ ψ(J) + ε n₀ + N ≤
  ψ⁻(J) + σ₃ + ε n₀ + N ≤ ∑ψ⁻ + σ₃ + ε n₀ + N` (K4a, D3, `T4FinalFacts`), thin
  `w_e ≤ 3 log₂ n₀ + 1` (U5); D5; `ψ(G) = degreeWeight S σ ≤ degreeWeight S thm4Coeff`;
  `6 log₂ n₀ + 2 ≤ ε n₀ + C`. The labeler is chosen per graph (`final` does not depend
  on `lab`, definitionally).
* K4c: `nonIsolatedCount S ≤ n`; `algoT4Exported`. K5: `nonIsolatedCount S ≤ 2m`,
  `T4.coeff_le`, `∑ deg = 2m`, `T4.hasPathwidth_mono`.
-/

noncomputable section

namespace CubicPathwidth.Alg

open Graph

/-! ## 6.5 Records in disjoint unions, locality of torsos -/

/-- Frame rule: a record on `K` is a record on any graph `M` that is the disjoint union
of `K` and `L`, ending in the disjoint union of the final graph `K'` and `L`. -/
def OpsRecordFrame : Prop :=
  ∀ (K K' L M M' : Graph) (ops : List Op), K.WF → L.WF → M.WF →
    (∀ x, x ∈ K.nodes → x ∉ L.nodes) →
    (∀ v, v ∈ M.nodes ↔ v ∈ K.nodes ∨ v ∈ L.nodes) →
    (∀ u v, M.Adj u v ↔ K.Adj u v ∨ L.Adj u v) →
    (∀ v, v ∈ M'.nodes ↔ v ∈ K'.nodes ∨ v ∈ L.nodes) →
    (∀ u v, M'.Adj u v ↔ K'.Adj u v ∨ L.Adj u v) →
    OpsRecord K ops K' → OpsRecord M ops M'

/-- The torso of a state, and reachability from it, only depend on the graph inside
the undeleted vertices. -/
def TorsoLocal : Prop :=
  ∀ (n : ℕ) (S S' : SimpleGraph (Fin n)) (F₀ : Finset (Fin n)),
    (∀ u ∈ F₀, ∀ v ∈ F₀, S.Adj u v ↔ S'.Adj u v) →
    (∀ F B : Finset (Fin n), B ⊆ F → F ⊆ F₀ → T4.tgraph S F B = T4.tgraph S' F B) ∧
    ∀ F B F' B' : Finset (Fin n), B ⊆ F → F ⊆ F₀ →
      T4.Reach S' (F, B) (F', B') → T4.Reach S (F, B) (F', B')

/-! ## 6.6 Pieces and the potential bridge (D3) -/

/-- A graph on the work list or in `final` of `algo_T4`: well formed, nonempty,
connected, minimum degree at least `3`. -/
def T4Piece (J : Graph) : Prop :=
  J.WF ∧ J.nodes ≠ [] ∧
    (∀ x ∈ J.nodes, ∀ y ∈ J.nodes, Relation.ReflTransGen J.Adj x y) ∧
    ∀ v ∈ J.nodes, 3 ≤ J.degree v

/-- The node set of a graph as a `Finset (Fin n)`. -/
def finNodes (n : ℕ) (J : Graph) : Finset (Fin n) :=
  Finset.univ.filter fun x : Fin n => x.val ∈ J.nodes

/-- (D3) A torso state whose torso is the disjoint union of a list of connected,
nonempty graphs (on vertices below `n`): torso degrees are degrees, torso components
are the node sets, and `ψ`, `ψ⁻` are the sums of `psiPort`, `psiMinusPort`. -/
def TorsoPotentialBridge : Prop :=
  ∀ (n : ℕ) (S : SimpleGraph (Fin n)) (F B : Finset (Fin n)) (gs : List Graph),
    (∀ J ∈ gs, J.WF ∧ J.nodes ≠ [] ∧
      ∀ x ∈ J.nodes, ∀ y ∈ J.nodes, Relation.ReflTransGen J.Adj x y) →
    gs.Pairwise (fun A C => ∀ x, x ∈ A.nodes → x ∉ C.nodes) →
    (∀ J ∈ gs, ∀ v ∈ J.nodes, v < n) →
    (∀ x : Fin n, x ∈ B ↔ ∃ J ∈ gs, x.val ∈ J.nodes) →
    (∀ x y : Fin n, (T4.tgraph S F B).Adj x y ↔ ∃ J ∈ gs, J.Adj x.val y.val) →
    (∀ J ∈ gs, ∀ x : Fin n, x.val ∈ J.nodes → T4.tdeg S F B x = J.degree x.val) ∧
    (∀ J ∈ gs, finNodes n J ∈ T4.tcomps S F B) ∧
    (∀ C ∈ T4.tcomps S F B, ∃ J ∈ gs, C = finNodes n J) ∧
    ∀ b : ℕ → ℝ, T4.psi b S F B = (gs.map (psiPort b)).sum ∧
      T4.psiMinus b S F B = (gs.map (psiMinusPort b)).sum

/-- (D3) `0 ≤ ψ⁻(J)` and `ψ(J) ≤ ψ⁻(J) + b₃` for a nonempty graph of minimum degree at
least `3` (port form of `T4.PsiClaim` and `runMin ≤ b₃`). -/
def PsiPortFacts : Prop :=
  ∀ b : ℕ → ℝ, T4.BootProps b → ∀ J : Graph, J.WF → J.nodes ≠ [] →
    (∀ v ∈ J.nodes, 3 ≤ J.degree v) →
    0 ≤ psiMinusPort b J ∧ psiPort b J ≤ psiMinusPort b J + b 3

/-! ## 6.7 The loop invariant of `t4Loop` (D2) -/

/-- (D2, part (a)) Structural invariant of the work loop of `algo_T4` relative to
`G0 = nonIsolated G`, for the work stack, the final list and the global ops: Stage 1's
`T4Inv` and `ThinOK`, the global ops are a legal record from `G0` to the union of all
current graphs, every current graph is a `T4Piece`, and every thin entry carries a
legal record emptying its graph with exactly one deletion. -/
def T4LoopInv (G0 : Graph) (stack : List Graph) (final : List FinalEntry) (ops : List Op) :
    Prop :=
  T4Inv G0 (stack ++ final.map (·.graph)) ops ∧ ThinOK final ∧
    OpsRecord G0 ops (unionAll (stack ++ final.map (·.graph))) ∧
    (∀ J ∈ stack ++ final.map (·.graph), T4Piece J) ∧
    ∀ e ∈ final, e.kind = FinalKind.thin →
      OpsRecord e.graph e.tops Graph.empty ∧ (deletedSet e.tops).length = 1

/-- (D2, part (b)) The potential `|D| + ∑_{J ∈ stack ++ final} ψ⁻_b(J)`, with `|D|`
the number of deletions recorded in the global ops. -/
def T4Pot (b : ℕ → ℝ) (stack : List Graph) (final : List FinalEntry) (ops : List Op) : ℝ :=
  ((deletedSet ops).length : ℝ) + ((stack ++ final.map (·.graph)).map (psiMinusPort b)).sum

/-- (D2a1) The invariant holds at the start of the loop in `algoT4Full`. -/
def T4LoopInvInit : Prop :=
  ∀ G : Graph, G.WF →
    let r := reduceRecordF (nonIsolated G).copy
    T4LoopInv (nonIsolated G) (componentGraphs r.1).reverse [] r.2.1

/-- (D2a2) One round of `t4Loop` preserves the structural invariant: fuel exhaustion
(the stack is dumped into `final`), finalizing a graph of maximum degree `≤ 5`, a thin
round, and a commit. -/
def T4LoopInvStep : Prop :=
  (∀ (G0 : Graph) (stack : List Graph) (final : List FinalEntry) (ops : List Op),
    G0.WF → T4LoopInv G0 stack final ops →
    T4LoopInv G0 [] (final ++ stack.map fun J => FinalEntry.mk J FinalKind.sweep []) ops) ∧
  ∀ (G0 J : Graph) (rest : List Graph) (final : List FinalEntry) (ops : List Op),
    G0.WF → T4LoopInv G0 (J :: rest) final ops →
    (J.maxDegree ≤ 5 →
      T4LoopInv G0 rest (final ++ [FinalEntry.mk J FinalKind.sweep []]) ops) ∧
    (¬ J.maxDegree ≤ 5 →
      let w := t4ChooseW J
      let red := reduceRecordF (J.copy.removeNode w)
      (red.1.numNodes = 0 →
        T4LoopInv G0 rest (final ++ [FinalEntry.mk J FinalKind.thin (Op.del w :: red.2.1)]) ops) ∧
      (red.1.numNodes ≠ 0 →
        T4LoopInv G0 ((componentGraphs red.1).reverse ++ rest) final
          (ops ++ (Op.del w :: red.2.1))))

/-- (D2b) Lemma A.34 (`lem:alg-deletion`) for one commit of the algorithm (via
`KeyStepAt`): deleting the chosen vertex `w` of a piece of maximum degree `≥ 6` and
reducing, when something survives, lowers `ψ⁻_σ` by at least `1`. -/
def CommitBound : Prop :=
  ∀ J : Graph, T4Piece J → ¬ J.maxDegree ≤ 5 →
    let red := reduceRecordF (J.copy.removeNode (t4ChooseW J))
    red.1.numNodes ≠ 0 →
    1 + ((componentGraphs red.1).map (psiMinusPort T4.sigma)).sum ≤ psiMinusPort T4.sigma J

/-- (D2c) The whole run of `t4Loop` (any fuel) from a state satisfying the invariant:
the invariant holds at the end, the potential `T4Pot σ` does not increase, and without
fallback every `.sweep` entry has maximum degree at most `5`. -/
def T4LoopRun : Prop :=
  ∀ (G0 : Graph) (fuel : Nat) (stack : List Graph) (final : List FinalEntry) (ops : List Op),
    G0.WF → T4LoopInv G0 stack final ops →
    (∀ e ∈ final, e.kind = FinalKind.sweep → e.graph.maxDegree ≤ 5) →
    let r := t4Loop fuel stack final ops
    T4LoopInv G0 [] r.1 r.2.1 ∧
      T4Pot T4.sigma [] r.1 r.2.1 ≤ T4Pot T4.sigma stack final ops ∧
      (r.2.2 = false → ∀ e ∈ r.1, e.kind = FinalKind.sweep → e.graph.maxDegree ≤ 5)

/-- (D5, second theorem) What the corollaries use about the final components of a run
without fallback. -/
def T4FinalFacts : Prop :=
  ∀ G : Graph, G.WF → ∀ lab : Labeler, (algoT4Full G lab).fallback = false →
    ∀ e ∈ (algoT4Full G lab).final,
      T4Piece e.graph ∧ e.graph.numNodes ≤ (nonIsolated G).numNodes ∧
        (e.kind = FinalKind.sweep → e.graph.MaxDegLE 5)

/-! ## 6.8 Internal form of Theorem 4 for `algo_T4` (K4, K5) -/

/-- (K4a) Plain sweep of one `.sweep` component with good labels: width at most
`ψ_σ(J) + ε |J| + N` (Theorem 3 with the triple `S` at minimum degree `3`,
`T3.GoodLabelsCount5`; small components by the trivial bound). -/
def SweepComponentBound : Prop :=
  T3.AdmissibleTriple (5 / 32) (1 / 4) (11 / 32) →
    ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ J : Graph, J.WF → J.MaxDegLE 5 →
      (∀ v ∈ J.nodes, 3 ≤ J.degree v) →
      ∃ Y : Labels, pdWidth (plainLayout J Y) ≤ psiPort T4.sigma J + ε * (J.numNodes : ℝ) + N

/-- The number `n₀` of non-isolated vertices. -/
def nonIsolatedCount {n : ℕ} (S : SimpleGraph (Fin n)) : ℕ := by
  classical
  exact (Finset.univ.filter fun v : Fin n => S.degree v ≠ 0).card

/-- (K4b) Internal form of Theorem 4 for `algo_T4`: `ε n₀ + C(ε)` with `n₀` the number of
non-isolated vertices, for EVERY `n` (no threshold). Both `AlgoT4RealizesTheorem4`
(`n₀ ≤ n`) and `AlgoT4RealizesCorollary5` (`n₀ ≤ 2m`, `thm4Coeff d ≤ 7d/96`) follow. -/
def AlgoT4InternalBound : Prop :=
  T3.AdmissibleTriple (5 / 32) (1 / 4) (11 / 32) →
    ∀ ε : ℝ, 0 < ε → ∃ C : ℝ, ∀ (n : ℕ) (S : SimpleGraph (Fin n)) [DecidableRel S.Adj],
      ∃ lab : Labeler,
        (algoT4Full (Graph.ofSimpleGraph S) lab).fallback = false ∧
        pdWidth (algoT4 (Graph.ofSimpleGraph S) lab) ≤
          T4.degreeWeight S T4.thm4Coeff + ε * (nonIsolatedCount S : ℝ) + C

end CubicPathwidth.Alg