Documentation

DescriptiveComplexity.Numbers.Digits

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).

source
theorem DescriptiveComplexity.finsum_mem_ite_one {ι : Type} [Finite ι] (S : Set ι) (p : ι → Prop) [DecidablePred p] :
(∑ᶠ (i : ι) (_ : i ∈ S), if p i then 1 else 0) = {i : ι | i ∈ S ∧ p i}.ncard

A sum of 0s and 1s counts.

source
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
Instances For
    source
    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'
    source
    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.

    source
    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.

    source
    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.

    source
    theorem DescriptiveComplexity.finsum_coeff_eq_digitNum {A : Type} [Finite A] {Le : A → A → Prop} {Blk sub : A → Prop} {B : ℕ} (k : A → ℕ) (h : ∀ (e : A), sub e → Blk e) :
    ∑ᶠ (e : A) (_ : e ∈ {e : A | sub e}), k e * B ^ bitRank Le Blk e = digitNum Le Blk B fun (e : A) => if sub e then k e else 0

    Weighing blocks: a sum of place values of the blocks satisfying sub, each taken k times, is the number whose digits are k there and 0 elsewhere. A number written by one bit per block, at a height inside the block that may vary from block to block, is of this shape.

    source
    theorem DescriptiveComplexity.finsum_pow_eq_digitNum {A : Type} [Finite A] {Le : A → A → Prop} {Blk sub : A → Prop} {B : ℕ} (h : ∀ (e : A), sub e → Blk e) :
    ∑ᶠ (e : A) (_ : e ∈ {e : A | sub e}), B ^ bitRank Le Blk e = digitNum Le Blk B fun (e : A) => if sub e then 1 else 0

    Selecting blocks: the sum of the place values of the blocks satisfying sub is the number whose digits are 1 there and 0 elsewhere.

    source
    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.

    source
    theorem DescriptiveComplexity.digitNum_finsum {A : Type} [Finite A] {ι : Type} [Finite ι] {Le : A → A → Prop} {Blk : A → Prop} {B : ℕ} (S : Set ι) (c : ι → A → ℕ) :
    ∑ᶠ (i : ι) (_ : i ∈ S), digitNum Le Blk B (c i) = digitNum Le Blk B fun (e : A) => ∑ᶠ (i : ι) (_ : i ∈ S), c i e

    Digit-wise addition: a sum of numbers written on the same blocks is written by the sums of the digits – before any carrying, which is what the bound on the digits then rules out.