Polynomial bounds in the length of an encoded structure

A well-formed input a of cardinality n ≥ 1 has encoding length at most (v.count + 1) * (2 * n ^ v.maxArity + 1), a polynomial in n fixed by the vocabulary. So every polynomial bound in the encoding length is eventually below one fixed power n ^ k. Machine simulations in descriptive complexity (Fagin, Immerman–Vardi, Grädel, NL ⊆ FO(TC)) choose their tuple width k this way, so that the power universe Fin (n ^ k) holds the machine's input, its running time and its configurations.

Main results

• Cslib.Logic.Vocabulary.length_encStructure_le_pow: the encoding of a well-formed input of cardinality n ≥ 1 has length at most (v.count + 1) * (2 * n ^ v.maxArity + 1).
• Cslib.Logic.Vocabulary.exists_pow_bound: for a polynomially bounded g, a tuple width k ≥ 1 bounding all arities of v with g (encStructure a).length < a.1 ^ k on every well-formed input of cardinality at least two.

theorem Cslib.Logic.Vocabulary.length_encStructure_le_pow {L : FirstOrder.Language} (v : Vocabulary L) {a : EncodedStructure} (ha : v.WellFormed a) (ha1 : 1 ≤ a.1) : (encStructure a).length ≤ (v.count + 1) * (2 * a.1 ^ v.maxArity + 1)

For a well-formed input a with 1 ≤ a.1, (encStructure a).length is bounded by (v.count + 1) * (2 * a.1 ^ v.maxArity + 1).

theorem Cslib.Logic.Vocabulary.exists_pow_bound {L : FirstOrder.Language} (v : Vocabulary L) (g : ℕ → ℕ) (hg : PolynomiallyBounded g) : ∃ (k : ℕ), 1 ≤ k ∧ (∀ (i : Fin v.count), v.arity i ≤ k) ∧ ∀ (a : EncodedStructure), v.WellFormed a → 2 ≤ a.1 → g (encStructure a).length < a.1 ^ k

A polynomial bound in the encoding length is below a single power of the cardinality: for a polynomially bounded g there is an exponent k ≥ 1 bounding all relation arities of v such that g (encStructure a).length < a.1 ^ k for every well-formed input a with a.1 ≥ 2.