The binary encoding of subset-sum instances, and what it decodes to

The catalog's weighted problems – Knapsack and everything reduced from it – live on FirstOrder.Language.binWeights structures, whose numbers are sets of bit positions read by DescriptiveComplexity.binNum. A user does not start there: they start from a list of weights and a target. This file is the bridge, and it is what the size discipline of DescriptiveComplexity.Encoding is for, since for these problems the representation is part of the statement – in unary they are solvable in polynomial time.

• DescriptiveComplexity.binarySubsetSumEncoding is the honest binary encoding of DescriptiveComplexity.SubsetSumInstance = List ℕ × ℕ: one element per item, one element per bit position, bit and tgt reading the binary digits, place values carried by the order. Both size bounds – card_le (no padding) and le_card (no compression) – are discharged at construction, against the declared size DescriptiveComplexity.ssSize, the total bit length. That they have teeth is DescriptiveComplexity.no_unary_encoding, in DescriptiveComplexity.Encoding.UnaryBlowup: no encoding sized this way can hold one universe element per unit of weight.
• The BinarySubsetSum namespace decodes it: the vocabulary's relations on an encoded instance (BinarySubsetSum.item_itemPt and friends), the order is linear (BinarySubsetSum.isLinOrd), the rank of a position is its index (BinarySubsetSum.bitRank_posnPt), and therefore each item's decoded weight is its list entry and the decoded target is the target (BinarySubsetSum.weight_itemPt, BinarySubsetSum.target).
• DescriptiveComplexity.selection_toIndex and DescriptiveComplexity.selection_ofIndex turn a selection of items on any structure into a Finset of indices and back, along any injective indexing of the items, preserving both the total weight and whether the selection is empty. They are the reusable half: any problem on binWeights that quantifies over selections of items – Knapsack here, and variants that constrain the selection further – gets both directions from these two.
• DescriptiveComplexity.binarySubsetSumEncoding_faithful closes the loop for Knapsack: DescriptiveComplexity.ConcreteSubsetSum, the textbook predicate on a list and a target, is exactly what DescriptiveComplexity.Knapsack computes on the encoded structure. Read through it, DescriptiveComplexity.knapsack_NP_complete is a statement about lists of binary-written numbers.
• DescriptiveComplexity.bwDecoding is the converse direction, the one hardness needs: a computable decoder from presented structures back to lists of weights. It needs no well-formedness condition, there being no junk to exclude – a structure whose order is not linear is a definite no-instance, and a concrete no-instance decodes it. Hence DescriptiveComplexity.exists_concreteSubsetSum_iff, for every nonempty finite structure.

The universe elements are named by BinarySubsetSum.itemPt and BinarySubsetSum.posnPt rather than written as Sum.inl/Sum.inr: the encoded universe binarySubsetSumEncoding.Univ i is a projection out of the encoder, so it is opaque to simp's type-correctness check, and a raw constructor application would be typed at the unfolded sum instead. The two constructors carry the right type by definition, and BinarySubsetSum.pt_cases replaces cases on a universe element.

The instance type, its size, and the encoding

@[reducible, inline]

abbrev DescriptiveComplexity.SubsetSumInstance : Type

A concrete subset-sum instance: a list of weights and a target.

Equations

• DescriptiveComplexity.SubsetSumInstance = (List ℕ × ℕ)

def DescriptiveComplexity.ssSize : SubsetSumInstance → ℕ

The honest size of a subset-sum instance: the total bit length of its weights and of its target, plus the number of items (so that zero weights still take room). An encoding sized this way must represent weights in binary or violate card_le.

Equations

• DescriptiveComplexity.ssSize i = (List.map Nat.size i.1).sum + i.2.size + i.1.length

def DescriptiveComplexity.binarySubsetSumEncoding : Encoding FirstOrder.Language.binWeights SubsetSumInstance

The honest binary encoding of subset-sum instances – one element per item, one element per bit position, bit and tgt reading the binary digits, place values carried by the order – which passes both size bounds with room to spare. Its semantics is binarySubsetSumEncoding_faithful.

Equations

• One or more equations did not get rendered due to their size.

