Exact truth-table certificates for second-order witnesses

The encoder bijects Boolean relation environments with all bit strings of the prescribed length. The decoder rejects exactly incorrect lengths. Nullary relations take one bit, and an empty context takes no bits. The exact length is a polynomial in the universe size, for a fixed relation context.

theorem Complexity.DescriptiveComplexity.DecREnv.mem_encodingSites (card : ℕ) (rctx : List ℕ) (site : EncodingSite card rctx) : site ∈ encodingSites card rctx

Every relation-table cell occurs in the certificate enumeration.

theorem Complexity.DescriptiveComplexity.DecREnv.encodingSites_nodup (card : ℕ) (rctx : List ℕ) : (encodingSites card rctx).Nodup

Each relation-table cell occurs exactly once.

@[simp]

theorem Complexity.DescriptiveComplexity.DecREnv.encodingSites_length (card : ℕ) (rctx : List ℕ) : (encodingSites card rctx).length = encodingLength card rctx

The site list has the exact sum-of-powers length.

@[simp]

theorem Complexity.DescriptiveComplexity.DecREnv.encodingLength_nil (card : ℕ) : encodingLength card [] = 0

The empty relation context needs no certificate bits.

@[simp]

theorem Complexity.DescriptiveComplexity.DecREnv.encodingLength_cons (card k : ℕ) (rctx : List ℕ) : encodingLength card (k :: rctx) = card ^ k + encodingLength card rctx

Extending the context adds one truth table of length card ^ k.

@[simp]

theorem Complexity.DescriptiveComplexity.DecREnv.encode_length {card : ℕ} {rctx : List ℕ} (ρ : DecREnv card rctx) : ρ.encode.length = encodingLength card rctx

The certificate has exactly the sum of its relation-table sizes.

theorem Complexity.DescriptiveComplexity.DecREnv.encode_eq_flatMap {card : ℕ} {rctx : List ℕ} (ρ : DecREnv card rctx) : ρ.encode = List.flatMap (fun (r : Fin rctx.length) => encodeRelC (ρ r)) (List.finRange rctx.length)

The certificate lists each relation's canonical truth table in context order.

theorem Complexity.DescriptiveComplexity.DecREnv.encode_cons {card k : ℕ} {rctx : List ℕ} (S : (Fin k → Fin card) → Bool) (ρ : DecREnv card rctx) : (cons S ρ).encode = encodeRelC S ++ ρ.encode

Extending the environment prepends the new relation's truth table.

theorem Complexity.DescriptiveComplexity.DecREnv.encode_unary {card : ℕ} (color : Fin card → Bool) : (cons (fun (args : Fin 1 → Fin card) => color (args 0)) (empty card)).encode = List.ofFn color

A single unary relation is encoded in vertex order.

@[simp]

theorem Complexity.DescriptiveComplexity.DecREnv.read_encode {card : ℕ} {rctx : List ℕ} (ρ : DecREnv card rctx) : read card rctx ρ.encode = ρ

Direct reads recover every encoded relation.

theorem Complexity.DescriptiveComplexity.DecREnv.encode_read (card : ℕ) (rctx : List ℕ) (bits : List Bool) (h : bits.length = encodingLength card rctx) : (read card rctx bits).encode = bits

Every string of the specified length is the encoding of its decoded tables.

@[simp]

theorem Complexity.DescriptiveComplexity.DecREnv.decode_encode {card : ℕ} {rctx : List ℕ} (ρ : DecREnv card rctx) : decode card rctx ρ.encode = some ρ

The checked decoder recovers the supplied relation environment.

theorem Complexity.DescriptiveComplexity.DecREnv.encode_injective (card : ℕ) (rctx : List ℕ) : Function.Injective encode

Distinct relation environments have distinct certificates.

theorem Complexity.DescriptiveComplexity.DecREnv.decode_eq_some_iff {card : ℕ} {rctx : List ℕ} (bits : List Bool) (ρ : DecREnv card rctx) : decode card rctx bits = some ρ ↔ ρ.encode = bits

Decoding succeeds precisely on a relation environment's canonical encoding.

@[simp]

theorem Complexity.DescriptiveComplexity.DecREnv.decode_eq_none_iff (card : ℕ) (rctx : List ℕ) (bits : List Bool) : decode card rctx bits = none ↔ bits.length ≠ encodingLength card rctx

Certificate rejection is exactly a length mismatch.

@[simp]

theorem Complexity.DescriptiveComplexity.DecREnv.encodingPolynomial_eval (card : ℕ) (rctx : List ℕ) : Polynomial.eval card (encodingPolynomial rctx) = encodingLength card rctx

Exact witness length is a polynomial in universe cardinality.

theorem Complexity.DescriptiveComplexity.DecREnv.encodingLength_mono (rctx : List ℕ) : Monotone fun (card : ℕ) => encodingLength card rctx

Increasing the universe size cannot shorten a relation certificate.