Minimum- and maximum-weight multipartite cliques

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

definition

Loading review…

Natural Language Statement

Definition

For fixed $k$ , output the vertices of a minimum- or maximum-weight clique with one vertex from each of $k$ parts of size $n$ . The encoding contains all $k^2$ blocks; the objective sums only the edges with part indices $i<j$ .

Concept map

5 concepts; 1 descendant hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

Show types on hover

1	/-
2	Copyright (c) 2026 Anthropic, PBC. All rights reserved.
3	Released under Apache 2.0 license as described in the file LICENSE.
4	SPDX-License-Identifier: Apache-2.0
5	-/
6	/-
7	Modified for the independent Lax packaging by Édouard Bonnet, 2026.
8	Derived from 3sum-apsp/EndStatement.lean / PaperStatements.lean at upstream commit e1a4e6508154ea59f030480661590a9fe3018011.
9	Changes: Lax module/namespace layout, separated concepts and proofs, archive
10	annotations, and compatibility with the archive Lean/mathlib environment.
11	See NOTICE and README.md in the submission root for provenance and scope.
12	-/
13
14	import Mathlib.Algebra.MvPolynomial.Basic
15	import Mathlib.Analysis.SpecialFunctions.Log.Base
16	import Mathlib.Analysis.SpecialFunctions.Log.Basic
17	import Mathlib.Analysis.SpecialFunctions.Pow.Real
18	import Mathlib.Combinatorics.SimpleGraph.Basic
19	import Mathlib.Data.Finset.Sort
20	import Mathlib.LinearAlgebra.Matrix.Notation
21	import Mathlib.MeasureTheory.Integral.Bochner.Basic
22	import Mathlib.NumberTheory.PrimeCounting
23	import Mathlib.Probability.Independence.Basic
24	import Mathlib.Tactic.DeriveFintype
25	import Lax350013.ZeroWeightClique
26
27	/-!
28	---
29	title: Minimum- and maximum-weight multipartite cliques
30	type: definition
31	---
32	For fixed $k$ , output the vertices of a minimum- or maximum-weight clique with one vertex from each of $k$ parts of size $n$ . The encoding contains all $k^2$ blocks; the objective sums only the edges with part indices $i<j$ .
33	-/
34
35	namespace Lax350013.CliqueOptimization
36
37	open Finset
38
39	/-- The total edge weight of the `k`-clique that has the vertex `v p` in part `p` (Corollary 39):
40	the sum, over the pairs of parts `p < q`, of the weight between `v p` and `v q`. -/
41	def cliqueWeight {k n : ℕ} (w : Fin k → Fin k → Fin n → Fin n → ℤ) (v : Fin k → Fin n) : ℤ :=
42	∑ p : Fin k, ∑ q ∈ Finset.univ.filter (fun q : Fin k => p < q), w p q (v p) (v q)
43
44	/-- Min-Weight `k`-Clique (Corollary 39): accept, and leave in the `p`-th of the `k`
45	output cells (`p = 0, …, k − 1`) the number, below `n`, of the vertex chosen in part `p`, so that
46	the `k` vertices form a `k`-clique of minimum total edge weight. Every such clique is accepted.
47
48	NOTE. The parts have at least one vertex: at `n = 0` there is no clique to output. -/
49	def MinKClique (k : ℕ) : Lax350013.PolynomialTime.Problem where
50	Instance n := {_w : Fin k → Fin k → Fin n → Fin n → ℤ // 1 ≤ n}
51	input w := (Lax350013.ZeroWeightClique.ZeroWeightKClique k).input w.1
52	output {n} w out := ∃ v : Fin k → Fin n, (∀ p : Fin k, out p.val = ((v p).val : ℤ)) ∧
53	∀ v', cliqueWeight w.1 v ≤ cliqueWeight w.1 v'
54
55	/-- Max-Weight `k`-Clique (Corollary 39): the same with maximum total edge weight. -/
56	def MaxKClique (k : ℕ) : Lax350013.PolynomialTime.Problem where
57	Instance n := {_w : Fin k → Fin k → Fin n → Fin n → ℤ // 1 ≤ n}
58	input w := (Lax350013.ZeroWeightClique.ZeroWeightKClique k).input w.1
59	output {n} w out := ∃ v : Fin k → Fin n, (∀ p : Fin k, out p.val = ((v p).val : ℤ)) ∧
60	∀ v', cliqueWeight w.1 v' ≤ cliqueWeight w.1 v
61
62	end Lax350013.CliqueOptimization
63

Builds on

Lax350013.ZeroWeightClique

Used by

Lax350013.WeightedCliqueAlgorithms

From Mathlib

Discussion

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

Loading discussion…

Lax Lean Archive

Minimum- and maximum-weight multipartite cliques

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments