Wide numbers: sums that no longer fit in the instance's own positions

A binary-weighted instance carries a set of bit positions, and each weight is a number below 2 ^ n for n the number of positions (DescriptiveComplexity.binNum_lt_two_pow). A sum of such weights need not be: m items of n bits reach m · 2 ^ n. For Knapsack that costs nothing – the sum is required to equal the target, which is itself an n-bit number, so every running total along the way is below 2 ^ n. For Partition it is fatal: each half is total / 2, which may well exceed every number the instance can write, so a certificate carrying the running totals on the positions would not exist even for yes-instances.

This file widens the representation. Bit positions become pairs, ordered with the first coordinate major:

• DescriptiveComplexity.WidePosn: the pairs whose second coordinate is a position – |A| · n of them, enough room for any sum of the instance's weights (DescriptiveComplexity.finsum_binNum_lt_wide);
• DescriptiveComplexity.wideLe: the lexicographic order, first coordinate major, which makes the pairs (⊥, p) the lowest n positions, with the same ranks as the positions p themselves (DescriptiveComplexity.bitRank_wide), so that a weight is read unchanged in the wide representation (DescriptiveComplexity.binNum_wide).

Everything else – the ripple-carry lemmas of DescriptiveComplexity.Numbers.BinRel – applies verbatim at the pair type, being stated for an arbitrary relation on an arbitrary finite type. What the first-order layer needs on top is the translation of the walk along the wide positions into two coordinates, which is DescriptiveComplexity.minPos_wide, DescriptiveComplexity.maxPos_wide and DescriptiveComplexity.succPos_wide.

def DescriptiveComplexity.WidePosn {A : Type} (Posn : A → Prop) : A × A → Prop

The positions of the wide representation: pairs whose second coordinate is a position of the instance.

Equations

• DescriptiveComplexity.WidePosn Posn u = Posn u.2

def DescriptiveComplexity.wideLe {A : Type} (Le : A → A → Prop) : A × A → A × A → Prop

The order of the wide representation: lexicographic, first coordinate major.

Equations

• DescriptiveComplexity.wideLe Le u v = (Le u.1 v.1 ∧ u.1 ≠ v.1 ∨ u.1 = v.1 ∧ Le u.2 v.2)

theorem DescriptiveComplexity.isLinOrd_wideLe {A : Type} {Le : A → A → Prop} (hlin : IsLinOrd Le) : IsLinOrd (wideLe Le)

The wide order is a linear order.

theorem DescriptiveComplexity.bitRank_wide {A : Type} {Le : A → A → Prop} {Posn : A → Prop} (hlin : IsLinOrd Le) {a₀ : A} (h₀ : ∀ (x : A), Le a₀ x) (p : A) : bitRank (wideLe Le) (WidePosn Posn) (a₀, p) = bitRank Le Posn p

The instance's positions sit at the bottom of the wide ones, with unchanged ranks: a weight means the same number read either way.

theorem DescriptiveComplexity.binNum_wide {A : Type} {Le : A → A → Prop} {Posn : A → Prop} (hlin : IsLinOrd Le) {a₀ : A} (h₀ : ∀ (x : A), Le a₀ x) (b : A → Prop) : (binNum (wideLe Le) (WidePosn Posn) fun (u : A × A) => u.1 = a₀ ∧ b u.2) = binNum Le Posn b

A weight is the same number in the wide representation.

theorem DescriptiveComplexity.binNum_wide_bot {A : Type} {Le : A → A → Prop} {Posn : A → Prop} (hlin : IsLinOrd Le) {a₀ : A} (h₀ : ∀ (x : A), Le a₀ x) (b : A → Prop) : (binNum (wideLe Le) (WidePosn Posn) fun (u : A × A) => (∀ (y : A), Le u.1 y) ∧ b u.2) = binNum Le Posn b

The same, with the bottom block named by minimality rather than by a constant: this is the shape a first-order kernel produces, since a formula can only say “this block is minimal”.

theorem DescriptiveComplexity.ncard_widePosn {A : Type} {Posn : A → Prop} : {u : A × A | WidePosn Posn u}.ncard = Nat.card A * {p : A | Posn p}.ncard

There are |A| times as many wide positions as positions.

Walking the wide positions

theorem DescriptiveComplexity.minPos_wide {A : Type} {Le : A → A → Prop} {Posn : A → Prop} {x p : A} (hlin : IsLinOrd Le) : MinPos (wideLe Le) (WidePosn Posn) (x, p) ↔ (∀ (y : A), Le x y) ∧ MinPos Le Posn p

The lowest wide position is the lowest position of the lowest block.

theorem DescriptiveComplexity.maxPos_wide {A : Type} {Le : A → A → Prop} {Posn : A → Prop} {x p : A} (hlin : IsLinOrd Le) : MaxPos (wideLe Le) (WidePosn Posn) (x, p) ↔ (∀ (y : A), Le y x) ∧ MaxPos Le Posn p

The highest wide position is the highest position of the highest block.

theorem DescriptiveComplexity.succPos_wide {A : Type} {Le : A → A → Prop} {Posn : A → Prop} {x p y q : A} (hlin : IsLinOrd Le) : SuccPos (wideLe Le) (WidePosn Posn) (x, p) (y, q) ↔ x = y ∧ SuccPos Le Posn p q ∨ SuccPos Le (fun (x : A) => True) x y ∧ MaxPos Le Posn p ∧ MinPos Le Posn q

Stepping along the wide positions: inside a block, or from the top of one block to the bottom of the next.

The room the wide positions buy

theorem DescriptiveComplexity.finsum_lt_two_pow_mul {A : Type} [Finite A] {n : ℕ} (w : A → ℕ) (S : Set A) (hw : ∀ (i : A), w i < 2 ^ n) : ∑ᶠ (i : A) (_ : i ∈ S), w i < 2 ^ (Nat.card A * n)

A sum of numbers below 2 ^ n, over a universe of m elements, is below 2 ^ (m * n).

theorem DescriptiveComplexity.finsum_binNum_lt_wide {A : Type} [Finite A] {Le : A → A → Prop} {Posn : A → Prop} (hlin : IsLinOrd Le) (bits : A → A → Prop) (S : Set A) : ∑ᶠ (i : A) (_ : i ∈ S), binNum Le Posn (bits i) < 2 ^ {u : A × A | WidePosn Posn u}.ncard

The wide positions are wide enough: any sum of the instance's weights fits in them.