Faithful encodings of concrete instance types

A DescriptiveComplexity.DecisionProblem is a property of finite structures. A user of the library starts elsewhere: from concrete data – a list of atoms, a family of weights – which must be encoded as a structure before any theorem of the library applies. That encoding step carries two obligations:

1. semantic equivalence – the abstract semantics on the encoded structure agrees with the textbook semantics of the concrete data; and
2. representation faithfulness – the encoded structure is of the right size. Get this wrong and the complexity result is about a different computational problem, however faithfully its meaning matches: encode a number in unary (as the cardinality of a marked set) when the honest size counts its bit length, and a subset-sum instance sits on a universe exponential in its own size, so its NP-hardness silently evaporates.

This file makes obligation 2 a proof obligation: DescriptiveComplexity.Encoding bundles the concrete instance type, its declared size, the encoding map, and polynomial bounds in both directions between the declared size and the cardinality of the encoded universe – so that an encoding cannot be constructed without discharging them. card_le forbids padding (protecting membership claims: pad the universe to 2 ^ size and "in NP over structures" becomes a much weaker statement about the concrete problem); le_card forbids compression (protecting hardness claims), and also defends the definition against inflating size to make card_le vacuous. Obligation 1 remains a theorem the user proves, now packaged as DescriptiveComplexity.Encoding.Faithful.

The bounds compare the declared size with Nat.card of the universe rather than with a bit size: the vocabulary is fixed and of fixed arity, so a structure on n elements takes Θ(n ^ r) bits – cardinality and bit size are polynomially related, and the criterion is polynomial.

Hygiene: computability, enforced

The relations of an encoding are Bool-valued (relBool), and the FirstOrder.Language.Structure instance on the universe is derived from them, not supplied: an encoder is a computation, not an arbitrary Prop. This is enforced by the compiler rather than by convention – a definition whose data decides an undecidable predicate must be marked noncomputable, so the check to run on an encoder is simply "its relBool elaborates as a plain def, with no noncomputable marker". Together with the DecidableEq and Fintype fields this makes an encoding genuinely executable: an encoded structure can be #eval-ed on a small instance and tested before anything is proved about it.

Do not run #print axioms on a bundled Encoding to check its encoder: proof fields are erased by the compiler but not by #print axioms, so the bound proofs (which typically use classical axioms through Nat.card) mask the report. The axiom report is only informative on a standalone relBool definition – and even there "no axioms" is the expected answer only for quotient-free data: an encoder deciding Finset membership goes through Multiset quotients, whose Decidable instances cite the classical axioms in proof positions without affecting executability. The reliable checks are the two the compiler and evaluator give: no noncomputable marker, and a #guard/#eval that actually reduces.

What this does not buy

Nothing here rules out an encoder that computes the answer: encode a SAT instance on a universe of the right size with one unary predicate marking an element iff the formula is satisfiable, and take the problem "some element is marked". Both bounds hold, Faithful is provable, and the problem is even FO-definable; the illegitimacy is entirely in the computational power the encoder used. Computability of the encoder is enforced, a complexity bound on it is not – that would need the machine bridge (ROADMAP.md §7), on top of which "the encoder is computed by a polynomial-time machine" becomes expressible. Until then the reader of an encoding is told exactly which of the two obligations is machine-checked and which still requires reading relBool.

The decoding direction

Membership results transfer to the concrete problem along a faithful encoding; hardness results need a converse – the abstract problem must not be hard only on junk structures the encoding never produces. The machinery for that converse lives in DescriptiveComplexity/Decoding.lean: well-formedness as a decision problem (restricting hardness to W ⊓ P) and computable decodings (DescriptiveComplexity.Decoding), with the same hygiene as the encoders here. DescriptiveComplexity.Encoding.Covers below is the ideal, isomorphism-based decoding statement; junk conventions usually make it unprovable for honest encodings, which is exactly what the well-formedness route is for.

Main declarations

• DescriptiveComplexity.Encoding: the bundled encoding, with its two size bounds;
• DescriptiveComplexity.Encoding.str: the derived structure on an encoded universe;
• DescriptiveComplexity.Encoding.Faithful: obligation 1, semantic equivalence with a concrete predicate;
• DescriptiveComplexity.Encoding.Covers: the ideal, isomorphism-based decoding statement (see DescriptiveComplexity/Decoding.lean for the practical route);
• DescriptiveComplexity.Encoding.linear_bound: discharge a bound field from a linear estimate, the common case.

A worked example – the packaged conjunctive-query instances – is in DescriptiveComplexity/Examples/ConjunctiveQueries.lean; the theorem that the size bounds have teeth (no unary encoding of subset-sum satisfies them) is in DescriptiveComplexity/Encoding/UnaryBlowup.lean.

structure DescriptiveComplexity.Encoding (L : FirstOrder.Language) (ι : Type u_1) : Type (max 1 u_1)

An encoding of a concrete instance type ι by finite structures of the relational vocabulary L: a declared instance size, a computable (Bool- valued) family of structures, and polynomial bounds both ways between the declared size and the cardinality of the encoded universe – no padding (card_le) and no compression (le_card). See the module docstring for why the bounds are fields: an encoding must not be constructible with them postponed.

• size : ι → ℕ

  The textbook size of a concrete instance. The one line a reader audits: everything else is checked against it.

• Univ : ι → Type

  The universe carrying the encoded structure of an instance.

• deceq (i : ι) : DecidableEq (self.Univ i)

  Decidable equality on the universe, so the encoding is testable.

• fintype (i : ι) : Fintype (self.Univ i)

  The universe is (computably) finite.

