Executable graph encodings and triangle-free approximation
Lax47.Complexity · concepts/Lax47/Complexity.lean · lax-47
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
Graphs are finite Boolean adjacency matrices with symmetry and looplessness certificates. Their machine word is the vertex count followed by the complete row-major matrix, with Booleans encoded by and . An approximation is a function certified polynomial-time by the Lax759944 finite-Turing model; its returned independent set is decoded from that certified function.
Concept map
Lean source view on GitHub
| 1 | import Lax47.Machine |
| 2 | import Mathlib.Analysis.SpecialFunctions.Pow.Real |
| 3 | import Mathlib.Combinatorics.SimpleGraph.Clique |
| 4 | import Mathlib.Data.Finset.Card |
| 5 | |
| 6 | /-! |
| 7 | --- |
| 8 | title: Executable graph encodings and triangle-free approximation |
| 9 | type: definition |
| 10 | --- |
| 11 | Graphs are finite Boolean adjacency matrices with symmetry and looplessness |
| 12 | certificates. Their machine word is the vertex count followed by the complete |
| 13 | row-major matrix, with Booleans encoded by and . An approximation is a |
| 14 | function certified polynomial-time by the Lax759944 finite-Turing model; its |
| 15 | returned independent set is decoded from that certified function. |
| 16 | -/ |
| 17 | |
| 18 | set_option autoImplicit false |
| 19 | |
| 20 | namespace Lax47.Complexity |
| 21 | |
| 22 | open Lax47.Machine |
| 23 | |
| 24 | export Lax47.Machine |
| 25 | (BitString RandomSeed PolytimeProgram polynomialBound pairBits) |
| 26 | |
| 27 | /-- An executable simple graph on the labeled vertex set . -/ |
| 28 | structure GraphCode (n : ℕ) where |
| 29 | adjacent : Fin n → Fin n → Bool |
| 30 | loopless : ∀ vertex, adjacent vertex vertex = false |
| 31 | symmetric : ∀ left right, adjacent left right = adjacent right left |
| 32 | |
| 33 | /-- The mathematical simple graph represented by a Boolean adjacency matrix. -/ |
| 34 | def GraphCode.graph {n : ℕ} (code : GraphCode n) : SimpleGraph (Fin n) where |
| 35 | Adj left right := code.adjacent left right = true |
| 36 | symm := ⟨fun left right h ↦ by |
| 37 | rw [← code.symmetric] |
| 38 | exact h⟩ |
| 39 | loopless := ⟨fun vertex ↦ by |
| 40 | simp [code.loopless]⟩ |
| 41 | |
| 42 | /-- Vertex count followed by the row-major adjacency matrix. -/ |
| 43 | def GraphCode.bits {n : ℕ} (code : GraphCode n) : BitString := |
| 44 | n :: List.ofFn fun rank : Fin (n * n) ↦ |
| 45 | let vertex := finProdFinEquiv.symm rank |
| 46 | bitWord (code.adjacent vertex.1 vertex.2) |
| 47 | |
| 48 | /-- Decode the first output bits as a vertex set. -/ |
| 49 | def decodeVertexSet (n : ℕ) (bits : BitString) : Finset (Fin n) := |
| 50 | Finset.univ.filter fun vertex ↦ bits[vertex.1]? = some 1 |
| 51 | |
| 52 | /-- A polynomial-time executable approximation for triangle-free Max Independent Set. -/ |
| 53 | structure TriangleFreeMISApproximation (ε : ℝ) where |
| 54 | program : PolytimeProgram |
| 55 | correctness : ∀ (n : ℕ) (code : GraphCode n), |
| 56 | code.graph.CliqueFree 3 → |
| 57 | let set := decodeVertexSet n (program.output code.bits) |
| 58 | code.graph.IsIndepSet set ∧ |
| 59 | (code.graph.indepNum : ℝ) ≤ |
| 60 | Real.rpow n ((1 : ℝ) / 2 - ε) * set.card |
| 61 | |
| 62 | /-- Max Independent Set on triangle-free graphs admits a polynomial-time |
| 63 | -approximation. -/ |
| 64 | def TriangleFreeMISApproximable (ε : ℝ) : Prop := |
| 65 | Nonempty (TriangleFreeMISApproximation ε) |
| 66 | |
| 67 | end Lax47.Complexity |
| 68 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments