Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Canonical representations of weighted graphs and vertex sets

Lax263307.IndependentSetEncoding · concepts/Lax263307/IndependentSetEncoding.lean · lax-263307

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

    An instance is represented by its order, row-major adjacency matrix, and rational vertex weights in vertex order. Each rational contributes its sign, absolute numerator, and positive denominator. The resulting list uses the registered structural list presentation. A vertex set is represented by its zero-one membership vector, whose length records the ambient graph order.

    These encoders inspect only the supplied graph, weights, and vertex set. The private injectivity proofs certify the representations without introducing any graph or weight decoder into the mathematical problem.

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

    Lean source view on GitHub

    1import Lax263307.WeightedIndependentSet
    2import Lax560851.StructuralCombinators
    3import Lax759944.BinaryWordEncoding
    4import Mathlib.Data.List.OfFn
    5
    6/-!
    7---
    8title: Canonical representations of weighted graphs and vertex sets
    9type: definition
    10---
    11An instance is represented by its order, row-major adjacency matrix, and
    12rational vertex weights in vertex order. Each rational contributes its sign,
    13absolute numerator, and positive denominator. The resulting list uses the
    14registered structural list presentation. A vertex set is represented by its
    15zero-one membership vector, whose length records the ambient graph order.
    16
    17These encoders inspect only the supplied graph, weights, and vertex set.
    18The private injectivity proofs certify the representations without introducing
    19any graph or weight decoder into the mathematical problem.
    20-/
    21
    22namespace Lax263307.IndependentSetEncoding
    23
    24open WeightedIndependentSet
    25open Lax560851.StructuralPresentation Lax560851.StructuralCombinators
    26open Lax759944.BinaryWordEncoding (bitSize)
    27open scoped Classical
    28
    29/-- Canonical sign, absolute numerator, and denominator of a rational. -/
    30def encodeRational (q : ℚ) : List ℕ :=
    31 [if q.num < 0 then 1 else 0, q.num.natAbs, q.den]
    32
    33/-- The rational parameters in vertex order, followed by the accuracy. -/
    34def encodeParameters {n : ℕ} (w : Fin n → ℚ) (ε : ℚ) : List ℕ :=
    35 (List.ofFn w).flatMap encodeRational ++ encodeRational ε
    36
    37/-- Total binary encoding length of the weights and the accuracy. -/
    38def rationalBitSize {n : ℕ} (w : Fin n → ℚ) (ε : ℚ) : ℕ :=
    39 bitSize (encodeParameters w ε)
    40
    41/-- The full input word, including the row-major adjacency matrix. -/
    42def encodeInput {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
    43 (w : Fin n → ℚ) (ε : ℚ) : List ℕ :=
    44 [n] ++ (List.ofFn fun u => List.ofFn fun v =>
    45 if G.Adj u v then 1 else 0).flatten ++ encodeParameters w ε
    46
    47/-- The length-`n` membership vector of the selected independent set. -/
    48def encodeOutput {n : ℕ} (I : Finset (Fin n)) : List ℕ :=
    49 List.ofFn fun v => if v ∈ I then 1 else 0
    50
    51
    52/-- Canonical graph-and-weight packet, without the accuracy parameter. -/
    53noncomputable abbrev encodeInstance {n : ℕ} (G : SimpleGraph (Fin n))
    54 (w : Fin n → ℚ) : List ℕ :=
    55 [n] ++ (List.ofFn fun u => List.ofFn fun v =>
    56 if G.Adj u v then 1 else 0).flatten ++
    57 (List.ofFn w).flatMap encodeRational
    58
    59/-- Equal-length blocks can be separated without interpreting their contents. -/
    60private theorem blocks_injective {α β : Type*} (f : α → List β) (k : ℕ)
    61 (length : ∀ a, (f a).length = k) (injective : Function.Injective f) :
    62 ∀ xs ys : List α, xs.length = ys.length → xs.flatMap f = ys.flatMap f → xs = ys
    63 | [], [], _, _ => rfl
    64 | [], _ :: _, h, _ => nomatch h
    65 | _ :: _, [], h, _ => nomatch h
    66 | x :: xs, y :: ys, hlength, h =>
    67 let fields := List.append_inj h ((length x).trans (length y).symm)
    68 congrArg₂ List.cons (injective fields.1)
    69 (blocks_injective f k length injective xs ys (Nat.succ.inj hlength) fields.2)
    70
    71private theorem blocks_length {α β : Type*} (f : α → List β) (k : ℕ)
    72 (length : ∀ a, (f a).length = k) (xs : List α) :
    73 (xs.flatMap f).length = xs.length * k :=
    74 calc
    75 (xs.flatMap f).length = (xs.map fun a => (f a).length).sum := List.length_flatMap
    76 _ = (xs.map fun _ => k).sum := congrArg (fun g => (xs.map g).sum) (funext length)
    77 _ = (List.replicate xs.length k).sum := congrArg List.sum List.map_const
    78 _ = xs.length * k := List.sum_replicate _ _
    79
    80private theorem flag_injective (p q : Prop) [Decidable p] [Decidable q]
    81 (h : (if p then 1 else 0 : ℕ) = if q then 1 else 0) : p ↔ q :=
    82 ⟨fun hp => not_not.mp (fun hq => Nat.one_ne_zero
    83 ((if_pos hp).symm.trans (h.trans (if_neg hq)))),
    84 fun hq => not_not.mp (fun hp => Nat.one_ne_zero
    85 ((if_pos hq).symm.trans (h.symm.trans (if_neg hp))))⟩
    86
    87private theorem signed_integer_injective : ∀ a b : ℤ,
    88 (if a < 0 then 1 else 0 : ℕ) = (if b < 0 then 1 else 0) →
    89 a.natAbs = b.natAbs → a = b
    90 | .ofNat _, .ofNat _, _, habs => congrArg Int.ofNat habs
    91 | .negSucc _, .negSucc _, _, habs => congrArg Int.negSucc (Nat.succ.inj habs)
    92 | .ofNat a, .negSucc b, hsign, _ => False.elim (Nat.zero_ne_one
    93 ((if_neg (not_lt.mpr (Int.natCast_nonneg a))).symm.trans
    94 (hsign.trans (if_pos (Int.negSucc_lt_zero b)))))
    95 | .negSucc a, .ofNat b, hsign, _ => False.elim (Nat.one_ne_zero
    96 ((if_pos (Int.negSucc_lt_zero a)).symm.trans
    97 (hsign.trans (if_neg (not_lt.mpr (Int.natCast_nonneg b))))))
    98
    99private theorem rational_injective : Function.Injective encodeRational :=
    100 fun a b h =>
    101 let fields := List.cons.inj h
    102 let rest := List.cons.inj fields.2
    103 Rat.ext (signed_integer_injective a.num b.num fields.1 rest.1)
    104 (List.cons.inj rest.2).1
    105
    106private theorem matrix_blocks {n : ℕ} (G : SimpleGraph (Fin n)) :
    107 (List.ofFn fun u => List.ofFn fun v => if G.Adj u v then 1 else 0).flatten =
    108 (List.ofFn fun u v => if G.Adj u v then 1 else 0).flatMap List.ofFn :=
    109 (congrArg List.flatten (List.map_ofFn (f := fun (u v : Fin n) => (if G.Adj u v then 1 else 0 : ℕ))
    110 (g := fun f : Fin n → ℕ => List.ofFn f))).symm
    111
    112private theorem matrix_length {n : ℕ} (G : SimpleGraph (Fin n)) :
    113 (List.ofFn fun u => List.ofFn fun v => if G.Adj u v then 1 else 0).flatten.length = n*n :=
    114 (congrArg List.length (matrix_blocks G)).trans
    115 ((blocks_length List.ofFn n (fun _ => List.length_ofFn) _).trans
    116 (congrArg (· * n) List.length_ofFn))
    117
    118private theorem matrix_injective {n : ℕ} (G H : SimpleGraph (Fin n))
    119 (h : (List.ofFn fun u => List.ofFn fun v => if G.Adj u v then 1 else 0).flatten =
    120 (List.ofFn fun u => List.ofFn fun v => if H.Adj u v then 1 else 0).flatten) : G = H :=
    121 let rows := blocks_injective List.ofFn n (fun _ => List.length_ofFn)
    122 List.ofFn_injective _ _ (List.length_ofFn.trans List.length_ofFn.symm)
    123 ((matrix_blocks G).symm.trans (h.trans (matrix_blocks H)))
    124 SimpleGraph.ext (funext fun u => funext fun v => propext
    125 (flag_injective _ _ (congrFun (congrFun (List.ofFn_injective rows) u) v)))
    126
    127private theorem weights_injective {n : ℕ} (w z : Fin n → ℚ)
    128 (h : (List.ofFn w).flatMap encodeRational = (List.ofFn z).flatMap encodeRational) : w = z :=
    129 List.ofFn_injective (blocks_injective encodeRational 3 (fun _ => rfl)
    130 rational_injective _ _ (List.length_ofFn.trans List.length_ofFn.symm) h)
    131
    132/-- The canonical packet determines all three mathematical instance fields. -/
    133private theorem encodeInstance_injective : Function.Injective
    134 (fun x : Instance => encodeInstance x.graph x.weights) :=
    135 fun x y h =>
    136 let order : x.order = y.order := (List.cons.inj h).1
    137 match x, y, order, h with
    138 | ⟨n,G,w⟩, ⟨_,H,z⟩, rfl, h =>
    139 let fields := List.append_inj (List.cons.inj h).2
    140 ((matrix_length G).trans (matrix_length H).symm)
    141 congrArg₂ (Instance.mk n) (matrix_injective G H fields.1) (weights_injective w z fields.2)
    142
    143private theorem list_injective :
    144 ∀ xs ys : List ℕ, listToRaw nat xs = listToRaw nat ys → xs = ys
    145 | [], [], _ => rfl
    146 | [], _ :: _, h => nomatch h
    147 | _ :: _, [], h => nomatch h
    148 | _ :: xs, _ :: ys, h =>
    149 let fields := Lax560851.StructuralPresentation.Raw.pair.inj h
    150 congrArg₂ List.cons (Lax560851.StructuralPresentation.Raw.nat.inj fields.1)
    151 (list_injective xs ys fields.2)
    152
    153/-- The standard structural-list representation of a weighted graph. -/
    154noncomputable def input : Presentation Instance :=
    155 presentationOf (fun x => listToRaw nat (encodeInstance x.graph x.weights))
    156
    157/-- Distinct mathematical instances have distinct structural representations. -/
    158theorem input_faithful : input.Faithful :=
    159 fun _ _ h => encodeInstance_injective (list_injective _ _ h)
    160
    161/-- A solution is written as its membership vector. -/
    162def output (s : Solution) : List ℕ := encodeOutput s.2
    163
    164/-- The vector's length and entries determine its ambient set and vertices. -/
    165theorem output_injective : Function.Injective output :=
    166 fun ⟨n,_I⟩ ⟨m,J⟩ h =>
    167 let order : n = m := List.length_ofFn.symm.trans
    168 ((congrArg List.length h).trans List.length_ofFn)
    169 match m, order, J, h with
    170 | _, rfl, _J, h =>
    171 congrArg (Sigma.mk n) (Finset.ext (fun v => flag_injective _ _
    172 (congrFun (List.ofFn_injective h) v)))
    173
    174end Lax263307.IndependentSetEncoding
    175
    Builds on
    Used by
    From Mathlib

    Discussion

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

    Loading discussion…