import CubicPathwidth.Alg.Spec
import CubicPathwidth.C3.Defs
import CubicPathwidth.T2.DefsB
import CubicPathwidth.T3.Defs
import CubicPathwidth.T4.Defs
import CubicPathwidth.T4.ProcessDefs

/-!
# Stage 2 statements for the port of `sweep.py` (DRAFT approval surface)

STATUS: DRAFT FOR APPROVAL (2026-10-09). Every `def … : Prop` below is a proposition
that we DEFINE; nothing is proved here and nothing is assumed. Proofs go in
`CubicPathwidth/Alg/Proofs2/*.lean`, one theorem per Prop.

Scope ("deterministic bridge", chosen by the user):
1. the fallbacks of the port never fire (the statements of `Spec.lean` §7, unchanged,
   plus contract-level versions in §2 below);
2. the width of every output is bounded by the quantities that the existing Lean
   existence proofs control (frontiers of a labeling, the level-zero counts, `lem:undo`
   of the paper for undoing reductions, `lem:alg-deletion` for the deletion process);
3. corollaries: for every graph SOME labeling makes the implemented algorithm meet
   Theorems 1–4 and Corollary 5, in the ε–N form of the frozen statements, under the
   same external hypotheses as the existing Lean targets.

What is NOT covered: how the labels are computed (local Gaussian labels, the finite
law, perturbation, derandomization: Section 10 of the paper). The labels are
existentially quantified; the corollaries say that the decomposition-building code
realizes the existence theorems.

Paper references (labels of the paper):
`lem:undo`, `cl:alg-elim`,
`cl:alg-balanced`, `lem:connector-linear`,
`lem:alg-deletion`, `prop:alg-sweep`; and
`lem:median-layout`.

Labels. The port takes rational labels `Y : Nat → ℚ`; the existing good labels are
real and injective on `Fin n`. The bridges (§3) are stated for rational labels that
are injective on the nodes (and nonzero, for the switched layout), with frontiers at
rational thresholds that mirror `C3.outerFrontier`, `C3.innerFrontier`,
`C3.lowerZero`, `C3.upperZero` exactly. The passage from real to rational labels is
the plan interface `LabelTransfer` (`Plan2.lean`): the layouts depend only on the order of
the labels and on their signs, so the rank labels `Y v = 2·rank(v) - (2ℓ - 1)`
(`ℓ` = number of labels `≤ 0`) are odd integers, never zero, with the same order and
sign pattern as `y`. This keeps the approval surface free of real-number arithmetic
on the port side, and the transfer is a separate, purely combinatorial task.

This file (§§1–5) is the approval surface. The plan interfaces (§6) are in
`Plan2.lean`; they may change during proof work without renewed approval.
-/

noncomputable section

namespace CubicPathwidth.Alg

open Graph

/-! # Approval surface -/

/-! ## 1. Vocabulary -/

/-- The labels separate the nodes of `G` (no ties among nodes). -/
def LabelsInjOn (G : Graph) (Y : Labels) : Prop :=
  ∀ u ∈ G.nodes, ∀ v ∈ G.nodes, Y u = Y v → u = v

/-- Outer frontier of the level set `{Y ≤ t}`: nodes above `t` with a neighbour at or
below `t`. Mirror of `C3.outerFrontier` (the frontier `Fr(t)` of the plain sweep). -/
def outerFr (G : Graph) (Y : Labels) (t : ℚ) : List Nat :=
  G.nodes.filter fun w => decide (t < Y w) && (G.nbrs w).any fun u => decide (Y u ≤ t)

/-- Inner frontier of the level set `{Y ≤ t}`: its nodes with a neighbour above `t`.
Mirror of `C3.innerFrontier`. -/
def innerFr (G : Graph) (Y : Labels) (t : ℚ) : List Nat :=
  G.nodes.filter fun u => decide (Y u ≤ t) && (G.nbrs u).any fun w => decide (t < Y w)

