First-order access to the native structure encoding

The canonical power structure supplies the original relation tables and their domains. Native ordered arithmetic defines the length and every bit of encStructure directly, without guessing auxiliary relations. The power universe must contain the complete encoded word and its endpoint.

The machine input is the existing unary-cardinality, framed-table encoding. Numeric symbols of the power universe have their canonical meanings, rather than being extra input tables.

Main definitions

• Cslib.Logic.Vocabulary.inputLength: the endpoint of the raw native input encoding.
• Cslib.Logic.Vocabulary.inputBit: the set bits of the raw native input encoding.

Main results

• Cslib.Logic.Vocabulary.realize_inputLength, Cslib.Logic.Vocabulary.realize_inputBit: exact length and bit semantics, uniformly over sufficiently large power universes.

References

• N. Immerman, Relational Queries Computable in Polynomial Time, Section 3, Lemma 3.1: first-order definition of the machine's input. The construction here uses the library's framed encoding and canonical BIT arithmetic.

noncomputable def Cslib.Logic.Vocabulary.inputLength {L : FirstOrder.Language} (v : Vocabulary L) : (FO.Ordered.language v.powerLanguage).Formula (Fin 1)

The length of the native source-only encoding, inside the canonically ordered power domain.

noncomputable def Cslib.Logic.Vocabulary.inputBit {L : FirstOrder.Language} (v : Vocabulary L) : (FO.Ordered.language v.powerLanguage).Formula (Fin 1)

A set bit of the native source-only encoding. Positions outside the encoded word are false.

theorem Cslib.Logic.Vocabulary.realize_inputLength {L : FirstOrder.Language} (v : Vocabulary L) {a : EncodedStructure} (ha : v.WellFormed a) {B : ℕ} [Fact (2 ≤ B)] (hB : (encStructure a).length < B) (p : Fin B) : v.inputLength.Realize ![p] ↔ (encStructure a).length = ↑p

The direct first-order length formula equals the length of the native machine input. The endpoint must be an element of the canonical power universe.

theorem Cslib.Logic.Vocabulary.realize_inputBit {L : FirstOrder.Language} (v : Vocabulary L) {a : EncodedStructure} (ha : v.WellFormed a) {B : ℕ} [Fact (2 ≤ B)] (hB : (encStructure a).length < B) (p : Fin B) : v.inputBit.Realize ![p] ↔ (encStructure a)[↑p]? = some true

The direct first-order input-bit formula recognizes precisely the set bits of the existing native machine encoding, including its frame markers and rejecting terminators and padding.