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, in DescriptiveComplexity.Encoding.BinarySubsetSum, is the positive contrast: 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, and is faithful for Knapsack.

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.

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.