Lax Lean Archive

Partition

Lax799700.Partition · concepts/Lax799700/Partition.lean · lax-799700

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

    PARTITION: can a family of numbers be split into two parts of equal sum? It lives on the vocabulary of Knapsack with the target symbol unused: what a part must match is the weight of the items it leaves out. That is what makes Partition a different problem rather than a special case of Knapsack: the number to reach, half the total, is not part of the instance, so an interpretation cannot compute it, and the classical padding by two extra items is not first-order definable. Hardness comes instead by an ordered first-order reduction from NAE-SAT, whose not-all-equal condition is the two-sided constraint a balanced split imposes. Membership is by an existential second-order definition.

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

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

    1 hasEqualSplit_iso proven

    2 partition_iff proven

    3 partition_NP_complete proven

    Lean source view on GitHub

    1import Mathlib.Algebra.BigOperators.Finprod
    2import Mathlib.ModelTheory.Semantics
    3import Mathlib.ModelTheory.Complexity
    4import Mathlib.Tactic.FinCases
    5import Mathlib.Data.Set.Finite.Lemmas
    6import Mathlib.Data.Fintype.EquivFin
    7import Mathlib.Data.Set.Card
    8import Mathlib.SetTheory.Cardinal.Finite
    9import Mathlib.Logic.Equiv.Prod
    10import Mathlib.ModelTheory.Syntax
    11import Lax799700.Knapsack
    12import Lax904597.Machines
    13import Lax904597.Classes
    14import Lax799700.Problems
    15
    16/-!
    17---
    18title: Partition
    19type: theorem
    20---
    21PARTITION: can a family of numbers be split into two parts of equal sum?
    22It lives on the vocabulary of Knapsack with the target symbol unused:
    23what a part must match is the weight of the items it leaves out. That is
    24what makes Partition a different problem rather than a special case of
    25Knapsack: the number to reach, half the total, is not part of the
    26instance, so an interpretation cannot compute it, and the classical
    27padding by two extra items is not first-order definable. Hardness comes
    28instead by an ordered first-order reduction from NAE-SAT, whose
    29not-all-equal condition is the two-sided constraint a balanced split
    30imposes. Membership is by an existential second-order definition.
    31
    32-/
    33
    34namespace Lax799700.Partition
    35
    36open Lax799700.Knapsack Lax904597.Machines
    37
    38open FirstOrder
    39
    40open Language Structure
    41
    42section Problem
    43
    44variable (A : Type) [binWeights.Structure A]
    45
    46/-- A binary-weighted instance is a yes-instance of Partition when its order is
    47a linear order and some set of items weighs exactly as much as the items it
    48leaves out. -/
    49def HasEqualSplit : Prop :=
    50 Finite A ∧ IsLinOrd (BWLe (A := A)) ∧
    51 ∃ S : A → Prop, (∀ i, S i → BWItem i) ∧
    52 (∑ᶠ i ∈ {i | S i}, BWWeight i) = ∑ᶠ i ∈ {i | BWItem i ∧ ¬S i}, BWWeight i
    53
    54end Problem
    55
    56open Lax904597.Problems Lax904597.Classes Lax799700.Problems
    57
    58/-- The property `HasEqualSplit` is isomorphism-invariant. -/
    59axiom hasEqualSplit_iso : ∀ {A B : Type} [Lax799700.Knapsack.binWeights.Structure A] [Lax799700.Knapsack.binWeights.Structure B],
    60 (A ≃[Lax799700.Knapsack.binWeights] B) → (HasEqualSplit A ↔ HasEqualSplit B)
    61
    62/-- The problem Partition: does the structure satisfy `HasEqualSplit`? -/
    63def Partition : DecisionProblem Lax799700.Knapsack.binWeights :=
    64 DecisionProblem.ofPred HasEqualSplit
    65
    66/-- The yes-instances of Partition are exactly the structures satisfying
    67`HasEqualSplit`. -/
    68axiom partition_iff : ∀ (A : Type) [Lax799700.Knapsack.binWeights.Structure A], Partition A ↔ HasEqualSplit A
    69
    70/-- Partition is NP-complete. -/
    71axiom partition_NP_complete : NP.Complete Partition
    72
    73end Lax799700.Partition
    74
    Show ProofShow 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…