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

theorem DescriptiveComplexity.partSum_min {A : Type} {ILe : A → A → Prop} {IItem S : A → Prop} {w : A → ℕ} (hlin : IsLinOrd ILe) (hS : ∀ (i : A), S i → IItem i) {i : A} (hi : MinPos ILe IItem i) : PartSum ILe S w i = if S i then w i else 0

At the first item, the running total is that item's contribution.

theorem DescriptiveComplexity.partSum_succ {A : Type} [Finite A] {ILe : A → A → Prop} {IItem S : A → Prop} {w : A → ℕ} (hlin : IsLinOrd ILe) (hS : ∀ (i : A), S i → IItem i) {h i : A} (hsucc : SuccPos ILe IItem h i) : PartSum ILe S w i = PartSum ILe S w h + if S i then w i else 0

Each step of the walk adds one item's contribution.

theorem DescriptiveComplexity.partSum_le {A : Type} [Finite A] {ILe : A → A → Prop} {S : A → Prop} {w : A → ℕ} (i : A) : PartSum ILe S w i ≤ ∑ᶠ (j : A) (_ : j ∈ {j : A | S j}), w j

A running total never exceeds the total.

theorem DescriptiveComplexity.partSum_max {A : Type} {ILe : A → A → Prop} {IItem S : A → Prop} {w : A → ℕ} (hS : ∀ (i : A), S i → IItem i) {i : A} (hi : MaxPos ILe IItem i) : PartSum ILe S w i = ∑ᶠ (j : A) (_ : j ∈ {j : A | S j}), w j

At the last item, the running total is the total.

theorem DescriptiveComplexity.xor3_iff (x y z : Prop) : Xor x (Xor y z) ↔ (x ↔ (y ↔ z))

The parity of three bits, as an iterated equivalence.

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)

theorem DescriptiveComplexity.binNum_chainAdd {A P : Type} (PLe : P → P → Prop) (PPosn : P → Prop) (S : A → Prop) (wt : A → P → Prop) (i : A) : binNum PLe PPosn (ChainAdd S wt i) = if S i then binNum PLe PPosn (wt i) else 0

An item contributes its weight, or nothing.

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.