Cardinality words and full-word bit indices

The cardinality is obtained by adding one to a decoded maximum, without requiring the cardinality itself to be a source element. Bit positions are compared as whole radix words; neither the position nor a fixed chunk number must fit in one source element.

Main definitions

• Cslib.Logic.FO.Ordered.Radix.cardinality: the source cardinality as a radix word.
• Cslib.Logic.FO.Ordered.Radix.bitIndex: read a bit at a word-valued index.

Main results

• Cslib.Logic.FO.Ordered.Radix.realize_cardinality: exact cardinality, including its high digit.
• Cslib.Logic.FO.Ordered.Radix.realize_bitIndex: exact bit semantics and high-index rejection.

References

• N. Immerman, Descriptive Complexity, Exercise 1.33(3): the full-tuple application.

noncomputable def Cslib.Logic.FO.Ordered.Radix.cardinality (L : FirstOrder.Language) {α : Type u_1} {m : ℕ} (B : (language L).Term α) (N : Fin m → (language L).Term α) : (language L).Formula α

Represent the source cardinality by decoding max and adding one in the word domain.

noncomputable def Cslib.Logic.FO.Ordered.Radix.bitIndex (L : FirstOrder.Language) {α : Type u_1} {d : ℕ} (B e : (language L).Term α) (x y : Fin d → (language L).Term α) : (language L).Formula α

A fixed disjunction selects a chunk; base-one conversion builds its full index r*e+b.

theorem Cslib.Logic.FO.Ordered.Radix.realize_cardinality {L : FirstOrder.Language} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] {α : Type u_1} {m : ℕ} (B : (language L).Term α) (N : Fin m → (language L).Term α) (v : α → Fin n) (hB : 1 < ↑(FirstOrder.Language.Term.realize v B)) (hBn : ↑(FirstOrder.Language.Term.realize v B) ^ 3 < n) : (cardinality L B N).Realize v ↔ (∀ (i : Fin m), ↑(FirstOrder.Language.Term.realize v (N i)) < ↑(FirstOrder.Language.Term.realize v B)) ∧ Nat.ofDigits (↑(FirstOrder.Language.Term.realize v B)) (List.ofFn fun (i : Fin m) => ↑(FirstOrder.Language.Term.realize v (N i))) = n

When 1 < B and B ^ 3 fits in the universe, cardinality L B N holds exactly when N is a radix-B word whose value is the universe size n, including its high digit.

theorem Cslib.Logic.FO.Ordered.Radix.realize_bitIndex {L : FirstOrder.Language} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] {α : Type u_1} {d : ℕ} (B e : (language L).Term α) (x y : Fin d → (language L).Term α) (v : α → Fin n) (he : 0 < ↑(FirstOrder.Language.Term.realize v e)) (hBe : ↑(FirstOrder.Language.Term.realize v B) = 2 ^ ↑(FirstOrder.Language.Term.realize v e)) (hBn : ↑(FirstOrder.Language.Term.realize v B) ^ 3 < n) (hx : ∀ (i : Fin d), ↑(FirstOrder.Language.Term.realize v (x i)) < ↑(FirstOrder.Language.Term.realize v B)) (hy : ∀ (i : Fin d), ↑(FirstOrder.Language.Term.realize v (y i)) < ↑(FirstOrder.Language.Term.realize v B)) : (bitIndex L B e x y).Realize v ↔ (Nat.ofDigits (↑(FirstOrder.Language.Term.realize v B)) (List.ofFn fun (i : Fin d) => ↑(FirstOrder.Language.Term.realize v (x i)))).testBit (Nat.ofDigits (↑(FirstOrder.Language.Term.realize v B)) (List.ofFn fun (i : Fin d) => ↑(FirstOrder.Language.Term.realize v (y i)))) = true

For a radix B = 2 ^ e with 0 < e and B ^ 3 in the universe, and radix-B words x and y, bitIndex L B e x y holds exactly when bit y of x is set.