Partition is in NP

The certificate guesses the split and two ripple-carry walks, one along the chosen items and one along the items left out, and asks that they end on the same number. Two things differ from Knapsack (DescriptiveComplexity.Problems.Knapsack.Membership):

• the walks run on the wide positions of DescriptiveComplexity.Numbers.Wide – pairs (x, p) with p a position of the instance – because each half is total / 2, which the instance's own positions need not be able to write. A wide position is therefore two variables, guarded by posn p alone, and the step from one to the next is either inside a block or from the top of one block to the bottom of the next (DescriptiveComplexity.succPos_wide);
• there is no target to reach and no number to guess: the two walks are simply required to agree at the last item, and with no items at all both sums are empty, so Knapsack's degenerate clause has no counterpart here.

The two walks are the same clauses read twice, once for the side b = true (the chosen items) and once for b = false (the others), so the whole clause family is written as a function of b, and so is the semantic argument, which is DescriptiveComplexity.chain_sound and DescriptiveComplexity.exists_chain (DescriptiveComplexity.Problems.Knapsack.Chain) applied twice.

inductive DescriptiveComplexity.PIdx : Type

The relation variables of the certificate: the chosen items, and the running totals and carries of the two walks.

• sel : PIdx

  The chosen items.

• ps (b : Bool) : PIdx

  The running total of the walk on the side b.

• cy (b : Bool) : PIdx

  The carries of the walk on the side b.

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqPIdx : DecidableEq PIdx

Equations

• DescriptiveComplexity.instDecidableEqPIdx = DescriptiveComplexity.instDecidableEqPIdx.decEq

def DescriptiveComplexity.instDecidableEqPIdx.decEq (x✝ x✝¹ : PIdx) : Decidable (x✝ = x✝¹)

Equations

