Counting the binary numbers below a bound

A number written in binary on the positions of a linear order is a set of positions (DescriptiveComplexity.binNum). This file counts those sets: over n positions the decoding is a bijection onto the numbers below 2 ^ n (DescriptiveComplexity.binCode_bijective), so the sets of bits whose value is below that of a given set w are exactly as many as the value of w (DescriptiveComplexity.card_binNum_lt).

That is what lets a number in the instance act as a weight in a count: a witness that carries, beside a solution, a number below the weight of that solution is counted once per unit of weight, and “below” is first-order (DescriptiveComplexity.binNum_lt_iff).

noncomputable def DescriptiveComplexity.binCode {A : Type} [Finite A] {Le : A → A → Prop} (hlin : IsLinOrd Le) (b : A → Prop) : Fin (2 ^ Nat.card A)

The decoding of a set of bits, over all the elements as positions, as a number below 2 ^ n.

Equations

• DescriptiveComplexity.binCode hlin b = ⟨DescriptiveComplexity.binNum Le (fun (x : A) => True) b, ⋯⟩

theorem DescriptiveComplexity.binCode_bijective {A : Type} [Finite A] {Le : A → A → Prop} (hlin : IsLinOrd Le) : Function.Bijective (binCode hlin)

Binary decoding is a bijection from the sets of positions onto the numbers below 2 ^ n.

theorem DescriptiveComplexity.card_binNum_lt {A : Type} [Finite A] {Le : A → A → Prop} (hlin : IsLinOrd Le) (w : A → Prop) : Nat.card { b : A → Prop // binNum Le (fun (x : A) => True) b < binNum Le (fun (x : A) => True) w } = binNum Le (fun (x : A) => True) w

The sets of bits below a weight are as many as the weight.