The two kinds of universe element

def DescriptiveComplexity.BinarySubsetSum.itemPt (i : SubsetSumInstance) (j : Fin i.1.length) : binarySubsetSumEncoding.Univ i

The universe element carrying the item at list position j.

Equations

• DescriptiveComplexity.BinarySubsetSum.itemPt i j = Sum.inl j

def DescriptiveComplexity.BinarySubsetSum.posnPt (i : SubsetSumInstance) (p : Fin (ssSize i + 1)) : binarySubsetSumEncoding.Univ i

The universe element carrying the bit position p.

Equations

• DescriptiveComplexity.BinarySubsetSum.posnPt i p = Sum.inr p

theorem DescriptiveComplexity.BinarySubsetSum.pt_cases {i : SubsetSumInstance} (q : binarySubsetSumEncoding.Univ i) : (∃ (j : Fin i.1.length), q = itemPt i j) ∨ ∃ (p : Fin (ssSize i + 1)), q = posnPt i p

The universe of an encoded instance is exactly its items and its bit positions. This replaces cases on a universe element.

theorem DescriptiveComplexity.BinarySubsetSum.itemPt_injective {i : SubsetSumInstance} : Function.Injective (itemPt i)

theorem DescriptiveComplexity.BinarySubsetSum.posnPt_injective {i : SubsetSumInstance} : Function.Injective (posnPt i)

@[simp]

