The native Bit Sum formula

The Bit Sum Lemma states that the number of set bits of a natural-number index is first-order definable from order and BIT. The construction here encodes an entire balanced addition tree in eight element variables and checks every node using the native PLUS formula. The bit-plane layout needs only exact shifts and fixed literal multiples, never a multiplication predicate.

The packed witnesses are constructed for every universe of size at least 257. A fixed finite formula handles all smaller input numerals, giving one formula for every canonical Fin n, n ≥ 2, including non-power-of-two sizes. Native TIMES and full-tuple BIT build on this prerequisite in Ordered.Multiplication and Ordered.TupleBit.

Main definitions

• Cslib.Logic.FO.Ordered.bitSum: a single native formula counting set bits.

Main results

• Cslib.Logic.FO.Ordered.realize_bitSum: exact natural-number bit-count semantics.
• Cslib.Logic.FO.Ordered.existsUnique_bitSum: every input has exactly one output.

References

• N. Immerman, Descriptive Complexity, Lemma 1.18 (Bit Sum Lemma), a prerequisite for Theorem 1.17(1). The historical notes credit Barrington, Immerman and Straubing; see also Barrington, Immerman and Straubing. The balanced-tree bit-plane packing here is a proved variant of the source's packed running-sum construction, not a transcription of its proof.

noncomputable def Cslib.Logic.FO.Ordered.bitSum (L : FirstOrder.Language) : (language L).Formula (Fin 2)

The number of set bits, defined uniformly from canonical order and BIT.

@[simp]

theorem Cslib.Logic.FO.Ordered.realize_bitSum {L : FirstOrder.Language} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] (v : Fin 2 → Fin n) : (bitSum L).Realize v ↔ ↑(v 1) = (↑(v 0)).bitIndices.length

The native Bit Sum formula counts all set bits, for every canonical universe size.

theorem Cslib.Logic.FO.Ordered.existsUnique_bitSum {L : FirstOrder.Language} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] (x : Fin n) : ∃! y : Fin n, (bitSum L).Realize ![x, y]

The bit count always fits in the input's universe and is uniquely defined.