/-- `L₀ = |U| + |D ∩ W|` with the sets `U`, `Wset`, `Dset` of `switched_layout`
(`inU`, `inW`, `inD` of `Port.lean`). Mirror of `C3.lowerZero`. -/
def lowerZeroP (G : Graph) (Y : Labels) : Nat :=
  (G.nodes.filter (inU G Y)).length +
    (G.nodes.filter fun v => inD G Y v && inW G Y v).length

/-- `L₀' = |W| + |D ∩ low|`. Mirror of `C3.upperZero`. -/
def upperZeroP (G : Graph) (Y : Labels) : Nat :=
  (G.nodes.filter (inW G Y)).length +
    (G.nodes.filter fun v => inD G Y v && isLow Y v).length

/-- One reduction (R1)–(R4) at `v`, exactly as one step of `reduceLoop`: remove `v`
and, if it has two neighbours, join them (no-op if already adjacent). -/
def redStep (G : Graph) (v : Nat) : Graph :=
  match G.nbrs v with
  | [a, b] => (G.removeNode v).addEdge a b
  | _ => G.removeNode v

/-- Same node set and same adjacency (orders of lists ignored). -/
def SameGraph (G H : Graph) : Prop :=
  (∀ v, v ∈ G.nodes ↔ v ∈ H.nodes) ∧ ∀ u v, G.Adj u v ↔ H.Adj u v

/-- `OpsRecord F ops R`: applying the recorded operations to `F` in order is a legal
sequence of reductions and deletions that ends in a graph with the nodes and edges
of `R` (the setting of `lem:undo`). A step `.red v nb` requires `v` to be a node of
degree at most two whose neighbours are exactly the elements of `nb` (in any order);
a step `.del w` requires `w` to be a node. -/
def OpsRecord : Graph → List Op → Graph → Prop
  | F, [], R => SameGraph F R
  | F, .red v nb :: ops, R =>
      v ∈ F.nodes ∧ nb.Nodup ∧ nb.length ≤ 2 ∧ (∀ x, x ∈ nb ↔ F.Adj v x) ∧
        OpsRecord (redStep F v) ops R
  | F, .del w :: ops, R => w ∈ F.nodes ∧ OpsRecord (F.removeNode w) ops R

/-- `ψ_b(J) = ∑_{v ∈ J} b(deg_J v)` (the potential `ψ` of `sec:bootstrap-lemma`). -/
def psiPort (b : ℕ → ℝ) (J : Graph) : ℝ := (J.nodes.map fun v => b (J.degree v)).sum

/-- Minimum degree (`0` for the empty graph). -/
def minDegree (J : Graph) : Nat := ((J.nodes.map J.degree).min?).getD 0

/-- `ψ⁻_b(J) = ψ_b(J) - H_{δ(J)}` for a connected graph `J`, with `H = T4.runMin b`
(the potential `ψ⁻` of `sec:bootstrap-proof`, one torso component). -/
def psiMinusPort (b : ℕ → ℝ) (J : Graph) : ℝ := psiPort b J - T4.runMin b (minDegree J)

/-! ## 2. The fallbacks never fire

`Spec.lean` §7 already states `ConnectorNoFallback`, `ReduceRecordNoFallback`,
`PdTw2NoFallback`, `AlgoT1NoFallback`, `AlgoMixedNoFallback` and `AlgoT4NoFallback`.
We checked them against the code and the paper and propose to approve them
UNCHANGED (no revised versions are needed). The following contract-level
statements complete them; they are the inputs that the top-level no-fallback proofs
use. -/

/-- `reduce_record` is a legal maximal sequence of reductions (`lem:reduction`
(F1), (F3)): its ops form an `OpsRecord` from `G` to the result; the result has
minimum degree at least `3`, and no degree increased. -/
def ReduceRecordMaximal : Prop :=
  ∀ G : Graph, G.WF →
    let r := reduceRecord G
    OpsRecord G r.2 r.1 ∧
      (∀ v ∈ r.1.nodes, 3 ≤ r.1.degree v) ∧
      (∀ v ∈ r.1.nodes, r.1.degree v ≤ G.degree v)

