Binary numbers as sets of positions, and sweeps along an order

The semantic layer of the normal form of FP (DescriptiveComplexity.Counting.Digits): no formula appears here.

• Carries: DescriptiveComplexity.Digits.testBit_add_iff reads a binary digit of a sum off the digits of the summands, the carry being given by lookahead (DescriptiveComplexity.Digits.Carry) rather than by a ripple – a condition with one existential and one universal quantifier over positions, hence first-order over an ordered set of positions.
• Numbers over a finite linear order P of positions: DescriptiveComplexity.Digits.bitsOf N is the set of positions whose rank (DescriptiveComplexity.orank) is a digit 1 of N. Only the digits of rank below the number of positions are seen, so this is N modulo 2 ^ |P| (DescriptiveComplexity.Digits.bitsOf_congr), and addition, doubling and the choice between a number and zero are operations on such sets with no side condition.
• Sweeps (DescriptiveComplexity.Digits.sweep_stage): a family of rows indexed by a finite linear order, each a function of the rows before it, is computed by an inflationary iteration that marks a row done in the very step that writes it, and writes a row only when the previous one is done and it is not itself. A row is thus written once, in full, from rows that are complete – which is what lets its defining condition be an arbitrary one, negations included.

Carries

def DescriptiveComplexity.Digits.Carry (M N i : ℕ) : Prop

The carry into the digit of rank i of M + N, by lookahead: some lower rank generates a carry, and every rank in between propagates it.

Equations

• DescriptiveComplexity.Digits.Carry M N i = ∃ k < i, M.testBit k = true ∧ N.testBit k = true ∧ ∀ (l : ℕ), k < l → l < i → M.testBit l = true ∨ N.testBit l = true

theorem DescriptiveComplexity.Digits.testBit_add_iff (M N i : ℕ) : (M + N).testBit i = true ↔ Xor (Xor (M.testBit i = true) (N.testBit i = true)) (Carry M N i)

A digit of a sum: the exclusive or of the digits of the summands and of the carry.

Numbers over a finite linear order of positions

def DescriptiveComplexity.Digits.bitsOf {P : Type} [LinearOrder P] (N : ℕ) (p : P) : Prop

The positions holding a digit 1 of N, the rank of a position being the rank of its digit.

Equations

• DescriptiveComplexity.Digits.bitsOf N p = (N.testBit (DescriptiveComplexity.orank p) = true)

theorem DescriptiveComplexity.Digits.bitsOf_congr {P : Type} [LinearOrder P] [Finite P] {M N : ℕ} (h : M % 2 ^ Nat.card P = N % 2 ^ Nat.card P) : bitsOf M = bitsOf N

Only the digits of rank below the number of positions are seen.

Sums and products along an order

noncomputable def DescriptiveComplexity.Digits.sumUpTo {I : Type} [LinearOrder I] (f : I → ℕ) (u : I) : ℕ

The sum of a family up to an index.

Equations

• DescriptiveComplexity.Digits.sumUpTo f u = ∑ᶠ (u' : I), if u' ≤ u then f u' else 0

noncomputable def DescriptiveComplexity.Digits.prodBefore {I : Type} [LinearOrder I] (f : I → ℕ) (u : I) : ℕ

The product of a family strictly before an index.

Equations

• DescriptiveComplexity.Digits.prodBefore f u = ∏ᶠ (u' : I), if u' < u then f u' else 1

theorem DescriptiveComplexity.Digits.sumUpTo_top {I : Type} [LinearOrder I] (f : I → ℕ) {u : I} (hu : ∀ (c : I), c ≤ u) : sumUpTo f u = ∑ᶠ (u' : I), f u'

theorem DescriptiveComplexity.Digits.prodBefore_bot {I : Type} [LinearOrder I] (f : I → ℕ) {u : I} (hu : ∀ (c : I), u ≤ c) : prodBefore f u = 1

Reading a number back from its digits

Sweeps

theorem DescriptiveComplexity.Digits.sweep_stage {W Idx Pos : Type} [LinearOrder Idx] [Finite Idx] (Φ : W → Idx → (Idx → Pos → Prop) → Pos → Prop) (T : W → Idx → Pos → Prop) (hΦ : ∀ (w : W) (i : Idx) (R : Idx → Pos → Prop), (∀ i' < i, R i' = T w i') → Φ w i R = T w i) (Dn : ℕ → W → Idx → Prop) (Rw : ℕ → W → Idx → Pos → Prop) (hD0 : ∀ (w : W) (i : Idx), ¬Dn 0 w i) (hR0 : ∀ (w : W) (i : Idx) (p : Pos), ¬Rw 0 w i p) (hD : ∀ (s : ℕ) (w : W) (i : Idx), Dn (s + 1) w i ↔ Dn s w i ∨ (∀ (a : Idx), i ≤ a) ∨ ∃ (i₀ : Idx), i₀ ⋖ i ∧ Dn s w i₀) (hR : ∀ (s : ℕ) (w : W) (i : Idx) (p : Pos), Rw (s + 1) w i p ↔ Rw s w i p ∨ ¬Dn s w i ∧ ((∀ (a : Idx), i ≤ a) ∨ ∃ (i₀ : Idx), i₀ ⋖ i ∧ Dn s w i₀) ∧ Φ w i (Rw s w) p) (s : ℕ) (w : W) (i : Idx) : (Dn s w i ↔ orank i < s) ∧ ∀ (p : Pos), Rw s w i p ↔ orank i < s ∧ T w i p

The stages of a sweep. Rows T w i indexed by a finite linear order, each determined by the rows before it through Φ, are computed by the iteration whose step marks a row done when it is the first or follows a done one, and writes a row under the same condition when it is not yet done: after s steps, the rows of rank below s are done and written, and nothing else is.

theorem DescriptiveComplexity.Digits.sweep_limit {W Idx Pos : Type} [LinearOrder Idx] [Finite Idx] (Φ : W → Idx → (Idx → Pos → Prop) → Pos → Prop) (T : W → Idx → Pos → Prop) (hΦ : ∀ (w : W) (i : Idx) (R : Idx → Pos → Prop), (∀ i' < i, R i' = T w i') → Φ w i R = T w i) (Dn : ℕ → W → Idx → Prop) (Rw : ℕ → W → Idx → Pos → Prop) (hD0 : ∀ (w : W) (i : Idx), ¬Dn 0 w i) (hR0 : ∀ (w : W) (i : Idx) (p : Pos), ¬Rw 0 w i p) (hD : ∀ (s : ℕ) (w : W) (i : Idx), Dn (s + 1) w i ↔ Dn s w i ∨ (∀ (a : Idx), i ≤ a) ∨ ∃ (i₀ : Idx), i₀ ⋖ i ∧ Dn s w i₀) (hR : ∀ (s : ℕ) (w : W) (i : Idx) (p : Pos), Rw (s + 1) w i p ↔ Rw s w i p ∨ ¬Dn s w i ∧ ((∀ (a : Idx), i ≤ a) ∨ ∃ (i₀ : Idx), i₀ ⋖ i ∧ Dn s w i₀) ∧ Φ w i (Rw s w) p) (w : W) (i : Idx) (p : Pos) : (∃ (s : ℕ), Rw s w i p) ↔ T w i p

The limit of a sweep: every row is eventually written, and written right.