Lax Lean Archive

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

Faster weighted clique algorithms

Lax350013.WeightedCliqueAlgorithms · concepts/Lax350013/WeightedCliqueAlgorithms.lean · lax-350013

proven

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

    Theorem

    Corollary 39 gives deterministic time O(nk−0.0017⌊k/3⌋)O(n^{k-0.0017\lfloor k/3\rfloor}) for zero-weight clique detection and for finding a minimum- or maximum-weight clique, for every fixed k≥3k\geq3 and polynomially bounded integer weights.

    Concept map
    7 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.

    1 minMax proven

    2 zeroWeight proven

    Lean source view on GitHub

    1/-
    2Copyright (c) 2026 Anthropic, PBC. All rights reserved.
    3Released under Apache 2.0 license as described in the file LICENSE.
    4SPDX-License-Identifier: Apache-2.0
    5-/
    6/-
    7Modified for the independent Lax packaging by Édouard Bonnet, 2026.
    8Derived from 3sum-apsp/EndStatement.lean / PaperStatements.lean at upstream commit e1a4e6508154ea59f030480661590a9fe3018011.
    9Changes: Lax module/namespace layout, separated concepts and proofs, archive
    10annotations, and compatibility with the archive Lean/mathlib environment.
    11See NOTICE and README.md in the submission root for provenance and scope.
    12-/
    13
    14import Mathlib.Algebra.MvPolynomial.Basic
    15import Mathlib.Analysis.SpecialFunctions.Log.Base
    16import Mathlib.Analysis.SpecialFunctions.Log.Basic
    17import Mathlib.Analysis.SpecialFunctions.Pow.Real
    18import Mathlib.Combinatorics.SimpleGraph.Basic
    19import Mathlib.Data.Finset.Sort
    20import Mathlib.LinearAlgebra.Matrix.Notation
    21import Mathlib.MeasureTheory.Integral.Bochner.Basic
    22import Mathlib.NumberTheory.PrimeCounting
    23import Mathlib.Probability.Independence.Basic
    24import Mathlib.Tactic.DeriveFintype
    25import Lax350013.ZeroWeightClique
    26import Lax350013.CliqueOptimization
    27import Lax350013.RAMResources
    28
    29/-!
    30---
    31title: Faster weighted clique algorithms
    32type: theorem
    33---
    34Corollary 39 gives deterministic time O(nk−0.0017⌊k/3⌋)O(n^{k-0.0017\lfloor k/3\rfloor}) for zero-weight clique detection and for finding a minimum- or maximum-weight clique, for every fixed k≥3k\geq3 and polynomially bounded integer weights.
    35-/
    36
    37namespace Lax350013.WeightedCliqueAlgorithms
    38
    39open Finset
    40open Lax350013.WordRAM
    41open Lax350013.RAMResources
    42open Lax350013.CliqueOptimization
    43
    44/-- **Corollary 39**, the case of Zero-Weight k-Clique. The paper: "Let k ≥ 3 and ν ≥ 1 be
    45constants. Given a complete k-partite graph with parts of n vertices and integer edge weights of
    46absolute value at most n^ν, deterministic algorithms decide in O(n^{k−ε_T⌊k/3⌋}) time whether some
    47k-clique, with one vertex in each part, has total edge weight zero". -/
    48def Corollary_39_zero : Prop :=
    49 ∀ k : ℕ, 3 ≤ k →
    50 SolvedInTime (Lax350013.ZeroWeightClique.ZeroWeightKClique k) ((k : ℝ) - 0.0017 * ((k / 3 : ℕ) : ℝ)) 0
    51
    52/-- **Corollary 39**, the other two cases: "deterministic algorithms [...] in
    53O(n^{k−ε_T⌊k/3⌋}) time [...] find a k-clique of minimum, or of maximum, total edge weight." The
    54hypotheses are those of `Corollary_39_zero`; `ε_T = 0.0017` (Theorem 19). That the time bound
    55covers finding, and not only deciding, is confirmed by the end of the paper's proof. -/
    56def Corollary_39_min_max : Prop :=
    57 ∀ k : ℕ, 3 ≤ k →
    58 SolvedInTime (MinKClique k) ((k : ℝ) - 0.0017 * ((k / 3 : ℕ) : ℝ)) 0 ∧
    59 SolvedInTime (MaxKClique k) ((k : ℝ) - 0.0017 * ((k / 3 : ℕ) : ℝ)) 0
    60
    61/-- Faster weighted clique algorithms: Corollary 39 zero. -/
    62axiom zeroWeight : Corollary_39_zero
    63
    64
    65/-- Faster weighted clique algorithms: Corollary 39 min max. -/
    66axiom minMax : Corollary_39_min_max
    67
    68end Lax350013.WeightedCliqueAlgorithms
    69
    Show ProofShow Proof
    Builds on
    Used by

    none

    From Mathlib

    Discussion

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

    Loading discussion…