Numbers written in base B on a relation-ordered index set

DescriptiveComplexity.binNum writes a number in base two, one bit per position. The reduction that proves Knapsack NP-hard needs the same reading in a larger base: the ground elements of a set system become blocks of bits, and the number of sets covering an element becomes the digit of that block. Choosing the base above the number of sets is what stops carries from crossing a block boundary, and then a sum of weights equals the target exactly when every element is covered once – which is uniqueness of base-B expansions, DescriptiveComplexity.digitNum_inj here.

The development mirrors the binary one: a peeling lemma for the lowest block (DescriptiveComplexity.digitNum_peel_min) and an induction on the number of blocks. DescriptiveComplexity.binNum is the special case of base two with digits 0 and 1 (DescriptiveComplexity.binNum_eq_digitNum).

noncomputable def DescriptiveComplexity.digitNum {A : Type} (Le : A → A → Prop) (Blk : A → Prop) (B : ℕ) (c : A → ℕ) : ℕ

The number written by the digits c in base B, the place values being fixed by the rank of a block among the blocks.

Equations

• DescriptiveComplexity.digitNum Le Blk B c = ∑ᶠ (e : A) (_ : e ∈ {e : A | Blk e}), c e * B ^ DescriptiveComplexity.bitRank Le Blk e

theorem DescriptiveComplexity.digitNum_congr_on {A : Type} {Le : A → A → Prop} {Blk : A → Prop} {B : ℕ} {c c' : A → ℕ} (h : ∀ (e : A), Blk e → c e = c' e) : digitNum Le Blk B c = digitNum Le Blk B c'

theorem DescriptiveComplexity.digitNum_mul_left {A : Type} [Finite A] {Le : A → A → Prop} {Blk : A → Prop} {B : ℕ} (k : ℕ) (c : A → ℕ) : (digitNum Le Blk B fun (e : A) => k * c e) = k * digitNum Le Blk B c

Scaling every digit scales the value. A gadget whose block totals are all even therefore weighs twice the number obtained by halving each digit, which is how a reduction can write half of a total it cannot compute.

theorem DescriptiveComplexity.digitNum_peel_min {A : Type} [Finite A] {Le : A → A → Prop} {Blk : A → Prop} {B : ℕ} {c : A → ℕ} {e₀ : A} (hlin : IsLinOrd Le) (h₀ : Blk e₀) (hmin : ∀ (q : A), Blk q → Le e₀ q) : digitNum Le Blk B c = c e₀ + B * digitNum Le (fun (q : A) => Blk q ∧ q ≠ e₀) B c

Peeling the lowest block: the value is the lowest digit plus B times the value of the rest.

theorem DescriptiveComplexity.digitNum_inj {A : Type} [Finite A] {Le : A → A → Prop} {B : ℕ} (hlin : IsLinOrd Le) (hB : 0 < B) (n : ℕ) (Blk : A → Prop) : {e : A | Blk e}.ncard = n → ∀ (c d : A → ℕ), (∀ (e : A), c e < B) → (∀ (e : A), d e < B) → digitNum Le Blk B c = digitNum Le Blk B d → ∀ (e : A), Blk e → c e = d e

Uniqueness of base-B expansions: digits below the base are determined by the number they write.

theorem DescriptiveComplexity.binNum_eq_digitNum {A : Type} [Finite A] {Le : A → A → Prop} {Posn b : A → Prop} : binNum Le Posn b = digitNum Le Posn 2 fun (p : A) => if b p then 1 else 0

Base two with digits 0 and 1 is the binary reading.