Lax Lean Archive

Executable graph encodings and triangle-free approximation

Lax614640.Complexity · concepts/Lax614640/Complexity.lean · lax-614640

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

    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 00 and 11. 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
    4 concepts; 3 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Lax614640.Machine
    2import Mathlib.Analysis.SpecialFunctions.Pow.Real
    3import Mathlib.Combinatorics.SimpleGraph.Clique
    4import Mathlib.Data.Finset.Card
    5
    6/-!
    7---
    8title: Executable graph encodings and triangle-free approximation
    9type: definition
    10---
    11Graphs are finite Boolean adjacency matrices with symmetry and looplessness
    12certificates. Their machine word is the vertex count followed by the complete
    13row-major matrix, with Booleans encoded by 00 and 11. An approximation is a
    14function certified polynomial-time by the Lax759944 finite-Turing model; its
    15returned independent set is decoded from that certified function.
    16-/
    17
    18set_option autoImplicit false
    19
    20namespace Lax614640.Complexity
    21
    22open Lax614640.Machine
    23
    24export Lax614640.Machine
    25 (BitString RandomSeed PolytimeProgram polynomialBound pairBits)
    26
    27/-- An executable simple graph on the labeled vertex set Fin⁡(n)\operatorname{Fin}(n). -/
    28structure 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. -/
    34def 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 ↦ (code.symmetric left right).symm.trans h⟩
    37 loopless := ⟨fun vertex h ↦ Bool.noConfusion ((code.loopless vertex).symm.trans h)⟩
    38
    39/-- Vertex count followed by the row-major adjacency matrix. -/
    40def GraphCode.bits {n : ℕ} (code : GraphCode n) : BitString :=
    41 n :: List.ofFn fun rank : Fin (n * n) ↦
    42 let vertex := finProdFinEquiv.symm rank
    43 bitWord (code.adjacent vertex.1 vertex.2)
    44
    45/-- Decode the first nn output bits as a vertex set. -/
    46def decodeVertexSet (n : ℕ) (bits : BitString) : Finset (Fin n) :=
    47 Finset.univ.filter fun vertex ↦ bits[vertex.1]? = some 1
    48
    49/-- A polynomial-time executable approximation for triangle-free Max Independent Set. -/
    50structure TriangleFreeMISApproximation (ε : ℝ) where
    51 program : PolytimeProgram
    52 correctness : ∀ (n : ℕ) (code : GraphCode n),
    53 code.graph.CliqueFree 3 →
    54 let set := decodeVertexSet n (program.output code.bits)
    55 code.graph.IsIndepSet set ∧
    56 (code.graph.indepNum : ℝ) ≤
    57 Real.rpow n ((1 : ℝ) / 2 - ε) * set.card
    58
    59/-- Max Independent Set on triangle-free graphs admits a polynomial-time
    60n1/2−εn^{1/2-\varepsilon}-approximation. -/
    61def TriangleFreeMISApproximable (ε : ℝ) : Prop :=
    62 Nonempty (TriangleFreeMISApproximation ε)
    63
    64end Lax614640.Complexity
    65
    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…