theorem DescriptiveComplexity.BinarySubsetSum.itemPt_inj {i : SubsetSumInstance} {j j' : Fin i.1.length} : itemPt i j = itemPt i j' ↔ j = j'

@[simp]

theorem DescriptiveComplexity.BinarySubsetSum.posnPt_inj {i : SubsetSumInstance} {p p' : Fin (ssSize i + 1)} : posnPt i p = posnPt i p' ↔ p = p'

@[simp]

theorem DescriptiveComplexity.BinarySubsetSum.itemPt_ne_posnPt {i : SubsetSumInstance} (j : Fin i.1.length) (p : Fin (ssSize i + 1)) : itemPt i j ≠ posnPt i p

@[simp]

theorem DescriptiveComplexity.BinarySubsetSum.posnPt_ne_itemPt {i : SubsetSumInstance} (p : Fin (ssSize i + 1)) (j : Fin i.1.length) : posnPt i p ≠ itemPt i j

The vocabulary on an encoded instance

Every relation of Language.binWeights is the encoder's computation, read back on the two kinds of element: the order puts all items before all positions and orders each kind by index. All of it holds by computation, the encoder being a plain def.

@[simp]

theorem DescriptiveComplexity.BinarySubsetSum.item_itemPt {i : SubsetSumInstance} (j : Fin i.1.length) : BWItem (itemPt i j)

@[simp]

theorem DescriptiveComplexity.BinarySubsetSum.item_posnPt {i : SubsetSumInstance} (p : Fin (ssSize i + 1)) : ¬BWItem (posnPt i p)

@[simp]

theorem DescriptiveComplexity.BinarySubsetSum.posn_itemPt {i : SubsetSumInstance} (j : Fin i.1.length) : ¬BWPosn (itemPt i j)

@[simp]

theorem DescriptiveComplexity.BinarySubsetSum.posn_posnPt {i : SubsetSumInstance} (p : Fin (ssSize i + 1)) : BWPosn (posnPt i p)

@[simp]

theorem DescriptiveComplexity.BinarySubsetSum.bit_itemPt_posnPt {i : SubsetSumInstance} (j : Fin i.1.length) (p : Fin (ssSize i + 1)) : BWBit (itemPt i j) (posnPt i p) ↔ (i.1.get j).testBit ↑p = true

@[simp]

theorem DescriptiveComplexity.BinarySubsetSum.bit_itemPt_itemPt {i : SubsetSumInstance} (j j' : Fin i.1.length) : ¬BWBit (itemPt i j) (itemPt i j')

@[simp]

theorem DescriptiveComplexity.BinarySubsetSum.bit_posnPt {i : SubsetSumInstance} (p : Fin (ssSize i + 1)) (q : binarySubsetSumEncoding.Univ i) : ¬BWBit (posnPt i p) q

@[simp]

theorem DescriptiveComplexity.BinarySubsetSum.tgt_posnPt {i : SubsetSumInstance} (p : Fin (ssSize i + 1)) : BWTgt (posnPt i p) ↔ i.2.testBit ↑p = true

@[simp]

theorem DescriptiveComplexity.BinarySubsetSum.tgt_itemPt {i : SubsetSumInstance} (j : Fin i.1.length) : ¬BWTgt (itemPt i j)

@[simp]

theorem DescriptiveComplexity.BinarySubsetSum.le_itemPt_itemPt {i : SubsetSumInstance} (j j' : Fin i.1.length) : BWLe (itemPt i j) (itemPt i j') ↔ j ≤ j'

@[simp]

theorem DescriptiveComplexity.BinarySubsetSum.le_itemPt_posnPt {i : SubsetSumInstance} (j : Fin i.1.length) (p : Fin (ssSize i + 1)) : BWLe (itemPt i j) (posnPt i p)

@[simp]

theorem DescriptiveComplexity.BinarySubsetSum.le_posnPt_itemPt {i : SubsetSumInstance} (p : Fin (ssSize i + 1)) (j : Fin i.1.length) : ¬BWLe (posnPt i p) (itemPt i j)

@[simp]

theorem DescriptiveComplexity.BinarySubsetSum.le_posnPt_posnPt {i : SubsetSumInstance} (p p' : Fin (ssSize i + 1)) : BWLe (posnPt i p) (posnPt i p') ↔ p ≤ p'

theorem DescriptiveComplexity.BinarySubsetSum.isLinOrd {i : SubsetSumInstance} : IsLinOrd BWLe

The encoded order is linear: all items, in index order, then all positions, in index order.

Decoding the numbers

The rank of a position is its index, so binNum is the plain sum of place values, and the encoder's Nat.testBit digits are read back as the number they came from.

theorem DescriptiveComplexity.BinarySubsetSum.bitRank_posnPt {i : SubsetSumInstance} (p : Fin (ssSize i + 1)) : bitRank BWLe BWPosn (posnPt i p) = ↑p

The rank of a bit position is its index: the positions strictly below it are exactly those with a smaller index.

theorem DescriptiveComplexity.BinarySubsetSum.binNum_eq_sum {i : SubsetSumInstance} (b : binarySubsetSumEncoding.Univ i → Prop) : binNum BWLe BWPosn b = ∑ p : Fin (ssSize i + 1), if b (posnPt i p) then 2 ^ ↑p else 0

On an encoded instance, binNum is the plain sum of place values over the bit positions.

theorem DescriptiveComplexity.BinarySubsetSum.binNum_eq {i : SubsetSumInstance} (w : ℕ) (hw : w < 2 ^ (ssSize i + 1)) (b : binarySubsetSumEncoding.Univ i → Prop) (hb : ∀ (p : Fin (ssSize i + 1)), b (posnPt i p) ↔ w.testBit ↑p = true) : binNum BWLe BWPosn b = w

The decoding. A set of bit positions carrying the binary digits of a number that fits in the position block decodes to that number.

The weights and the target

theorem DescriptiveComplexity.BinarySubsetSum.get_lt {i : SubsetSumInstance} (j : Fin i.1.length) : i.1.get j < 2 ^ (ssSize i + 1)

Every weight fits in the position block: its bit length is part of the declared size.

theorem DescriptiveComplexity.BinarySubsetSum.target_lt {i : SubsetSumInstance} : i.2 < 2 ^ (ssSize i + 1)

The target fits in the position block, for the same reason.

@[simp]

theorem DescriptiveComplexity.BinarySubsetSum.weight_itemPt {i : SubsetSumInstance} (j : Fin i.1.length) : BWWeight (itemPt i j) = i.1.get j

An item's decoded weight is its list entry.

@[simp]

theorem DescriptiveComplexity.BinarySubsetSum.weight_posnPt {i : SubsetSumInstance} (p : Fin (ssSize i + 1)) : BWWeight (posnPt i p) = 0

A bit position is not an item, and carries no weight.

@[simp]

theorem DescriptiveComplexity.BinarySubsetSum.target {i : SubsetSumInstance} : BWTarget (binarySubsetSumEncoding.Univ i) = i.2

The decoded target is the target.

theorem DescriptiveComplexity.BinarySubsetSum.item_iff_range {i : SubsetSumInstance} (q : binarySubsetSumEncoding.Univ i) : BWItem q ↔ ∃ (j : Fin i.1.length), itemPt i j = q

The items of an encoded instance are exactly the elements it indexes.

Selections of items, both ways

A selection of items is a set of indices, along any injective indexing of the items – the encoding's own, or a decoder's listing of the items of a presented structure. Both directions preserve the total weight and whether the selection is empty, which is everything a problem on binWeights asks of a selection.

theorem DescriptiveComplexity.selection_toIndex {A : Type} [FirstOrder.Language.binWeights.Structure A] {n : ℕ} (f : Fin n → A) (hf : Function.Injective f) (hrange : ∀ (a : A), BWItem a ↔ ∃ (j : Fin n), f j = a) (S : A → Prop) (hS : ∀ (a : A), S a → BWItem a) : ∃ (J : Finset (Fin n)), ∑ᶠ (a : A) (_ : a ∈ {a : A | S a}), BWWeight a = ∑ j ∈ J, BWWeight (f j) ∧ ((∃ (a : A), S a) ↔ J.Nonempty)

Every selection of items is a Finset of indices, with the same total weight and the same emptiness.

theorem DescriptiveComplexity.selection_ofIndex {A : Type} [FirstOrder.Language.binWeights.Structure A] {n : ℕ} (f : Fin n → A) (hf : Function.Injective f) (hitem : ∀ (j : Fin n), BWItem (f j)) (J : Finset (Fin n)) : ∃ (S : A → Prop), (∀ (a : A), S a → BWItem a) ∧ ∑ᶠ (a : A) (_ : a ∈ {a : A | S a}), BWWeight a = ∑ j ∈ J, BWWeight (f j) ∧ ((∃ (a : A), S a) ↔ J.Nonempty)

Conversely, every Finset of indices is a selection of items, with the same total weight and the same emptiness.

theorem DescriptiveComplexity.hasSubsetSum_iff_index {A : Type} [FirstOrder.Language.binWeights.Structure A] {n : ℕ} (f : Fin n → A) [Finite A] (hf : Function.Injective f) (hrange : ∀ (a : A), BWItem a ↔ ∃ (j : Fin n), f j = a) (hlin : IsLinOrd BWLe) : HasSubsetSum A ↔ ∃ (J : Finset (Fin n)), ∑ j ∈ J, BWWeight (f j) = BWTarget A

Knapsack, read along an indexing of the items: the abstract problem is the concrete subset-sum question about the indexed weights.

Faithfulness for Knapsack

def DescriptiveComplexity.ConcreteSubsetSum (i : SubsetSumInstance) : Prop

The textbook subset-sum predicate on a concrete instance: some set of list positions has weights summing to the target. Nothing here mentions model theory; it is the problem as it is stated before any encoding.

Equations

• DescriptiveComplexity.ConcreteSubsetSum i = ∃ (J : Finset (Fin i.1.length)), ∑ j ∈ J, i.1.get j = i.2

theorem DescriptiveComplexity.binarySubsetSumEncoding_faithful : binarySubsetSumEncoding.Faithful ConcreteSubsetSum Knapsack

The binary encoding is faithful: on every encoded instance, Knapsack computes the textbook predicate ConcreteSubsetSum. With the size bounds discharged at construction, this is what makes knapsack_NP_complete a statement about lists of binary-written numbers.

The decoding direction

Faithfulness reads membership back to concrete instances; reading hardness back needs the converse – that the abstract problem is not hard only on junk structures no encoding produces. Here there is no junk to exclude: every presented binWeights structure decodes. A structure whose order is not linear is a definite no-instance (HasSubsetSum carries IsLinOrd as a conjunct), and any concrete no-instance decodes it; on the rest, the decoder lists the items and reads their weights and the target off the presentation. So the well-formedness condition is trivial, and exists_concreteSubsetSum_iff holds for every nonempty finite structure.

The vocabulary of a presentation is decidable, being a table of Bools; these instances are what lets a decoder build Finsets and sum over them.

@[instance_reducible]

instance DescriptiveComplexity.BinarySubsetSum.instDecidablePredFinCardBWItem (S : FinPresentation FirstOrder.Language.binWeights) : DecidablePred BWItem

Equations

• DescriptiveComplexity.BinarySubsetSum.instDecidablePredFinCardBWItem S a = DescriptiveComplexity.BinarySubsetSum.instDecidablePredFinCardBWItem._aux_1 S a

@[instance_reducible]

instance DescriptiveComplexity.BinarySubsetSum.instDecidablePredFinCardBWPosn (S : FinPresentation FirstOrder.Language.binWeights) : DecidablePred BWPosn

Equations

• DescriptiveComplexity.BinarySubsetSum.instDecidablePredFinCardBWPosn S a = DescriptiveComplexity.BinarySubsetSum.instDecidablePredFinCardBWPosn._aux_1 S a

@[instance_reducible]

instance DescriptiveComplexity.BinarySubsetSum.instDecidablePredFinCardBWTgt (S : FinPresentation FirstOrder.Language.binWeights) : DecidablePred BWTgt

Equations

• DescriptiveComplexity.BinarySubsetSum.instDecidablePredFinCardBWTgt S a = DescriptiveComplexity.BinarySubsetSum.instDecidablePredFinCardBWTgt._aux_1 S a

@[instance_reducible]

instance DescriptiveComplexity.BinarySubsetSum.instDecidableRelFinCardBWBit (S : FinPresentation FirstOrder.Language.binWeights) : DecidableRel BWBit

Equations

• DescriptiveComplexity.BinarySubsetSum.instDecidableRelFinCardBWBit S a b = DescriptiveComplexity.BinarySubsetSum.instDecidableRelFinCardBWBit._aux_1 S a b

@[instance_reducible]

instance DescriptiveComplexity.BinarySubsetSum.instDecidableRelFinCardBWLe (S : FinPresentation FirstOrder.Language.binWeights) : DecidableRel BWLe

Equations

• DescriptiveComplexity.BinarySubsetSum.instDecidableRelFinCardBWLe S a b = DescriptiveComplexity.BinarySubsetSum.instDecidableRelFinCardBWLe._aux_1 S a b

def DescriptiveComplexity.BinarySubsetSum.isLinOrdB (S : FinPresentation FirstOrder.Language.binWeights) : Bool

Is the presented order linear?

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.BinarySubsetSum.isLinOrdB_iff (S : FinPresentation FirstOrder.Language.binWeights) : isLinOrdB S = true ↔ IsLinOrd BWLe

def DescriptiveComplexity.BinarySubsetSum.items (S : FinPresentation FirstOrder.Language.binWeights) : List (Fin S.card)

The items of a presentation, listed without duplicates.

Equations

• DescriptiveComplexity.BinarySubsetSum.items S = List.filter (fun (a : Fin S.card) => decide (DescriptiveComplexity.BWItem a)) (List.finRange S.card)

def DescriptiveComplexity.BinarySubsetSum.rankB (S : FinPresentation FirstOrder.Language.binWeights) (p : Fin S.card) : ℕ

The rank of a bit position, as a computation.

Equations

• DescriptiveComplexity.BinarySubsetSum.rankB S p = {q : Fin S.card | DescriptiveComplexity.BWPosn q ∧ DescriptiveComplexity.BWLe q p ∧ q ≠ p}.card

def DescriptiveComplexity.BinarySubsetSum.numB (S : FinPresentation FirstOrder.Language.binWeights) (b : Fin S.card → Prop) [DecidablePred b] : ℕ

A binary number of the presentation, as a computation: the noncomputable binNum is a finsum, and this is the Finset sum it equals.

Equations

• DescriptiveComplexity.BinarySubsetSum.numB S b = ∑ p : Fin S.card with DescriptiveComplexity.BWPosn p ∧ b p, 2 ^ DescriptiveComplexity.BinarySubsetSum.rankB S p

theorem DescriptiveComplexity.BinarySubsetSum.numB_eq (S : FinPresentation FirstOrder.Language.binWeights) (b : Fin S.card → Prop) [DecidablePred b] : numB S b = binNum BWLe BWPosn b

@[simp]

theorem DescriptiveComplexity.BinarySubsetSum.numB_bit (S : FinPresentation FirstOrder.Language.binWeights) (a : Fin S.card) : numB S (BWBit a) = BWWeight a

@[simp]

theorem DescriptiveComplexity.BinarySubsetSum.numB_tgt (S : FinPresentation FirstOrder.Language.binWeights) : numB S BWTgt = BWTarget (Fin S.card)

@[simp]

theorem DescriptiveComplexity.BinarySubsetSum.mem_items {S : FinPresentation FirstOrder.Language.binWeights} {a : Fin S.card} : a ∈ items S ↔ BWItem a

theorem DescriptiveComplexity.BinarySubsetSum.items_get_injective {S : FinPresentation FirstOrder.Language.binWeights} : Function.Injective (items S).get

theorem DescriptiveComplexity.BinarySubsetSum.items_range {S : FinPresentation FirstOrder.Language.binWeights} (a : Fin S.card) : BWItem a ↔ ∃ (j : Fin (items S).length), (items S).get j = a

def DescriptiveComplexity.bwDecode (S : FinPresentation FirstOrder.Language.binWeights) : Option SubsetSumInstance

The decoder: on a presentation whose order is linear, list the items and read their weights and the target off it; otherwise return a concrete no-instance, the presented structure being one too.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.concreteSubsetSum_map {α : Type} (l : List α) (g : α → ℕ) (t : ℕ) : ConcreteSubsetSum (List.map g l, t) ↔ ∃ (J : Finset (Fin l.length)), ∑ j ∈ J, g (l.get j) = t

Reindexing a decoded weight list: the concrete question about l.map g is the same question about g along l.

theorem DescriptiveComplexity.not_concreteSubsetSum_empty : ¬ConcreteSubsetSum ([], 1)

The empty list with a positive target is a concrete no-instance – what the decoder returns on a structure that is a no-instance for lack of a linear order.

theorem DescriptiveComplexity.bwDecode_sound (S : FinPresentation FirstOrder.Language.binWeights) (i : SubsetSumInstance) (hi : i ∈ bwDecode S) : ConcreteSubsetSum i ↔ Knapsack.Holds (Fin S.card)

theorem DescriptiveComplexity.bwDecode_total (S : FinPresentation FirstOrder.Language.binWeights) (_hpos : 0 < S.card) (_hW : (DecisionProblem.ofSentence ⊤).Holds (Fin S.card)) : (bwDecode S).isSome = true

def DescriptiveComplexity.bwDecoding : Decoding FirstOrder.Language.binWeights (DecisionProblem.ofSentence ⊤) ConcreteSubsetSum Knapsack

The computable decoding of binary-weighted structures. Together with binarySubsetSumEncoding_faithful it closes the loop: encoded instances are equidecided, and every nonempty finite structure decodes to an equidecided concrete instance, so Knapsack is nowhere hard only on junk. The well-formedness condition is ⊤ because there is no junk to exclude.

Equations

• DescriptiveComplexity.bwDecoding = { dec := DescriptiveComplexity.bwDecode, sound := DescriptiveComplexity.bwDecode_sound, total := DescriptiveComplexity.bwDecode_total }

def DescriptiveComplexity.bwPres : FinPresentation FirstOrder.Language.binWeights

A presented three-element structure: element 0 an item, elements 1 and 2 bit positions with 1 the low one, the item's weight and the target both 1. The decoder runs on it.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.exists_concreteSubsetSum_iff (A : Type) [FirstOrder.Language.binWeights.Structure A] [Finite A] [Nonempty A] : ∃ (i : SubsetSumInstance), ConcreteSubsetSum i ↔ Knapsack.Holds A

Hardness reads back to concrete data: every nonempty finite binary-weighted structure is decided by Knapsack exactly as some list of weights and target is by the textbook predicate.