The arithmetic a sweep can do: comparison and addition, bit by bit

The base of a machine of DescriptiveComplexity.LogTime.Machine never evaluates a numeric predicate; if it is to compare or to add, it has to build the operation out of bits. This file does so, and the two constructions are the bit-level analogues of DescriptiveComplexity.HeadArith's plusP one resource bound higher:

• DescriptiveComplexity.leSweep – the comparison, one state bit carrying the verdict on the positions read so far, overwritten whenever the two registers differ (DescriptiveComplexity.leSweep_accepts);
• DescriptiveComplexity.plusSweep – the ripple-carry addition, one state bit for the carry and one for “every output bit has matched so far”, accepting when the last carry is out and nothing mismatched (DescriptiveComplexity.plusSweep_accepts).

Both are single passes from the lowest position upwards, both use a constant number of state bits, and neither reads the instance – so the machine model is not vacuous: the order and the addition of the numeric predicates are computed by it, from bits alone.

Where the arithmetic stops

Multiplication is not here, and not for lack of effort: a sweep carries a constant number of bits past each position, whereas the schoolbook product of two log n-bit numbers accumulates a column count that grows with the number of positions. That boundary is the honest limit of a sweep, and it is why the model has a second primitive that is not one: DescriptiveComplexity.BaseTest.bit reads a bit at an address instead of computing anything. Eliminating × in favor of that read is the classical theorem the model waits on, not a widening of this file; see DescriptiveComplexity.LogTime.

Peeling a bit off a remainder

theorem DescriptiveComplexity.mod_two_pow_succ (x k : ℕ) : x % 2 ^ (k + 1) = x % 2 ^ k + if x.testBit k = true then 2 ^ k else 0

The remainder modulo the next power of two adds one bit.

theorem DescriptiveComplexity.orank_mod_two_pow_posCount {A : Type} [LinearOrder A] [Finite A] (a : A) : orank a % 2 ^ posCount A = orank a

A rank is its own remainder modulo the place value above the top position.

Comparison

@[reducible]

def DescriptiveComplexity.leSweep : Sweep 2

The comparison sweep: one state bit, holding the verdict on the positions read so far. A position where the registers differ overwrites it; a position where they agree keeps it. Read from the lowest position upwards, the verdict left at the end is the comparison of the two registers.

Equations

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

theorem DescriptiveComplexity.leSweep_state {A : Type} [LinearOrder A] (x : Fin 2 → A) (i : ℕ) : leSweep.state x i 0 = true ↔ orank (x 0) % 2 ^ i ≤ orank (x 1) % 2 ^ i

The invariant of the comparison sweep: after the positions below i, the state bit compares the two registers modulo 2 ^ i.

theorem DescriptiveComplexity.leSweep_accepts {A : Type} [LinearOrder A] [Finite A] (x : Fin 2 → A) : leSweep.Accepts x ↔ x 0 ≤ x 1

The comparison sweep decides the order: the machine model computes ≤, from bits alone.

Addition

@[reducible]

def DescriptiveComplexity.plusSweep : Sweep 3

The ripple-carry addition sweep: state bit 0 is the carry, state bit 1 records that every output bit has matched the third register so far. The sweep accepts when nothing has mismatched and the last carry is out – which is the statement that the sum does not overflow the universe.

Equations

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

theorem DescriptiveComplexity.plusSweep_carry {A : Type} [LinearOrder A] (x : Fin 3 → A) (i : ℕ) : plusSweep.state x i 0 = true ↔ 2 ^ i ≤ orank (x 0) % 2 ^ i + orank (x 1) % 2 ^ i

The carry of the addition sweep is the carry of the two remainders.

theorem DescriptiveComplexity.carry_succ (a b i : ℕ) : 2 ^ (i + 1) ≤ a % 2 ^ (i + 1) + b % 2 ^ (i + 1) ↔ a.testBit i = true ∧ b.testBit i = true ∨ (a.testBit i = true ∨ b.testBit i = true) ∧ 2 ^ i ≤ a % 2 ^ i + b % 2 ^ i

theorem DescriptiveComplexity.carry_iff_lookahead (a b i : ℕ) : 2 ^ i ≤ a % 2 ^ i + b % 2 ^ i ↔ ∃ j < i, a.testBit j = true ∧ b.testBit j = true ∧ ∀ (k : ℕ), j < k → k < i → a.testBit k = true ∨ b.testBit k = true

The carry is a lookahead condition: the arithmetic carry into position i – the one plusSweep computes with a single state bit – is “some lower position generates a carry, and every position between it and i propagates one”. That is a first-order condition on the bits alone, with no addition in it, which is what makes + a derived predicate of the bit-level logic rather than an atom of it (DescriptiveComplexity.BitAtom.plus is kept all the same: plusSweep_accepts is half of what shows the model has to build its arithmetic instead of reading it).

theorem DescriptiveComplexity.add_mod_iff_bits (a b c i : ℕ) : (a % 2 ^ i + b % 2 ^ i = c % 2 ^ i + if 2 ^ i ≤ a % 2 ^ i + b % 2 ^ i then 2 ^ i else 0) ↔ ∀ j < i, c.testBit j = true ↔ ((a.testBit j = true ↔ b.testBit j = true) ↔ 2 ^ j ≤ a % 2 ^ j + b % 2 ^ j)

The bitwise reading of an addition: the low i bits of a + b agree with those of c – up to the carry leaving position i – exactly when the full-adder equation holds at every position below i. The equation is written as an iff-chain, which for three propositions is the parity of their truth values, that is, the exclusive or of the two input bits and the carry.

theorem DescriptiveComplexity.plusSweep_carry_true {A : Type} [LinearOrder A] (x : Fin 3 → A) (i : ℕ) (h : 2 ^ i ≤ orank (x 0) % 2 ^ i + orank (x 1) % 2 ^ i) : plusSweep.state x i 0 = true

The carry bit is set when the remainders overflow.

theorem DescriptiveComplexity.plusSweep_carry_false {A : Type} [LinearOrder A] (x : Fin 3 → A) (i : ℕ) (h : ¬2 ^ i ≤ orank (x 0) % 2 ^ i + orank (x 1) % 2 ^ i) : plusSweep.state x i 0 = false

The carry bit is clear when the remainders do not overflow.

theorem DescriptiveComplexity.plusSweep_ok {A : Type} [LinearOrder A] (x : Fin 3 → A) (i : ℕ) : plusSweep.state x i 1 = true ↔ orank (x 0) % 2 ^ i + orank (x 1) % 2 ^ i = orank (x 2) % 2 ^ i + if 2 ^ i ≤ orank (x 0) % 2 ^ i + orank (x 1) % 2 ^ i then 2 ^ i else 0

The match bit of the addition sweep records that the two remainders add up, up to the carry it has produced.

theorem DescriptiveComplexity.plusSweep_accepts {A : Type} [LinearOrder A] [Finite A] (x : Fin 3 → A) : plusSweep.Accepts x ↔ orank (x 0) + orank (x 1) = orank (x 2)

The addition sweep decides addition: the machine model computes the numeric predicate plus, from bits alone – the bit-level analogue of the head program DescriptiveComplexity.HeadProgram.plusP.

The trivial sweep

@[reducible]

def DescriptiveComplexity.trueSweep : Sweep 0

The trivial sweep: no state, no register, always accepting. It is what a constant of the bit-level logic compiles to, so that a trivially true kernel needs no dummy variable.

Equations

• DescriptiveComplexity.trueSweep = { σ := 0, init := Fin.elim0, step := Fin.elim0, acc := DescriptiveComplexity.BitExpr.tt }