Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Lax47.Complexity

Executable graph encodings and triangle-free approximation

concepts/Lax47/Complexity.lean · lax-47

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.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    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 Lax51 finite-Turing model; its returned independent set is decoded from that certified function.

    Lean source view on GitHub

    1import Lax47.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 Lax51 finite-Turing model; its
    15returned independent set is decoded from that certified function.
    16-/
    17
    18set_option autoImplicit false
    19
    20namespace Lax47.Complexity
    21
    22open Lax47.Machine
    23
    24export Lax47.Machine
    25 (BitString Language RandomSeed PolytimeProgram NPVerifier BPPAlgorithm
    26 InNP InBPP NPSubsetBPP polynomialBound pairBits)
    27
    28/-- An executable simple graph on the labeled vertex set Fin⁡(n)\operatorname{Fin}(n). -/
    29structure GraphCode (n : ℕ) where
    30 adjacent : Fin n → Fin n → Bool
    31 loopless : ∀ vertex, adjacent vertex vertex = false
    32 symmetric : ∀ left right, adjacent left right = adjacent right left
    33
    34/-- The mathematical simple graph represented by a Boolean adjacency matrix. -/
    35def GraphCode.graph {n : ℕ} (code : GraphCode n) : SimpleGraph (Fin n) where
    36 Adj left right := code.adjacent left right = true
    37 symm left right h := by
    38 change code.adjacent right left = true
    39 rw [← code.symmetric]
    40 exact h
    41 loopless := ⟨fun vertex ↦ by
    42 simp [code.loopless]⟩
    43
    44/-- Vertex count followed by the row-major adjacency matrix. -/
    45def GraphCode.bits {n : ℕ} (code : GraphCode n) : BitString :=
    46 n :: List.ofFn fun rank : Fin (n * n) ↦
    47 let vertex := finProdFinEquiv.symm rank
    48 bitWord (code.adjacent vertex.1 vertex.2)
    49
    50/-- Decode the first nn output bits as a vertex set. -/
    51def decodeVertexSet (n : ℕ) (bits : BitString) : Finset (Fin n) :=
    52 Finset.univ.filter fun vertex ↦ bits[vertex.1]? = some 1
    53
    54/-- A polynomial-time executable approximation for triangle-free Max Independent Set. -/
    55structure TriangleFreeMISApproximation (ε : ℝ) where
    56 program : PolytimeProgram
    57 correctness : ∀ (n : ℕ) (code : GraphCode n),
    58 code.graph.CliqueFree 3 →
    59 let set := decodeVertexSet n (program.output code.bits)
    60 code.graph.IsIndepSet set ∧
    61 (code.graph.indepNum : ℝ) ≤
    62 Real.rpow n ((1 : ℝ) / 2 - ε) * set.card
    63
    64end Lax47.Complexity
    65

    Builds on

    Used by

    From Mathlib

    Community review

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

    0 comments

    Loading discussion…