/-- `undo` never falls back (`lem:undo`; invariant (I2) of `lem:reduction`, and
`cl:alg-elim`, `cl:alg-balanced` for the calls of `pd_tw2`) when its input is a legal
record of reductions and deletions from `F` to `R` and `bagsR` decomposes `R`. -/
def UndoNoFallback : Prop :=
  ∀ (F R : Graph) (ops : List Op) (bagsR : List Bag),
    F.WF → R.WF → OpsRecord F ops R → ValidPD R bagsR →
    (undoF F ops R bagsR).2 = false

/-- The deletion loop of `algo_T4` never runs out of fuel (`lem:alg-deletion`: at
most `n` commits and `n` final components, so at most `2n` rounds), and no
reduction inside it does. Stated for the initial call made by `algoT4Full`. -/
def T4LoopNoFallback : Prop :=
  ∀ G : Graph, G.WF →
    let H := (reduceRecordF (nonIsolated G).copy).1
    let ops0 := (reduceRecordF (nonIsolated G).copy).2.1
    (t4Loop (2 * H.numNodes + 1) (componentGraphs H).reverse [] ops0).2.2 = false

/-! ## 3. Width bridges (contract level, one per function)

Widths are `pdWidth = (largest bag, read as a set) - 1`, as in `Spec.lean`; a bound
`pdWidth bags ≤ w` says every bag has at most `w + 1` distinct vertices. -/

/-- Plain sweep (`prop:alg-sweep`, `lem:layout`): bag `i` is `{v_i}` plus the
frontier of the first `i - 1` vertices, so for labels without ties the width is at
most the largest outer frontier `|Fr(t)|`. Port analogue of `T2.PlainLayoutClaim`. -/
def PlainLayoutWidth : Prop :=
  ∀ G : Graph, G.WF → ∀ Y : Labels, LabelsInjOn G Y →
    ∀ w : ℝ, (∀ t : ℚ, ((outerFr G Y t).length : ℝ) ≤ w) →
      pdWidth (plainLayout G Y) ≤ w

/-- Connector order (`lem:connector-linear`): if every item
has one or two distinct endpoints in `Qs`, the output is a permutation of `Qs`, and
after `j` elements at most `max(0, |Qs| - |items|) + 1` more elements than covered
items have been placed (inequality `eq:cubic-connector`). Here `c(j)` counts the
items contained in the first `j` elements. -/
def ConnectorLemma10 : Prop :=
  ∀ (Qs : List Nat) (items : List (List Nat)), Qs.Nodup →
    (∀ e ∈ items, e.Nodup ∧ 1 ≤ e.length ∧ e.length ≤ 2 ∧ ∀ z ∈ e, z ∈ Qs) →
    (connectorOrder Qs items).Perm Qs ∧
      ∀ j, j ≤ Qs.length →
        (j : ℤ) - ((items.filter fun e => subsetB e ((connectorOrder Qs items).take j)).length : ℤ)
          ≤ max 0 ((Qs.length : ℤ) - (items.length : ℤ)) + 1

/-- Median-switched layout (`lem:median-layout` with the connector of
`lem:connector-linear`): for maximum degree `≤ 3` and labels without ties and
without zeros, inner frontiers below `0`, outer frontiers above `0` and
`max(L₀, L₀') + 1` bound the width, and the connector does not fall back. Port
analogue of `C3.SwitchedLayoutClaim` (same hypotheses). -/
def SwitchedLayoutWidth : Prop :=
  ∀ G : Graph, G.WF → G.MaxDegLE 3 → ∀ Y : Labels, LabelsInjOn G Y →
    (∀ v ∈ G.nodes, Y v ≠ 0) → ∀ w : ℝ,
      (∀ t : ℚ, t < 0 → ((innerFr G Y t).length : ℝ) ≤ w) →
      (∀ t : ℚ, 0 < t → ((outerFr G Y t).length : ℝ) ≤ w) →
      (max (lowerZeroP G Y) (upperZeroP G Y) : ℝ) + 1 ≤ w →
      (switchedLayoutF G Y).2 = false ∧ pdWidth (switchedLayout G Y) ≤ w

