Lax Lean Archive

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

Binary branch decompositions of finite sets

Lax183560.BranchDecompositions · concepts/Lax183560/BranchDecompositions.lean · lax-183560

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

    A branch decomposition of a finite set is an unrooted tree of maximum degree three whose leaves are in bijection with the set. Each edge determines a cut by separating the leaves into two parts.

    For symmetric cut functions, a decomposition can be represented by a binary tree obtained by rooting it at an edge. Each subtree determines one side of a cut. The root determines the cut with an empty opposite side, which has value zero for the cut functions used here.

    Concept map
    1 concept; 2 descendants hidden
    100%
    DefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Finite
    2import Mathlib.LinearAlgebra.Matrix.Rank
    3import Mathlib.Data.ZMod.Basic
    4import Mathlib.Order.Lattice.Nat
    5
    6/-!
    7---
    8title: Binary branch decompositions of finite sets
    9type: definition
    10---
    11A branch decomposition of a finite set is an unrooted tree of maximum degree
    12three whose leaves are in bijection with the set. Each edge determines a cut
    13by separating the leaves into two parts.
    14
    15For symmetric cut functions, a decomposition can be represented by a binary
    16tree obtained by rooting it at an edge. Each subtree determines one side of
    17a cut. The root determines the cut with an empty opposite side, which has
    18value zero for the cut functions used here.
    19-/
    20
    21namespace Lax183560.BranchDecompositions
    22
    23inductive BinaryTree (α : Type) where
    24 | leaf : α → BinaryTree α
    25 | fork : BinaryTree α → BinaryTree α → BinaryTree α
    26
    27/-- Leaves with multiplicity, in left-to-right order. -/
    28def BinaryTree.leaves {α : Type} : BinaryTree α → List α
    29 | .leaf a => [a]
    30 | .fork left right => left.leaves ++ right.leaves
    31
    32/-- A valid branch tree contains each element of the ground set once. -/
    33def BinaryTree.Valid {α : Type} [DecidableEq α]
    34 (t : BinaryTree α) (ground : Finset α) : Prop :=
    35 t.leaves.Nodup ∧ t.leaves.toFinset = ground
    36
    37/-- Maximum cut value among the cuts at the nodes of a branch tree. -/
    38def BinaryTree.cutWidth {α : Type} [DecidableEq α]
    39 (measure : Finset α → ℕ) : BinaryTree α → ℕ
    40 | .leaf a => measure {a}
    41 | .fork left right =>
    42 max (measure ((left.leaves ++ right.leaves).toFinset))
    43 (max (left.cutWidth measure) (right.cutWidth measure))
    44
    45end Lax183560.BranchDecompositions
    46
    Builds on

    none

    Used by
    From Mathlib

    Discussion

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

    Loading discussion…