Adding up binary weights along the item order

The certificate of a binary-weighted problem walks the items in order and carries the running total: PS i is the total over the chosen items up to i, and Cy i the carries of the step that appends i. The conditions the walk must satisfy – every bit the exclusive or of the three inputs, every carry their majority, no carry into the lowest position, none out of the highest – are DescriptiveComplexity.IsChain, and this file proves the two statements the Σ₁ definitions need:

• DescriptiveComplexity.chain_sound: a walk really does compute the running totals, so at the last item it computes the total;
• DescriptiveComplexity.exists_chain: whenever the total fits in the positions, a walk exists – the certificate a yes-instance offers.

Nothing here mentions a vocabulary: the items, their order and the bit positions are all parameters, because the clients need different ones.

• Knapsack walks the instance's own positions, its running totals being bounded by the target, which is written there;
• Partition cannot – each half is total / 2, which may exceed every number the instance can write – so it walks the wider positions of DescriptiveComplexity.Numbers.Wide;
• 0-1 integer programming walks the same positions as Knapsack but needs one walk per row, so its guessed relations carry a row argument and each slice is a walk of its own.

Partial sums along the item order

noncomputable def DescriptiveComplexity.PartSum {A : Type} (Le : A → A → Prop) (S : A → Prop) (w : A → ℕ) (i : A) : ℕ

The running total of the weights w over the chosen items up to i.

Equations

• DescriptiveComplexity.PartSum Le S w i = ∑ᶠ (j : A) (_ : j ∈ {j : A | S j ∧ Le j i}), w j

Walks along the item order

def DescriptiveComplexity.ChainAdd {A P : Type} (S : A → Prop) (wt : A → P → Prop) (i : A) (p : P) : Prop

The bit that an item contributes at a position: its own bit, if chosen.

Equations

• DescriptiveComplexity.ChainAdd S wt i p = (S i ∧ wt i p)

def DescriptiveComplexity.IsChain {A P : Type} (Le : A → A → Prop) (Item : A → Prop) (PLe : P → P → Prop) (PPosn : P → Prop) (S : A → Prop) (wt PS Cy : A → P → Prop) : Prop

A ripple-carry walk along the items: PS i is the running total up to i and Cy i the carries of the step appending i.

Equations

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

theorem DescriptiveComplexity.chain_sound {A : Type} [Finite A] {ILe : A → A → Prop} {IItem : A → Prop} {P : Type} [Finite P] {PLe : P → P → Prop} {PPosn : P → Prop} {S : A → Prop} {wt PS Cy : A → P → Prop} (hlin : IsLinOrd ILe) (hPlin : IsLinOrd PLe) (hS : ∀ (i : A), S i → IItem i) (hchain : IsChain ILe IItem PLe PPosn S wt PS Cy) (i : A) : IItem i → binNum PLe PPosn (PS i) = PartSum ILe S (fun (j : A) => binNum PLe PPosn (wt j)) i

A walk computes the running totals.

theorem DescriptiveComplexity.exists_chain {A : Type} [Finite A] {ILe : A → A → Prop} {IItem : A → Prop} {P : Type} [Finite P] {PLe : P → P → Prop} {PPosn : P → Prop} {S : A → Prop} {wt : A → P → Prop} (hlin : IsLinOrd ILe) (hPlin : IsLinOrd PLe) (hS : ∀ (i : A), S i → IItem i) (hbound : ∑ᶠ (j : A) (_ : j ∈ {j : A | S j}), binNum PLe PPosn (wt j) < 2 ^ {p : P | PPosn p}.ncard) : ∃ (PS : A → P → Prop) (Cy : A → P → Prop), IsChain ILe IItem PLe PPosn S wt PS Cy

A walk exists whenever the total fits in the positions: this is the certificate a yes-instance offers.

A walk is determined by the chosen items

What a definition that counts certificates needs: the conditions of a walk read the running totals only at items and positions, and the carries only at the items that have a predecessor, and there they are forced.

theorem DescriptiveComplexity.maj_congr {x y z x' y' z' : Prop} (hx : x ↔ x') (hy : y ↔ y') (hz : z ↔ z') : maj x y z ↔ maj x' y' z'

theorem DescriptiveComplexity.IsChain.congr {A : Type} {ILe : A → A → Prop} {IItem : A → Prop} {P : Type} {PLe : P → P → Prop} {PPosn : P → Prop} {S : A → Prop} {wt PS Cy PS' Cy' : A → P → Prop} (hchain : IsChain ILe IItem PLe PPosn S wt PS Cy) (hPS : ∀ (i : A) (p : P), IItem i → PPosn p → (PS i p ↔ PS' i p)) (hCy : ∀ (i j : A) (p : P), SuccPos ILe IItem i j → PPosn p → (Cy j p ↔ Cy' j p)) : IsChain ILe IItem PLe PPosn S wt PS' Cy'

The conditions of a walk only read the totals at items and positions, and the carries at the items that have a predecessor.

theorem DescriptiveComplexity.isChain_agree {A : Type} [Finite A] {ILe : A → A → Prop} {IItem : A → Prop} {P : Type} [Finite P] {PLe : P → P → Prop} {PPosn : P → Prop} {S : A → Prop} {wt PS Cy PS' Cy' : A → P → Prop} (hlin : IsLinOrd ILe) (hPlin : IsLinOrd PLe) (hS : ∀ (i : A), S i → IItem i) (h : IsChain ILe IItem PLe PPosn S wt PS Cy) (h' : IsChain ILe IItem PLe PPosn S wt PS' Cy') : (∀ (i : A) (p : P), IItem i → PPosn p → (PS i p ↔ PS' i p)) ∧ ∀ (i j : A) (p : P), SuccPos ILe IItem i j → PPosn p → (Cy j p ↔ Cy' j p)

Two walks of the same chosen items agree, wherever the conditions of a walk read them: the running totals are the partial sums, and each carry is the majority of three values already known.