/-- `pd_tw2` (`lem:undo`, step 3): when no fallback fires, every bag has at most
`3 ⌊log₂ N⌋ + 1` vertices (width `3 ⌊log₂ N⌋`), for every fuel. -/
def PdTw2Width : Prop :=
  ∀ (fuel : Nat) (H : Graph), H.WF → (pdTw2Fuel fuel H).2 = false →
    maxBagCard (pdTw2Fuel fuel H).1 ≤ 3 * Nat.log 2 H.numNodes + 1

/-- `undo` (`lem:undo`): when no fallback fires, the width is at most
`|D| + w + 3 ⌊log₂ |V(F)|⌋ + 1`, where `w` is the width of `bagsR`. (The lemma states
`+ 3 log₂ n + 4`; its proof, and this statement, give `+ 1`.) -/
def UndoWidth : Prop :=
  ∀ (F R : Graph) (ops : List Op) (bagsR : List Bag), F.WF →
    (undoF F ops R bagsR).2 = false →
    pdWidth (undo F ops R bagsR) ≤
      ((deletedSet ops).toFinset.card : ℝ) + pdWidth bagsR + 3 * (Nat.log 2 F.numNodes : ℝ) + 1

/-- The deletion process (`lem:alg-deletion`): the number of deleted
vertices plus `ψ⁻` of the final components is at most `ψ(G)`, for the bootstrap
sequence `σ` of the triple `S` (`T4.sigma`). -/
def DeletionProcessBound : Prop :=
  ∀ G : Graph, G.WF → ∀ lab : Labeler,
    (algoT4Full G lab).fallback = false →
    ((algoT4Full G lab).numDeleted : ℝ) +
        ((algoT4Full G lab).final.map fun e => psiMinusPort T4.sigma e.graph).sum
      ≤ psiPort T4.sigma G

/-! ## 4. Top-level width statements, one per algorithm -/

/-- `algo_T1` (Theorem 1 algorithm): the switched-layout bridge. -/
def AlgoT1Width : Prop :=
  ∀ G : Graph, G.WF → G.MaxDegLE 3 → ∀ Y : Labels, LabelsInjOn G Y →
    (∀ v ∈ G.nodes, Y v ≠ 0) → ∀ w : ℝ,
      (∀ t : ℚ, t < 0 → ((innerFr G Y t).length : ℝ) ≤ w) →
      (∀ t : ℚ, 0 < t → ((outerFr G Y t).length : ℝ) ≤ w) →
      (max (lowerZeroP G Y) (upperZeroP G Y) : ℝ) + 1 ≤ w →
      pdWidth (algoT1 G Y) ≤ w

/-- `algo_T2a` (Theorem 2(a) algorithm): the plain-sweep bridge. -/
def AlgoT2aWidth : Prop :=
  ∀ G : Graph, G.WF → ∀ Y : Labels, LabelsInjOn G Y →
    ∀ w : ℝ, (∀ t : ℚ, ((outerFr G Y t).length : ℝ) ≤ w) →
      pdWidth (algoT2a G Y) ≤ w

/-- `algo_mixed` (Theorems 2(b,c), 3; `sec:alg-plain`, step 4): the width is at most
the width of the plain sweep of the reduced graph `H` plus `3 ⌊log₂ n⌋ + 1`
(`lem:undo` with `D = ∅`). -/
def AlgoMixedWidth : Prop :=
  ∀ G : Graph, G.WF → ∀ lab : Labeler, (algoMixedF G lab).2 = false →
    let H := (reduceRecord G.copy).1
    pdWidth (algoMixed G lab) ≤ pdWidth (plainLayout H (lab H)) + 3 * (Nat.log 2 G.numNodes : ℝ) + 1

/-- `algo_T4` (Theorem 4, Corollary 5; `sec:alg-general`, step 4): the width is at
most the number of deleted vertices plus the width of the concatenated
decompositions of the final components plus `3 ⌊log₂ n₀⌋ + 1`, where `n₀` counts the
non-isolated vertices (`lem:undo` applied to `G₀`). -/
def AlgoT4Width : Prop :=
  ∀ G : Graph, G.WF → ∀ lab : Labeler, (algoT4Full G lab).fallback = false →
    pdWidth (algoT4 G lab) ≤
      ((algoT4Full G lab).numDeleted : ℝ) +
        pdWidth (((algoT4Full G lab).final.map (t4Decompose lab)).flatMap (·.1)) +
        3 * (Nat.log 2 (nonIsolated G).numNodes : ℝ) + 1

