Encoding canonical full-tuple interpretations

A full-tuple interpretation is the ordered interpretation whose domain formula is true (FullTupleInterpretation.toDomainInterpretation), with ranks given by lexicographic rank on all tuples. A valid source of size at least two is mapped to the full tuple universe, numbered by lexRank, agreeing with DomainInterpretation.encodedMap (FullTupleInterpretation.encodedMap_toDomainInterpretation). Only the target input relations are serialized; canonical order, BIT and constants are computed from the target cardinality. Relation tables keep tupleIndex order across their arguments. Malformed sources and sizes zero and one map to a fixed malformed target.

Main definitions

• Cslib.Logic.FO.Ordered.FullTupleInterpretation.toDomainInterpretation: embedding as an interpretation with domain formula ⊤.
• Cslib.Logic.FO.Ordered.FullTupleInterpretation.encodedMap: the total map on parsed instances.

Main results

• Cslib.Logic.FO.Ordered.FullTupleInterpretation.unrank_toDomainInterpretation: ranks are lexicographic ranks.
• Cslib.Logic.FO.Ordered.FullTupleInterpretation.encodedMap_toDomainInterpretation: agreement with DomainInterpretation.encodedMap.
• Cslib.Logic.FO.Ordered.FullTupleInterpretation.card_encodedMap: exact target cardinality.
• Cslib.Logic.FO.Ordered.FullTupleInterpretation.table_encodedMap: exact table numbering.
• Cslib.Logic.FO.Ordered.FullTupleInterpretation.wellFormed_encodedMap_iff: exact shape guard.

References

• N. Immerman, Descriptive Complexity, Remark 1.32, Exercise 1.33 and Proposition 3.5. The full-domain hypothesis is essential; restricted domains still require explicit definitions and correctness proofs for their numeric symbols.