• DescriptiveComplexity.instDecidableEqPIdx.decEq DescriptiveComplexity.PIdx.sel DescriptiveComplexity.PIdx.sel = isTrue ⋯
• DescriptiveComplexity.instDecidableEqPIdx.decEq DescriptiveComplexity.PIdx.sel (DescriptiveComplexity.PIdx.ps b) = isFalse ⋯
• DescriptiveComplexity.instDecidableEqPIdx.decEq DescriptiveComplexity.PIdx.sel (DescriptiveComplexity.PIdx.cy b) = isFalse ⋯
• DescriptiveComplexity.instDecidableEqPIdx.decEq (DescriptiveComplexity.PIdx.ps b) DescriptiveComplexity.PIdx.sel = isFalse ⋯
• DescriptiveComplexity.instDecidableEqPIdx.decEq (DescriptiveComplexity.PIdx.ps a) (DescriptiveComplexity.PIdx.ps b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• DescriptiveComplexity.instDecidableEqPIdx.decEq (DescriptiveComplexity.PIdx.ps b) (DescriptiveComplexity.PIdx.cy b_1) = isFalse ⋯
• DescriptiveComplexity.instDecidableEqPIdx.decEq (DescriptiveComplexity.PIdx.cy b) DescriptiveComplexity.PIdx.sel = isFalse ⋯
• DescriptiveComplexity.instDecidableEqPIdx.decEq (DescriptiveComplexity.PIdx.cy b) (DescriptiveComplexity.PIdx.ps b_1) = isFalse ⋯
• DescriptiveComplexity.instDecidableEqPIdx.decEq (DescriptiveComplexity.PIdx.cy a) (DescriptiveComplexity.PIdx.cy b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DescriptiveComplexity.instFintypePIdx : Fintype PIdx

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.partitionGuessBlock : SOBlock

The single existential block of the Σ₁ definition of Partition: the chosen items (unary), and, for each side, the running totals and the carries (ternary: an item and a wide position, itself a pair).

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.ptSelRel : partitionGuessBlock.lang.Relations 1

The symbol of the chosen-items relation variable.

Equations

• DescriptiveComplexity.ptSelRel = ⟨DescriptiveComplexity.PIdx.sel, DescriptiveComplexity.ptSelRel._proof_1⟩

def DescriptiveComplexity.ptPSRel (b : Bool) : partitionGuessBlock.lang.Relations 3

The symbol of the running total of the side b.

Equations

• DescriptiveComplexity.ptPSRel b = ⟨DescriptiveComplexity.PIdx.ps b, ⋯⟩

def DescriptiveComplexity.ptCyRel (b : Bool) : partitionGuessBlock.lang.Relations 3

The symbol of the carries of the side b.

Equations

• DescriptiveComplexity.ptCyRel b = ⟨DescriptiveComplexity.PIdx.cy b, ⋯⟩

@[reducible, inline]

abbrev DescriptiveComplexity.ptSOLang : FirstOrder.Language

The vocabulary of the kernel.

Equations

• DescriptiveComplexity.ptSOLang = FirstOrder.Language.binWeights.sum DescriptiveComplexity.partitionGuessBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.ptItemSym : ptSOLang.Relations 1

The item symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.ptItemSym = Sum.inl FirstOrder.Language.bwItem

@[reducible, inline]

abbrev DescriptiveComplexity.ptPosnSym : ptSOLang.Relations 1

The position symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.ptPosnSym = Sum.inl FirstOrder.Language.bwPosn

@[reducible, inline]

abbrev DescriptiveComplexity.ptBitSym : ptSOLang.Relations 2

The bit symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.ptBitSym = Sum.inl FirstOrder.Language.bwBit

@[reducible, inline]

abbrev DescriptiveComplexity.ptLeSym : ptSOLang.Relations 2

The order symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.ptLeSym = Sum.inl FirstOrder.Language.bwLe

@[reducible, inline]

abbrev DescriptiveComplexity.ptSelSym : ptSOLang.Relations 1

The chosen-items symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.ptSelSym = Sum.inr DescriptiveComplexity.ptSelRel

@[reducible, inline]

abbrev DescriptiveComplexity.ptPSSym (b : Bool) : ptSOLang.Relations 3

The running-total symbol of the side b in the kernel's vocabulary.

Equations

• DescriptiveComplexity.ptPSSym b = Sum.inr (DescriptiveComplexity.ptPSRel b)

@[reducible, inline]

abbrev DescriptiveComplexity.ptCySym (b : Bool) : ptSOLang.Relations 3

The carry symbol of the side b in the kernel's vocabulary.

Equations

• DescriptiveComplexity.ptCySym b = Sum.inr (DescriptiveComplexity.ptCyRel b)

Formula builders

def DescriptiveComplexity.ptItemF {α : Type} (x : α) : ptSOLang.Formula α

x is an item, as a formula.

Equations

• DescriptiveComplexity.ptItemF x = DescriptiveComplexity.ptItemSym.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.ptPosnF {α : Type} (x : α) : ptSOLang.Formula α

x is a bit position, as a formula.

Equations

• DescriptiveComplexity.ptPosnF x = DescriptiveComplexity.ptPosnSym.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.ptBitF {α : Type} (i p : α) : ptSOLang.Formula α

The weight of i has bit 1 at p, as a formula.

Equations

• DescriptiveComplexity.ptBitF i p = DescriptiveComplexity.ptBitSym.formula₂ (FirstOrder.Language.var i) (FirstOrder.Language.var p)

def DescriptiveComplexity.ptLeF {α : Type} (x y : α) : ptSOLang.Formula α

x ≤ y, as a formula.

Equations

• DescriptiveComplexity.ptLeF x y = DescriptiveComplexity.ptLeSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

def DescriptiveComplexity.ptEqF {α : Type} (x y : α) : ptSOLang.Formula α

x = y, as a formula.

Equations

• DescriptiveComplexity.ptEqF x y = (FirstOrder.Language.var x).equal (FirstOrder.Language.var y)

def DescriptiveComplexity.ptSelF {α : Type} (x : α) : ptSOLang.Formula α

x is chosen, as a formula.

Equations

• DescriptiveComplexity.ptSelF x = DescriptiveComplexity.ptSelSym.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.ptPSF {α : Type} (b : Bool) (i x p : α) : ptSOLang.Formula α

Bit (x, p) of the running total of the side b at i, as a formula.

Equations

• DescriptiveComplexity.ptPSF b i x p = (DescriptiveComplexity.ptPSSym b).formula ![FirstOrder.Language.var i, FirstOrder.Language.var x, FirstOrder.Language.var p]

def DescriptiveComplexity.ptCyF {α : Type} (b : Bool) (i x p : α) : ptSOLang.Formula α

The carry at (x, p) of the step appending i, as a formula.

Equations

• DescriptiveComplexity.ptCyF b i x p = (DescriptiveComplexity.ptCySym b).formula ![FirstOrder.Language.var i, FirstOrder.Language.var x, FirstOrder.Language.var p]

def DescriptiveComplexity.ptSideF {α : Type} (b : Bool) (i : α) : ptSOLang.Formula α

i belongs to the side b, as a formula.

Equations

• DescriptiveComplexity.ptSideF true i = DescriptiveComplexity.ptSelF i
• DescriptiveComplexity.ptSideF false i = DescriptiveComplexity.ptItemF i ⊓ FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.ptSelF i)

noncomputable def DescriptiveComplexity.ptBotF {α : Type} (x : α) : ptSOLang.Formula α

x is a minimum of the order, as a formula.

Equations

• DescriptiveComplexity.ptBotF x = FirstOrder.Language.Formula.iAlls Unit (DescriptiveComplexity.ptLeF (Sum.inl x) (Sum.inr ()))

noncomputable def DescriptiveComplexity.ptTopF {α : Type} (x : α) : ptSOLang.Formula α

x is a maximum of the order, as a formula.

Equations

• DescriptiveComplexity.ptTopF x = FirstOrder.Language.Formula.iAlls Unit (DescriptiveComplexity.ptLeF (Sum.inr ()) (Sum.inl x))

noncomputable def DescriptiveComplexity.ptAddF {α : Type} (b : Bool) (i x p : α) : ptSOLang.Formula α

The bit that the item i contributes at the wide position (x, p): its weight's bit, in the lowest block, if it is on the side b.

Equations

• DescriptiveComplexity.ptAddF b i x p = DescriptiveComplexity.ptSideF b i ⊓ (DescriptiveComplexity.ptBotF x ⊓ DescriptiveComplexity.ptBitF i p)

def DescriptiveComplexity.ptXor3F {α : Type} (x y z : ptSOLang.Formula α) : ptSOLang.Formula α

The exclusive or of three formulas, as x ↔ (y ↔ z).

Equations

• DescriptiveComplexity.ptXor3F x y z = x.iff (y.iff z)

def DescriptiveComplexity.ptMaj3F {α : Type} (x y z : ptSOLang.Formula α) : ptSOLang.Formula α

The majority of three formulas.

Equations

• DescriptiveComplexity.ptMaj3F x y z = x ⊓ y ⊔ (x ⊓ z ⊔ y ⊓ z)

noncomputable def DescriptiveComplexity.ptMinItemF {α : Type} (i : α) : ptSOLang.Formula α

i is the first item, as a formula.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.ptMaxItemF {α : Type} (i : α) : ptSOLang.Formula α

i is the last item, as a formula.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.ptSuccItemF {α : Type} (i j : α) : ptSOLang.Formula α

j is the item right after i, as a formula.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.ptMinPosnF {α : Type} (p : α) : ptSOLang.Formula α

p is the lowest position, as a formula.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.ptMaxPosnF {α : Type} (p : α) : ptSOLang.Formula α

p is the highest position, as a formula.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.ptSuccPosnF {α : Type} (p q : α) : ptSOLang.Formula α

q is the position right above p, as a formula.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.ptSuccAllF {α : Type} (x y : α) : ptSOLang.Formula α

y is the element right after x in the whole universe, as a formula.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.ptMinWideF {α : Type} (x p : α) : ptSOLang.Formula α

(x, p) is the lowest wide position, as a formula.

Equations

• DescriptiveComplexity.ptMinWideF x p = DescriptiveComplexity.ptBotF x ⊓ DescriptiveComplexity.ptMinPosnF p

noncomputable def DescriptiveComplexity.ptMaxWideF {α : Type} (x p : α) : ptSOLang.Formula α

(x, p) is the highest wide position, as a formula.

Equations

• DescriptiveComplexity.ptMaxWideF x p = DescriptiveComplexity.ptTopF x ⊓ DescriptiveComplexity.ptMaxPosnF p

noncomputable def DescriptiveComplexity.ptSuccWideF {α : Type} (x p y q : α) : ptSOLang.Formula α

(y, q) is the wide position right above (x, p), as a formula: a step inside a block, or from the top of one block to the bottom of the next.

Equations

• One or more equations did not get rendered due to their size.

The clauses

noncomputable def DescriptiveComplexity.partitionKernel : ptSOLang.Sentence

The first-order kernel of the Σ₁ definition of Partition.

Equations

• One or more equations did not get rendered due to their size.

Realization

def DescriptiveComplexity.PSel {A : Type} (ρ : partitionGuessBlock.Assignment A) (i : A) : Prop

The chosen items, read off an assignment of the block.

Equations

• DescriptiveComplexity.PSel ρ i = ρ DescriptiveComplexity.PIdx.sel ![i]

def DescriptiveComplexity.PPS {A : Type} (ρ : partitionGuessBlock.Assignment A) (b : Bool) (i : A) (u : A × A) : Prop

The running total of the side b, read off an assignment of the block.

Equations

• DescriptiveComplexity.PPS ρ b i u = ρ (DescriptiveComplexity.PIdx.ps b) ![i, u.1, u.2]

def DescriptiveComplexity.PCy {A : Type} (ρ : partitionGuessBlock.Assignment A) (b : Bool) (i : A) (u : A × A) : Prop

The carries of the side b, read off an assignment of the block.

Equations

• DescriptiveComplexity.PCy ρ b i u = ρ (DescriptiveComplexity.PIdx.cy b) ![i, u.1, u.2]

def DescriptiveComplexity.PSide {A : Type} [FirstOrder.Language.binWeights.Structure A] (ρ : partitionGuessBlock.Assignment A) (b : Bool) (i : A) : Prop

The items of the side b: the chosen ones, or the others.

Equations

• DescriptiveComplexity.PSide ρ true i = DescriptiveComplexity.PSel ρ i
• DescriptiveComplexity.PSide ρ false i = (DescriptiveComplexity.BWItem i ∧ ¬DescriptiveComplexity.PSel ρ i)

def DescriptiveComplexity.PWt {A : Type} [FirstOrder.Language.binWeights.Structure A] (i : A) (u : A × A) : Prop

The bit an item contributes at a wide position: its own bit, in the lowest block. The minimality of the block is written with the Unit-indexed quantifier the kernel's ∀ produces; DescriptiveComplexity.pWt_iff reads it back.

Equations

• DescriptiveComplexity.PWt i u = ((∀ (y : Unit → A), DescriptiveComplexity.BWLe u.1 (y ())) ∧ DescriptiveComplexity.BWBit i u.2)

theorem DescriptiveComplexity.pWt_iff {A : Type} [FirstOrder.Language.binWeights.Structure A] {i : A} {u : A × A} : PWt i u ↔ (∀ (y : A), BWLe u.1 y) ∧ BWBit i u.2

Membership

theorem DescriptiveComplexity.partition_sigmaSODefinable : SigmaSODefinable 1 Partition

Partition is Σ₁-definable: guess the split and the two ripple-carry walks, one along the chosen items and one along the others, and check first-order that they end on the same number. Since NP is defined as Σ₁-definability, this is the membership half of the NP-completeness of Partition.