/-- A thin final component (`sec:alg-general`, step 3) is decomposed with width at
most `3 ⌊log₂ |V(J)|⌋ + 1` (`lem:undo` with `D = {w}` and `R` empty). -/
def ThinComponentWidth : Prop :=
  ∀ G : Graph, G.WF → ∀ lab : Labeler, (algoT4Full G lab).fallback = false →
    ∀ e ∈ (algoT4Full G lab).final, e.kind = FinalKind.thin →
      pdWidth (t4Decompose lab e).1 ≤ 3 * (Nat.log 2 e.graph.numNodes : ℝ) + 1

/-! ## 5. Corollaries: the existence theorems are realized by the algorithms

Each statement has the quantifier structure of the frozen statement it realizes
(`C3Spec.lean`, `T2Spec.lean`, `T3Spec.lean`, `T4Spec.lean`), with the same external
hypothesis as the existing Lean target, and asserts for every graph `S` on `Fin n`
the existence of labels for which the port, run on `Graph.ofSimpleGraph S`, does not
fall back, outputs a path decomposition of `S` (`HasPathwidthAtMost`, already given
by the Stage 1 `…Exported` theorems), and has the claimed width. Hence each implies
its frozen theorem. -/

/-- Theorem 1 (`C3MainClaim`, second conjunct) realized by `algo_T1`. Unconditional,
as `C3.c3MainClaim` is. -/
def AlgoT1RealizesTheorem1 : Prop :=
  ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
    ∀ (S : SimpleGraph (Fin n)) [DecidableRel S.Adj], IsSubcubic S →
      ∃ Y : Labels,
        (algoT1F (Graph.ofSimpleGraph S) Y).2 = false ∧
        HasPathwidthAtMost S (pdWidth (algoT1 (Graph.ofSimpleGraph S) Y)) ∧
        pdWidth (algoT1 (Graph.ofSimpleGraph S) Y) ≤ (C3.c3 + ε) * (n : ℝ)

/-- Theorem 2(a) realized by `algo_T2a`, under hypothesis H1 (`T2.SimplexFourClaim`),
as `T2.Target2a`. -/
def AlgoT2aRealizesTheorem2a : Prop :=
  T2.SimplexFourClaim →
    ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
      ∀ (S : SimpleGraph (Fin n)) [DecidableRel S.Adj], T2.MaxDegreeAtMost 4 S →
        ∃ Y : Labels,
          HasPathwidthAtMost S (pdWidth (algoT2a (Graph.ofSimpleGraph S) Y)) ∧
          pdWidth (algoT2a (Graph.ofSimpleGraph S) Y) ≤ (T2.F4 + ε) * (n : ℝ)

/-- `algo_mixed` meets `pw ≤ a₃ n₃ + a₄ n₄ + o(n)` for maximum degree 4. -/
def MixedRealizes4 (a₃ a₄ : ℝ) : Prop :=
  ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
    ∀ (S : SimpleGraph (Fin n)) [DecidableRel S.Adj], T2.MaxDegreeAtMost 4 S →
      ∃ lab : Labeler,
        (algoMixedF (Graph.ofSimpleGraph S) lab).2 = false ∧
        HasPathwidthAtMost S (pdWidth (algoMixed (Graph.ofSimpleGraph S) lab)) ∧
        pdWidth (algoMixed (Graph.ofSimpleGraph S) lab) ≤
          a₃ * (T2.degreeCount S 3 : ℝ) + a₄ * (T2.degreeCount S 4 : ℝ) + ε * (n : ℝ)