def Cslib.Logic.FO.Ordered.FullTupleInterpretation.toDomainInterpretation {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} (I : FullTupleInterpretation L L' k) : DomainInterpretation L L' k

A full-tuple interpretation is the ordered interpretation with domain formula true.

theorem Cslib.Logic.FO.Ordered.FullTupleInterpretation.card_toDomainInterpretation {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} {I : FullTupleInterpretation L L' k} (M : Structure L) : I.toDomainInterpretation.card M = M.size ^ k

theorem Cslib.Logic.FO.Ordered.FullTupleInterpretation.unrank_toDomainInterpretation {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} {I : FullTupleInterpretation L L' k} {M : Structure L} (i : Fin (I.toDomainInterpretation.card M)) : I.toDomainInterpretation.unrank M i = lexEquiv.symm (Fin.cast ⋯ i)

The ranks of a full-tuple interpretation are the lexicographic ranks of all tuples.

@[simp]

theorem Cslib.Logic.FO.Ordered.FullTupleInterpretation.lexRank_unrank_toDomainInterpretation {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} {I : FullTupleInterpretation L L' k} {M : Structure L} (i : Fin (I.toDomainInterpretation.card M)) : lexRank (I.toDomainInterpretation.unrank M i) = ↑i

theorem Cslib.Logic.FO.Ordered.FullTupleInterpretation.admissible_toDomainInterpretation {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} {I : FullTupleInterpretation L L' k} (hk : 0 < k) : I.toDomainInterpretation.Admissible

Positive-dimensional full-tuple interpretations are admissible.

noncomputable def Cslib.Logic.FO.Ordered.FullTupleInterpretation.encodedMap {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {k : ℕ} (I : FullTupleInterpretation L L' k) (v : Vocabulary L) (v' : Vocabulary L') (a : EncodedStructure) : EncodedStructure

Encode the interpreted input relations on the canonical rank universe. Invalid shapes or sizes below two produce one empty table too many, outside every target query language.

theorem Cslib.Logic.FO.Ordered.FullTupleInterpretation.encodedMap_of_admissible {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {k : ℕ} (I : FullTupleInterpretation L L' k) (v : Vocabulary L) (v' : Vocabulary L') {a : EncodedStructure} (ha : v.WellFormed a) (hn : 2 ≤ a.1) : I.encodedMap v v' a = v'.encode (Fin (a.1 ^ k)) (Equiv.refl (Fin (a.1 ^ k)))

theorem Cslib.Logic.FO.Ordered.FullTupleInterpretation.encodedMap_of_not_admissible {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {k : ℕ} (I : FullTupleInterpretation L L' k) (v : Vocabulary L) (v' : Vocabulary L') {a : EncodedStructure} (ha : ¬(v.WellFormed a ∧ 2 ≤ a.1)) : I.encodedMap v v' a = (0, List.replicate (v'.count + 1) [])

theorem Cslib.Logic.FO.Ordered.FullTupleInterpretation.encodedMap_toDomainInterpretation {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {k : ℕ} {I : FullTupleInterpretation L L' k} (v : Vocabulary L) (v' : Vocabulary L') : I.toDomainInterpretation.encodedMap v v' = I.encodedMap v v'

The encoded maps agree: the full-tuple encoded map is that of the embedded interpretation, for every dimension and every input.

theorem Cslib.Logic.FO.Ordered.FullTupleInterpretation.card_encodedMap {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {k : ℕ} (I : FullTupleInterpretation L L' k) (v : Vocabulary L) (v' : Vocabulary L') {a : EncodedStructure} (ha : v.WellFormed a) (hn : 2 ≤ a.1) : (I.encodedMap v v' a).1 = a.1 ^ k

The canonical rank universe has exactly one element per source tuple.

@[simp]

theorem Cslib.Logic.FO.Ordered.FullTupleInterpretation.wellFormed_encodedMap_iff {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {k : ℕ} (I : FullTupleInterpretation L L' k) (v : Vocabulary L) (v' : Vocabulary L') {a : EncodedStructure} : v'.WellFormed (I.encodedMap v v' a) ↔ v.WellFormed a ∧ 2 ≤ a.1

Shape validity of the result is exactly source admissibility. Positive dimension is only needed when asking for canonical target numerics, not for this shape statement.

theorem Cslib.Logic.FO.Ordered.FullTupleInterpretation.two_le_card_encodedMap {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {k : ℕ} (I : FullTupleInterpretation L L' k) (v : Vocabulary L) (v' : Vocabulary L') {a : EncodedStructure} (hk : 0 < k) (ha : v.WellFormed a) (hn : 2 ≤ a.1) : 2 ≤ (I.encodedMap v v' a).1

A positive-dimensional admissible source produces an admissible target cardinality.

theorem Cslib.Logic.FO.Ordered.FullTupleInterpretation.table_encodedMap {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {k : ℕ} (I : FullTupleInterpretation L L' k) (v : Vocabulary L) (v' : Vocabulary L') {a : EncodedStructure} (ha : v.WellFormed a) (hn : 2 ≤ a.1) {r : ℕ} (R : L'.Relations r) (x : Fin r → Fin (a.1 ^ k)) : (v'.table (I.encodedMap v v' a) ⟨r, R⟩).getD (tupleIndex x) false = true ↔ (I.rel R).Realize fun (p : Fin r × Fin k) => lexEquiv.symm (x p.1) p.2

The bit at the existing table index of the target arguments is the defining formula on their inverse lexicographic ranks. Numeric predicates are not serialized as extra tables.

theorem Cslib.Logic.FO.Ordered.FullTupleInterpretation.length_encStructure_encodedMap {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {k : ℕ} (I : FullTupleInterpretation L L' k) (v : Vocabulary L) (v' : Vocabulary L') {a : EncodedStructure} (ha : v.WellFormed a) (hn : 2 ≤ a.1) : (encStructure (I.encodedMap v v' a)).length = 2 * a.1 ^ k + 1 + ∑ j : Fin v'.count, (2 * (a.1 ^ k) ^ v'.arity j + 1)

The output length includes its unary cardinality and every framed relation table.

noncomputable def Cslib.Logic.FO.Ordered.FullTupleInterpretation.encodedModelEquiv {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {k : ℕ} (I : FullTupleInterpretation L L' k) (v : Vocabulary L) (v' : Vocabulary L') {a : EncodedStructure} (hk : 0 < k) (ha : v.WellFormed a) [Fact (2 ≤ a.1)] : (language L').Equiv (I.toInterpretation.Model (Fin a.1)) (Fin (I.encodedMap v v' a).1)

The decoded output, with its own canonical numerics, is the interpreted full ordered structure. Its underlying numbering is the exact lexicographic rank, not an arbitrary input relation isomorphism.

theorem Cslib.Logic.FO.Ordered.FullTupleInterpretation.encodedModelEquiv_apply_val {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {k : ℕ} (I : FullTupleInterpretation L L' k) (v : Vocabulary L) (v' : Vocabulary L') {a : EncodedStructure} (hk : 0 < k) (ha : v.WellFormed a) [Fact (2 ≤ a.1)] (x : I.toInterpretation.Model (Fin a.1)) : ↑((I.encodedModelEquiv v v' hk ha) x) = lexRank ↑x

Every element retains its exact natural-number rank in the decoded target.