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.ptSelF {α : Type} (x : α) : ptSOLang.Formula α

x is chosen, as a formula.

Equations

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

The clauses

Realization

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.