/-- `algo_mixed` meets `pw ≤ a₃ n₃ + a₄ n₄ + a₅ n₅ + o(n)` for maximum degree 5. -/
def MixedRealizes5 (a₃ a₄ a₅ : ℝ) : Prop :=
  ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
    ∀ (S : SimpleGraph (Fin n)) [DecidableRel S.Adj], T2.MaxDegreeAtMost 5 S →
      ∃ lab : Labeler,
        (algoMixedF (Graph.ofSimpleGraph S) lab).2 = false ∧
        HasPathwidthAtMost S (pdWidth (algoMixed (Graph.ofSimpleGraph S) lab)) ∧
        pdWidth (algoMixed (Graph.ofSimpleGraph S) lab) ≤
          a₃ * (T2.degreeCount S 3 : ℝ) + a₄ * (T2.degreeCount S 4 : ℝ) +
            a₅ * (T2.degreeCount S 5 : ℝ) + ε * (n : ℝ)

/-- Theorem 2(b) realized by `algo_mixed` (hypothesis as `T2.Target2b`). -/
def AlgoMixedRealizesTheorem2b : Prop :=
  T2.AdmissiblePair T2.Fcubic (103 / 400) → MixedRealizes4 T2.Fcubic (103 / 400)

/-- Theorem 2(c) realized by `algo_mixed` (hypothesis as `T2.Target2c`). -/
def AlgoMixedRealizesTheorem2c : Prop :=
  T2.AdmissiblePair (5 / 32) (1 / 4) → MixedRealizes4 (5 / 32) (1 / 4)

/-- Theorem 3 with the triple `P` realized by `algo_mixed` (as `T3.Target3P`). -/
def AlgoMixedRealizesTheorem3P : Prop :=
  T3.AdmissibleTriple T2.Fcubic (103 / 400) (3667 / 10000) →
    MixedRealizes5 T2.Fcubic (103 / 400) (3667 / 10000)

/-- Theorem 3 with the triple `R` realized by `algo_mixed` (as `T3.Target3R`). -/
def AlgoMixedRealizesTheorem3R : Prop :=
  T3.AdmissibleTriple (291 / 2000) (253 / 1000) (9 / 25) →
    MixedRealizes5 (291 / 2000) (253 / 1000) (9 / 25)

/-- Theorem 3 with the triple `S` realized by `algo_mixed` (as `T3.Target3S`). -/
def AlgoMixedRealizesTheorem3S : Prop :=
  T3.AdmissibleTriple (5 / 32) (1 / 4) (11 / 32) →
    MixedRealizes5 (5 / 32) (1 / 4) (11 / 32)

/-- Theorem 4 (with the refined coefficients `T4.thm4Coeff`) realized by `algo_T4`
(hypothesis as `T4.Target4`). -/
def AlgoT4RealizesTheorem4 : Prop :=
  T3.AdmissibleTriple (5 / 32) (1 / 4) (11 / 32) →
    ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
      ∀ (S : SimpleGraph (Fin n)) [DecidableRel S.Adj],
        ∃ lab : Labeler,
          (algoT4Full (Graph.ofSimpleGraph S) lab).fallback = false ∧
          HasPathwidthAtMost S (pdWidth (algoT4 (Graph.ofSimpleGraph S) lab)) ∧
          pdWidth (algoT4 (Graph.ofSimpleGraph S) lab) ≤
            T4.degreeWeight S T4.thm4Coeff + ε * (n : ℝ)

/-- Corollary 5 realized by `algo_T4` (hypothesis as `T4.Target5`); uniform in the
number of edges, isolated vertices allowed. -/
def AlgoT4RealizesCorollary5 : Prop :=
  T3.AdmissibleTriple (5 / 32) (1 / 4) (11 / 32) →
    ∀ ε : ℝ, 0 < ε → ∃ M : ℕ, ∀ n : ℕ, ∀ (S : SimpleGraph (Fin n)) [DecidableRel S.Adj],
      M ≤ T4.edgeCount S →
        ∃ lab : Labeler,
          (algoT4Full (Graph.ofSimpleGraph S) lab).fallback = false ∧
          HasPathwidthAtMost S (pdWidth (algoT4 (Graph.ofSimpleGraph S) lab)) ∧
          pdWidth (algoT4 (Graph.ofSimpleGraph S) lab) ≤ (7 / 48 + ε) * (T4.edgeCount S : ℝ)

end CubicPathwidth.Alg