• relBool (i : ι) {n : ℕ} : L.Relations n → (Fin n → self.Univ i) → Bool

  The relations, as computations: relBool i R x decides whether the tuple x is in relation R on the encoded instance i. Keep this a plain def-legible field – a noncomputable encoder is a red flag (see the module docstring).

• card_le : ∃ (c : ℕ) (d : ℕ), ∀ (i : ι), Nat.card (self.Univ i) ≤ c * (self.size i + 1) ^ d

  No padding: the universe is polynomially bounded in the declared size.

• le_card : ∃ (c : ℕ) (d : ℕ), ∀ (i : ι), self.size i ≤ c * (Nat.card (self.Univ i) + 1) ^ d

  No compression: the declared size is polynomially bounded in the universe.

@[instance_reducible]

instance DescriptiveComplexity.Encoding.instDecidableEqUniv {L : FirstOrder.Language} {ι : Type u_1} (e : Encoding L ι) (i : ι) : DecidableEq (e.Univ i)

Equations

• e.instDecidableEqUniv i = e.deceq i

@[instance_reducible]

instance DescriptiveComplexity.Encoding.instFintypeUniv {L : FirstOrder.Language} {ι : Type u_1} (e : Encoding L ι) (i : ι) : Fintype (e.Univ i)

Equations

• e.instFintypeUniv i = e.fintype i

instance DescriptiveComplexity.Encoding.instFiniteUniv {L : FirstOrder.Language} {ι : Type u_1} (e : Encoding L ι) (i : ι) : Finite (e.Univ i)

theorem DescriptiveComplexity.Encoding.linear_bound {ι : Type u_1} {f s : ι → ℕ} {c : ℕ} (h : ∀ (i : ι), f i ≤ c * (s i + 1)) : ∃ (c' : ℕ) (d : ℕ), ∀ (i : ι), f i ≤ c' * (s i + 1) ^ d

Discharge a card_le/le_card field from a linear estimate – the common case; every honest encoding in the catalog's reach is linear or nearly so.

theorem DescriptiveComplexity.Encoding.poly_bound {ι : Type u_1} {f s : ι → ℕ} {c d : ℕ} (h : ∀ (i : ι), f i ≤ c * (s i + 1) ^ d) : ∃ (c' : ℕ) (d' : ℕ), ∀ (i : ι), f i ≤ c' * (s i + 1) ^ d'

Discharge a card_le/le_card field from a degree-d estimate.

@[instance_reducible]

instance DescriptiveComplexity.Encoding.str {L : FirstOrder.Language} {ι : Type u_1} [L.IsRelational] (e : Encoding L ι) (i : ι) : L.Structure (e.Univ i)

The L-structure an encoding puts on the universe of an instance: the relations are the encoder's computations, read as propositions. Derived from relBool rather than supplied, so that the structure of an encoded instance is exactly what the encoder computes.

Equations

• e.str i = { funMap := fun {n : ℕ} (f : L.Functions n) => isEmptyElim f, RelMap := fun {n : ℕ} (R : L.Relations n) (x : Fin n → e.Univ i) => e.relBool i R x = true }

@[simp]

theorem DescriptiveComplexity.Encoding.relMap_iff {L : FirstOrder.Language} {ι : Type u_1} [L.IsRelational] (e : Encoding L ι) (i : ι) {n : ℕ} (R : L.Relations n) (x : Fin n → e.Univ i) : FirstOrder.Language.Structure.RelMap R x ↔ e.relBool i R x = true

The relations of an encoded structure are the encoder's computations. The simp normal form for proofs about encoded structures.

@[instance_reducible]

instance DescriptiveComplexity.Encoding.instDecidableRelMapUniv {L : FirstOrder.Language} {ι : Type u_1} [L.IsRelational] (e : Encoding L ι) (i : ι) {n : ℕ} (R : L.Relations n) (x : Fin n → e.Univ i) : Decidable (FirstOrder.Language.Structure.RelMap R x)

Equations

• e.instDecidableRelMapUniv i R x = decidable_of_iff (e.relBool i R x = true) ⋯

def DescriptiveComplexity.Encoding.Faithful {L : FirstOrder.Language} {ι : Type u_1} [L.IsRelational] (e : Encoding L ι) (Conc : ι → Prop) (P : DecisionProblem L) : Prop

Semantic equivalence (obligation 1 of the module docstring): the abstract problem P computes the concrete predicate Conc on every encoded instance. A separate predicate rather than a field, because one encoding may serve several problems over the same vocabulary.

Equations

• e.Faithful Conc P = ∀ (i : ι), Conc i ↔ P.Holds (e.Univ i)

theorem DescriptiveComplexity.Encoding.faithful_congr {L : FirstOrder.Language} {ι : Type u_1} [L.IsRelational] {e : Encoding L ι} {Conc : ι → Prop} {P Q : DecisionProblem L} (hPQ : ∀ (A : Type) [inst : L.Structure A], P.Holds A ↔ Q.Holds A) : e.Faithful Conc P ↔ e.Faithful Conc Q

Faithfulness transports along (extensional) equality of decision problems, so a user may state it against the bundled problem or against the raw predicate.

def DescriptiveComplexity.Encoding.Covers {L : FirstOrder.Language} {ι : Type u_1} [L.IsRelational] (e : Encoding L ι) : Prop

The encoding reaches every finite structure up to isomorphism: the ideal decoding direction. Junk conventions can make this literally unprovable for an honest encoding (some abstract structures carry facts the concrete type cannot represent); the practical route is a computable decoding of the well-formed structures – DescriptiveComplexity.Decoding, in DescriptiveComplexity/Decoding.lean.

Equations

• e.Covers = ∀ (A : Type) [inst : L.Structure A] [Finite A], ∃ (i : ι), Nonempty (L.Equiv A (e.Univ i))