Native BIT on arbitrary-base full tuples

Fixed-length radix words represent the ranks of both input tuples, including indices larger than the source universe. The radix is a witnessed power of two with its cube in the source universe. Seven radix digits represent the source cardinality; 7 * k digits represent each rank. Native word arithmetic converts the original base without modular overflow. A fixed finite disjunction covers source sizes two through eight.

Main definitions

• Cslib.Logic.FO.Ordered.tupleBit: native BIT on the full lexicographically numbered tuple universe. Its syntax depends on the dimension, never on the source cardinality.

Main results

• Cslib.Logic.FO.Ordered.realize_tupleBit: exact BIT of natural-number lexicographic ranks.
• Cslib.Logic.FO.Ordered.not_realize_tupleBit_of_lt: rejection beyond the binary extent.

References

• N. Immerman, Descriptive Complexity, Remark 1.32 and Exercise 1.33(3). The source explicitly assumes the full tuple universe. The bounded radix-word construction here supplies that exercise's native numeric lifting; it makes no formula-size efficiency claim. Restricted tuple domains and numeric-preserving interpretation composition are separate obligations. Dimension zero is explicitly false, without claiming a canonical size-one target.

noncomputable def Cslib.Logic.FO.Ordered.TupleBit.parameters (L : FirstOrder.Language) {α : Type u_1} (e B : (language L).Term α) : (language L).Formula α

Parameter conditions for the binary radix B = 2 ^ e with e ≥ 1 and B ^ 3 < n.

noncomputable def Cslib.Logic.FO.Ordered.TupleBit.radixFormula (L : FirstOrder.Language) (k : ℕ) : (language L).Formula (Fin 2 × Fin k)

Radix-word BIT formula for source sizes n > 8.

noncomputable def Cslib.Logic.FO.Ordered.TupleBit.smallFormula (L : FirstOrder.Language) (k : ℕ) : (language L).Formula (Fin 2 × Fin k)

Finite disjunction BIT formula for small source sizes 2 ≤ n ≤ 8.

noncomputable def Cslib.Logic.FO.Ordered.tupleBit (L : FirstOrder.Language) (k : ℕ) : (language L).Formula (Fin 2 × Fin k)

Native BIT of full-tuple lexicographic ranks, uniformly over every canonical Fin n, n ≥ 2. The zero-dimensional formula is false; no canonical numeric structure on a singleton is claimed.

@[simp]

theorem Cslib.Logic.FO.Ordered.realize_tupleBit {L : FirstOrder.Language} {n k : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] (v : Fin 2 × Fin k → Fin n) : (tupleBit L k).Realize v ↔ (lexRank fun (i : Fin k) => v (0, i)).testBit (lexRank fun (i : Fin k) => v (1, i)) = true

Exact rank semantics for all source sizes, including non-powers of two and high indices.

theorem Cslib.Logic.FO.Ordered.not_realize_tupleBit_of_lt {L : FirstOrder.Language} {n k : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] (v : Fin 2 × Fin k → Fin n) (h : (lexRank fun (i : Fin k) => v (0, i)) < 2 ^ lexRank fun (i : Fin k) => v (1, i)) : ¬(tupleBit L k).Realize v

A bit index beyond the represented number's binary extent is rejected.