Native access to packed bit-sum trees

Eight first-order variables represent eight fixed-width bit strings. Their access formula uses a fixed disjunction and fixed chains of PLUS formulas, never a variable multiplication relation. The tree address uses the proved exact shift formula. Node decoding constrains all bits above the node's level to zero.

Main definitions

• Cslib.Logic.FO.Ordered.BitSum.treeAddress: native bit-plane addressing.
• Cslib.Logic.FO.Ordered.BitSum.packedBit: native access to eight packed words.
• Cslib.Logic.FO.Ordered.BitSum.nodeValue: decoding a node's entire value.

Main results

• Cslib.Logic.FO.Ordered.BitSum.realize_treeAddress: exact natural-number addresses.
• Cslib.Logic.FO.Ordered.BitSum.realize_packedBit: exact fixed-width word access.
• Cslib.Logic.FO.Ordered.BitSum.realize_nodeValue: exact decoding, including high zero bits.
• Cslib.Logic.FO.Ordered.BitSum.encodesNode_sumTree: constructed witnesses encode every node.

References

• N. Immerman, Descriptive Complexity, Lemma 1.18, historically due to Barrington, Immerman and Straubing. This module uses the balanced-tree packing variant.

noncomputable def Cslib.Logic.FO.Ordered.BitSum.treeAddress (L : FirstOrder.Language) {α : Type u_1} (m j b q a : (language L).Term α) : (language L).Formula α

A bit-plane address, using only PLUS, a literal three, and an exact binary shift.

noncomputable def Cslib.Logic.FO.Ordered.BitSum.packedBit (L : FirstOrder.Language) {α : Type u_1} (h : (language L).Term α) (w : Fin 8 → (language L).Term α) (a : (language L).Term α) : (language L).Formula α

Read an address in eight fixed-width words. The eight scales are syntactic literals.

noncomputable def Cslib.Logic.FO.Ordered.BitSum.nodeValue (L : FirstOrder.Language) {α : Type u_1} (m h : (language L).Term α) (w : Fin 8 → (language L).Term α) (j q z : (language L).Term α) : (language L).Formula α

Decode the whole node value, explicitly zeroing all bits above its level.

def Cslib.Logic.FO.Ordered.BitSum.EncodesNode (m h : ℕ) (w : Fin 8 → ℕ) (j q z : ℕ) : Prop

The explicit bitwise meaning of the packed node decoder.

theorem Cslib.Logic.FO.Ordered.BitSum.EncodesNode.unique {m h : ℕ} {w : Fin 8 → ℕ} {j q z z' : ℕ} (hz : EncodesNode m h w j q z) (hz' : EncodesNode m h w j q z') : z = z'

A packed node has at most one value, including all its high bits.

theorem Cslib.Logic.FO.Ordered.BitSum.encodesNode_sumTree (f : ℕ → Bool) {m h j q : ℕ} (hspace : 4 * 2 ^ m ≤ 8 * h) (hj : j ≤ m) (hq : q < 2 ^ (m - j)) : EncodesNode m h (BitString.sumTreeWords f m h) j q (BitString.sumTree f j q)

The actual packed tree decodes to the actual sum at every valid node.

@[simp]

theorem Cslib.Logic.FO.Ordered.BitSum.realize_treeAddress {L : FirstOrder.Language} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] {α : Type u_1} (m j b q a : (language L).Term α) (v : α → Fin n) : (treeAddress L m j b q a).Realize v ↔ ↑(FirstOrder.Language.Term.realize v j) ≤ ↑(FirstOrder.Language.Term.realize v m) ∧ BitString.sumTreeAddress ↑(FirstOrder.Language.Term.realize v m) ↑(FirstOrder.Language.Term.realize v j) ↑(FirstOrder.Language.Term.realize v b) ↑(FirstOrder.Language.Term.realize v q) = ↑(FirstOrder.Language.Term.realize v a)

treeAddress L m j b q a holds exactly when j ≤ m and a is the address BitString.sumTreeAddress m j b q.

@[simp]

theorem Cslib.Logic.FO.Ordered.BitSum.realize_packedBit {L : FirstOrder.Language} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] {α : Type u_1} (h : (language L).Term α) (w : Fin 8 → (language L).Term α) (a : (language L).Term α) (v : α → Fin n) : (packedBit L h w a).Realize v ↔ ∃ (r : Fin 8) (b : Fin n), ↑r * ↑(FirstOrder.Language.Term.realize v h) + ↑b = ↑(FirstOrder.Language.Term.realize v a) ∧ ↑b < ↑(FirstOrder.Language.Term.realize v h) ∧ (↑(FirstOrder.Language.Term.realize v (w r))).testBit ↑b = true

packedBit L h w a holds exactly when position a falls in one of the eight words w, of width h, at a set bit.

theorem Cslib.Logic.FO.Ordered.BitSum.realize_nodeValue {L : FirstOrder.Language} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] {α : Type u_1} (m h : (language L).Term α) (w : Fin 8 → (language L).Term α) (j q z : (language L).Term α) (v : α → Fin n) (hj : ↑(FirstOrder.Language.Term.realize v j) ≤ ↑(FirstOrder.Language.Term.realize v m)) (hspace : 8 * ↑(FirstOrder.Language.Term.realize v h) < n) : (nodeValue L m h w j q z).Realize v ↔ EncodesNode (↑(FirstOrder.Language.Term.realize v m)) (↑(FirstOrder.Language.Term.realize v h)) (fun (r : Fin 8) => ↑(FirstOrder.Language.Term.realize v (w r))) ↑(FirstOrder.Language.Term.realize v j) ↑(FirstOrder.Language.Term.realize v q) ↑(FirstOrder.Language.Term.realize v z)

When j ≤ m and eight words of width h fit in the universe, nodeValue L m h w j q z holds exactly when the words encode the value z at node j (EncodesNode).