Lax Lean Archive

The Bonnet–Chang reduction

Lax762056.Reduction · concepts/Lax762056/Reduction.lean · lax-762056

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    Order the vertices of FF as 0,…,n−10,\ldots,n-1. For every edge uvuv with u<vu<v, reserve rows (uv,0)(uv,0) and (uv,1)(uv,1) in an intermediate graph with 2n−12n-1 columns. Keep only columns from 2u2u through 2v2v. In row (uv,t)(uv,t) keep only side tt at column 2u2u and side 1−t1-t at column 2v2v; keep both sides at every intervening column. The resulting induced subgraph is GFG_F.

    The additive offset is b(F)=2∑uv∈E(F), u<v(v−u)b(F)=2\sum_{uv\in E(F),\,u<v}(v-u).

    Concept map
    5 concepts; 3 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    In the paper

    • page 4 of this submission's paper

    Lean source view on GitHub

    1import Lax762056.ColumnGraph
    2import Lax762056.MaxCut
    3
    4/-!
    5---
    6title: The Bonnet–Chang reduction
    7type: definition
    8---
    9Order the vertices of FF as 0,…,n−10,\ldots,n-1. For every edge uvuv with u<vu<v,
    10reserve rows (uv,0)(uv,0) and (uv,1)(uv,1) in an intermediate graph with 2n−12n-1
    11columns. Keep only columns from 2u2u through 2v2v. In row (uv,t)(uv,t) keep
    12only side tt at column 2u2u and side 1−t1-t at column 2v2v; keep both sides
    13at every intervening column. The resulting induced subgraph is GFG_F.
    14
    15The additive offset is b(F)=2∑uv∈E(F), u<v(v−u)b(F)=2\sum_{uv\in E(F),\,u<v}(v-u).
    16-/
    17
    18namespace Lax762056.Reduction
    19
    20open ColumnGraph MaxCut
    21
    22abbrev Edge {n : ℕ} (F : SimpleGraph (Fin n)) :=
    23 {e : Fin n × Fin n // e.1 < e.2 ∧ F.Adj e.1 e.2}
    24
    25abbrev Row {n : ℕ} (F : SimpleGraph (Fin n)) := Edge F × Bool
    26
    27abbrev Vertex {n : ℕ} (F : SimpleGraph (Fin n)) :=
    28 ColumnGraph.Vertex (Row F) (2 * n - 1)
    29
    30def retainedVertices {n : ℕ} (F : SimpleGraph (Fin n)) : Set (Vertex F) :=
    31 fun ((edge, tag), column, side) =>
    32 let u := edge.val.1.val
    33 let v := edge.val.2.val
    34 let j := column.val
    35 (j = 2 * u ∧ side = tag) ∨
    36 (2 * u < j ∧ j < 2 * v) ∨
    37 (j = 2 * v ∧ side = !tag)
    38
    39def reductionGraph {n : ℕ} (F : SimpleGraph (Fin n)) :
    40 SimpleGraph (retainedVertices F) :=
    41 (columnGraph (Row F) (2 * n - 1)).induce (retainedVertices F)
    42
    43noncomputable def offset {n : ℕ} (F : SimpleGraph (Fin n)) : ℕ :=
    44 2 * ∑ e ∈ edges F, (e.2.val - e.1.val)
    45
    46end Lax762056.Reduction
    47
    Builds on
    Used by
    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…