The size bounds have teeth: unary encodings are rejected

A criterion nobody can fail is worth nothing. This file proves that the card_le bound of DescriptiveComplexity.Encoding genuinely rejects the one mistake the choice of number encoding (DescriptiveComplexity.Numbers) can lead to: encoding a number in unary – as the cardinality of a marked set – when the honest size of the instance counts its bit length. Under a unary encoding a subset-sum instance sits on a universe exponential in its own size, and the NP-hardness of the weighted problems of the catalog (Knapsack, Partition, Job Sequencing, 0-1 Integer Programming) would silently evaporate.

• DescriptiveComplexity.no_unary_encoding: there is no encoding of subset-sum instances, sized by bit length, whose universe holds one element per unit of weight. The witness family is ([2 ^ k], 2 ^ k), of size Θ(k): a unary universe on it is exponential in the declared size, so card_le cannot be discharged.
• DescriptiveComplexity.binarySubsetSumEncoding: the honest binary encoding of the same instance type (DescriptiveComplexity.Numbers.Binary: items and bit positions, a bit relation) satisfies both bounds with room to spare.

Together they turn the prose lesson of DescriptiveComplexity.Numbers – unary versus binary genuinely changes the problem – into a theorem.

This file is deliberately off the library's core import path: the negative result needs a little asymptotics (Mathlib.Analysis.SpecificLimits.Normed), which the core does not otherwise pull in.

@[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

theorem DescriptiveComplexity.exists_mul_pow_lt_two_pow (c d : ℕ) : ∃ (k : ℕ), c * (2 * k + 4) ^ d < 2 ^ k

Exponential beats polynomial, in the pointed form the negative example needs: some k has c * (2 * k + 4) ^ d < 2 ^ k.

theorem DescriptiveComplexity.no_unary_encoding : ¬∃ (e : Encoding FirstOrder.Language.binWeights SubsetSumInstance), e.size = ssSize ∧ ∀ (i : SubsetSumInstance), i.1.sum ≤ Nat.card (e.Univ i)

No unary encoding: no encoding of subset-sum instances, sized by bit length, can have a universe holding one element per unit of weight – the no-padding bound card_le fails on the family ([2 ^ k], 2 ^ k). This is the theorem that gives the size discipline of Encoding its teeth: the representation choice that unary-vs-binary prose warns about is now a proof that does not close.

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

The positive counterpart: 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 – passes both size bounds with room to spare. (Only the size discipline is at stake here, so no semantic theorem accompanies this encoding; the catalog's Knapsack development is where Language.binWeights structures get their semantics.)

Equations

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