Binary certificates for relation environments

List each relation's truth table in context order, using the same tuple order as the structure encoder. The universe size and arities are supplied externally, so the certificate needs no header or delimiters. Its length is exactly the sum of card ^ arity. Every string of that length represents one environment.

These are the guessed relation tables in Immerman's Descriptive Complexity, Section 7.1, Proposition 7.6. The functions are computable; their machine time bounds are a separate obligation.

@[reducible, inline]

abbrev Complexity.DescriptiveComplexity.DecREnv.EncodingSite (card : ℕ) (rctx : List ℕ) : Type

A cell in one of the relation-variable truth tables.

Equations

• Complexity.DescriptiveComplexity.DecREnv.EncodingSite card rctx = ((r : Fin rctx.length) × (Fin (rctx.get r) → Fin card))

def Complexity.DescriptiveComplexity.DecREnv.encodingSites (card : ℕ) (rctx : List ℕ) : List (EncodingSite card rctx)

Certificate cells in relation-context order, then canonical tuple order.

Equations

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

def Complexity.DescriptiveComplexity.DecREnv.encodingLength (card : ℕ) (rctx : List ℕ) : ℕ

Exact number of bits required to describe all supplied relations.

Equations

• Complexity.DescriptiveComplexity.DecREnv.encodingLength card rctx = (List.map (fun (k : ℕ) => card ^ k) rctx).sum

noncomputable def Complexity.DescriptiveComplexity.DecREnv.encodingPolynomial (rctx : List ℕ) : Polynomial ℕ

The certificate-length polynomial for a fixed list of relation arities.

Equations

• Complexity.DescriptiveComplexity.DecREnv.encodingPolynomial rctx = (List.map (fun (k : ℕ) => Polynomial.X ^ k) rctx).sum

def Complexity.DescriptiveComplexity.DecREnv.encode {card : ℕ} {rctx : List ℕ} (ρ : DecREnv card rctx) : List Bool

Concatenate the supplied relation truth tables without headers or padding.

Equations

• ρ.encode = List.map (fun (site : Complexity.DescriptiveComplexity.DecREnv.EncodingSite card rctx) => ρ site.fst site.snd) (Complexity.DescriptiveComplexity.DecREnv.encodingSites card rctx)

def Complexity.DescriptiveComplexity.DecREnv.read (card : ℕ) (rctx : List ℕ) (bits : List Bool) : DecREnv card rctx

Read a relation environment, defaulting missing entries to false.

Equations

• Complexity.DescriptiveComplexity.DecREnv.read card rctx bits r args = bits[List.idxOf ⟨r, args⟩ (Complexity.DescriptiveComplexity.DecREnv.encodingSites card rctx)]?.getD false

def Complexity.DescriptiveComplexity.DecREnv.decode (card : ℕ) (rctx : List ℕ) (bits : List Bool) : Option (DecREnv card rctx)

Decode a certificate, rejecting precisely the strings of the wrong length.

Equations

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