Fields: reading a packed number out of one element

An element of a finite ordered universe carries log n bits, and both halves of Immerman's mutual definability pack several numbers into one such element: the packing argument for DescriptiveComplexity.PowArithDef writes the doubling chain's exponents side by side, and the Bit Sum Lemma writes a running sum after each segment. What both need first is a way to read one of those numbers back, and that is what this file gives:

DescriptiveComplexity.FieldAt p q x m: the bits of x from the place value p (included) up to the place value q (excluded), read as the number m.

The definition is a division with remainder written flat – x = lo + m * p + hi * q with lo < p and m * p < q – so every witness is at most x, hence a rank of the universe, and the whole thing is a formula of FO(≤, +, ×) (DescriptiveComplexity.arithDef_fieldAt). That is the same trick that makes DescriptiveComplexity.BitAt first-order, one field wide instead of one bit: DescriptiveComplexity.fieldAt_two_pow_succ is the bit as a one-bit field.

What to prove with it

DescriptiveComplexity.fieldAt_iff reads the field as x / 2 ^ a % 2 ^ (b - a), DescriptiveComplexity.fieldAt_unique makes it a function, and DescriptiveComplexity.exists_fieldAt says the value is always there to be read. A construction that lays numbers out in an element states its layout with FieldAt and never touches a bit again.

Fields of a natural number

theorem DescriptiveComplexity.field_iff (x m a d : ℕ) : (∃ (lo : ℕ) (hi : ℕ), lo + (m * 2 ^ a + hi * 2 ^ (a + d)) = x ∧ lo < 2 ^ a ∧ m * 2 ^ a < 2 ^ (a + d)) ↔ m = x / 2 ^ a % 2 ^ d

A field is a division with remainder, twice: m is the block of bits of x from position a to position b exactly when x splits as a low part below 2 ^ a, the block scaled by 2 ^ a, and a high part scaled by 2 ^ b. Every witness of the left-hand side is at most x, which is what makes the statement survive the truncation of a finite universe.

Fields of an element

theorem DescriptiveComplexity.lt_of_orank_lt {A : Type} [LinearOrder A] [Finite A] {x y : A} (h : orank x < orank y) : x < y

The order of the elements is the order of their ranks.

def DescriptiveComplexity.FieldAt {A : Type} [LinearOrder A] (p q x m : A) : Prop

The field of x between the place values p and q, read as the number m: the flat form of “the bits of x from p up to q”. All three witnesses are at most x, hence ranks of the universe.

Equations

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

theorem DescriptiveComplexity.fieldAt_iff {A : Type} [LinearOrder A] [Finite A] {p q x m : A} {a d : ℕ} (hp : orank p = 2 ^ a) (hq : orank q = 2 ^ (a + d)) : FieldAt p q x m ↔ orank m = orank x / 2 ^ a % 2 ^ d

What a field reads: at place values 2 ^ a and 2 ^ (a + d), the field of x is the d bits of x above position a.

theorem DescriptiveComplexity.fieldAt_unique {A : Type} [LinearOrder A] [Finite A] {p q x m m' : A} {a d : ℕ} (hp : orank p = 2 ^ a) (hq : orank q = 2 ^ (a + d)) (h : FieldAt p q x m) (h' : FieldAt p q x m') : m = m'

A field is a function of its two ends: at most one element reads it.

theorem DescriptiveComplexity.exists_fieldAt {A : Type} [LinearOrder A] [Finite A] {p q x : A} {a d : ℕ} (hp : orank p = 2 ^ a) (hq : orank q = 2 ^ (a + d)) : ∃ (m : A), FieldAt p q x m

A field is always there to be read: its value is below 2 ^ d ≤ q, hence a rank of the universe.

theorem DescriptiveComplexity.fieldAt_two_pow_succ {A : Type} [LinearOrder A] [Finite A] {p q x m : A} {a : ℕ} (hp : orank p = 2 ^ a) (hq : orank q = 2 ^ (a + 1)) : FieldAt p q x m ↔ if (orank x).testBit a = true then orank m = 1 else orank m = 0

A one-bit field is a bit: between a place value and its double, the field of x is 1 exactly where DescriptiveComplexity.BitAt holds.

Definability

theorem DescriptiveComplexity.arithDef_fieldAt {L : FirstOrder.Language} {α : Type} (p q x m : α) : ArithDef fun (x_1 : Type) (x_2 : L.Structure x_1) (x_3 : LinearOrder x_1) (x_4 : Finite x_1) (x_5 : Nonempty x_1) (v : α → x_1) => FieldAt (v p) (v q) (v x) (v m)

A field is first-order in ≤, + and ×: two guessed witnesses, two products and two sums, with no bit in sight. This is the reading primitive both halves of Immerman's mutual definability write their layouts with.