Binary numbers carried by a relation

The layer between DescriptiveComplexity.Numbers.Binary, which decodes a set of bits sitting on a genuine LinearOrder, and the problems carrying binary numbers, whose order is a relation symbol of the vocabulary and therefore an arbitrary binary relation until the yes-instances say otherwise.

• DescriptiveComplexity.IsLinOrd – being a linear order, as a property of a relation, first-order and foldable into the yes-instances;
• DescriptiveComplexity.bitRank – the rank of a position, the number of positions strictly below it, defined for an arbitrary relation;
• DescriptiveComplexity.binNum – the decoding ∑ 2 ^ rank, over a set of positions via finsum, so that it is total and needs no finiteness to be stated.

Everything transports along equivalences commuting with the relations, which is what the DecisionProblem.iso_invariant proofs of the group need.

The arithmetic the Σ₁ definitions need – that a bitwise ripple-carry chain computes an addition – is built on DescriptiveComplexity.binNum_peel_min, which peels the lowest position off a decoded number: binNum = bit at the bottom + 2 * (the rest), the recursion binary numbers actually satisfy. The same recursion gives the two facts a kernel needs about whole numbers rather than their bits: DescriptiveComplexity.binNum_inj_on, two numbers are equal exactly when their bits agree, and DescriptiveComplexity.binNum_lt_iff, one is smaller exactly when they differ and the higher bit is the second's – both bitwise, hence first-order, which is why a kernel can compare numbers it has guessed.

Linear orders, as a property of a relation

def DescriptiveComplexity.IsLinOrd {A : Type} (Le : A → A → Prop) : Prop

A binary relation is a linear order: reflexive, transitive, antisymmetric and total.

Equations

• DescriptiveComplexity.IsLinOrd Le = ((∀ (a : A), Le a a) ∧ (∀ (a b c : A), Le a b → Le b c → Le a c) ∧ (∀ (a b : A), Le a b → Le b a → a = b) ∧ ∀ (a b : A), Le a b ∨ Le b a)

theorem DescriptiveComplexity.IsLinOrd.of_equiv {A B : Type} (u : B ≃ A) {LeB : B → B → Prop} {LeA : A → A → Prop} (hle : ∀ (b b' : B), LeB b b' ↔ LeA (u b) (u b')) (h : IsLinOrd LeB) : IsLinOrd LeA

Linearity transports along an equivalence.

Building linear orders

Reductions into a problem carrying binary numbers have to construct the order of the instance they produce, and a Σ₁ certificate sometimes has to exhibit one. Both do it the same way: read the elements through a key into a lexicographic product of orders already at hand.

def DescriptiveComplexity.lexRel {α β : Type} (Ra : α → α → Prop) (Rb : β → β → Prop) : α × β → α × β → Prop

The lexicographic product of two relations.

Equations

• DescriptiveComplexity.lexRel Ra Rb u v = (Ra u.1 v.1 ∧ u.1 ≠ v.1 ∨ u.1 = v.1 ∧ Rb u.2 v.2)

theorem DescriptiveComplexity.isLinOrd_lexRel {α β : Type} {Ra : α → α → Prop} {Rb : β → β → Prop} (ha : IsLinOrd Ra) (hb : IsLinOrd Rb) : IsLinOrd (lexRel Ra Rb)

The lexicographic product of two linear orders is a linear order.

theorem DescriptiveComplexity.isLinOrd_of_key {M K : Type} {LeK : K → K → Prop} {R : M → M → Prop} (hK : IsLinOrd LeK) (key : M → K) (hinj : Function.Injective key) (h : ∀ (a b : M), R a b ↔ LeK (key a) (key b)) : IsLinOrd R

A relation read through an injective key into a linear order is a linear order.

@[instance_reducible]

noncomputable def DescriptiveComplexity.IsLinOrd.toLinearOrder {A : Type} {Le : A → A → Prop} (h : IsLinOrd Le) : LinearOrder A

A relation that is a linear order induces a LinearOrder structure, which is what Mathlib's order library asks for. Guessed orders – a schedule, a circuit – arrive as relations, so this is the bridge to it.

Equations

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

Decoding a set of positions

noncomputable def DescriptiveComplexity.bitRank {A : Type} (Le : A → A → Prop) (Posn : A → Prop) (p : A) : ℕ

The rank of a position: the number of positions strictly below it. This is the place value's exponent.

Equations

• DescriptiveComplexity.bitRank Le Posn p = {q : A | Posn q ∧ Le q p ∧ q ≠ p}.ncard

noncomputable def DescriptiveComplexity.binNum {A : Type} (Le : A → A → Prop) (Posn b : A → Prop) : ℕ

The number encoded by the set b of positions: ∑ 2 ^ rank.

Equations

• DescriptiveComplexity.binNum Le Posn b = ∑ᶠ (p : A) (_ : p ∈ {p : A | Posn p ∧ b p}), 2 ^ DescriptiveComplexity.bitRank Le Posn p

theorem DescriptiveComplexity.binNum_congr {A : Type} {Le : A → A → Prop} {Posn b b' : A → Prop} (h : ∀ (p : A), b p ↔ b' p) : binNum Le Posn b = binNum Le Posn b'

theorem DescriptiveComplexity.binNum_congr_on {A : Type} {Le : A → A → Prop} {Posn b b' : A → Prop} (h : ∀ (p : A), Posn p → (b p ↔ b' p)) : binNum Le Posn b = binNum Le Posn b'

Only the bits at positions matter.

@[simp]

theorem DescriptiveComplexity.binNum_bot {A : Type} (Le : A → A → Prop) (Posn : A → Prop) : (binNum Le Posn fun (x : A) => False) = 0

The value of the empty set of positions is zero.

theorem DescriptiveComplexity.binNum_equiv {A B : Type} (u : B ≃ A) {LeB : B → B → Prop} {PosnB bB : B → Prop} {LeA : A → A → Prop} {PosnA bA : A → Prop} (hle : ∀ (b b' : B), LeB b b' ↔ LeA (u b) (u b')) (hp : ∀ (b : B), PosnB b ↔ PosnA (u b)) (hb : ∀ (b : B), bB b ↔ bA (u b)) : binNum LeB PosnB bB = binNum LeA PosnA bA

The decoded number transports along an equivalence commuting with the three relations.

On a finite universe both are finite sums over Finsets, which is what a decoder computes. The Decidable arguments are what makes those Finsets constructible; nothing here needs the relations to be well-behaved.

Peeling the lowest position

theorem DescriptiveComplexity.binNum_peel_min {A : Type} [Finite A] {Le : A → A → Prop} {Posn b : A → Prop} {p₀ : A} (hlin : IsLinOrd Le) (h₀ : Posn p₀) (hmin : ∀ (q : A), Posn q → Le p₀ q) : binNum Le Posn b = (if b p₀ then 1 else 0) + 2 * binNum Le (fun (q : A) => Posn q ∧ q ≠ p₀) b

The recursion binary numbers satisfy: the value is the lowest bit plus twice the value of the rest.

The full adder

def DescriptiveComplexity.maj (x y z : Prop) : Prop

The majority of three propositions: the carry produced by a full adder.

Equations

• DescriptiveComplexity.maj x y z = (x ∧ y ∨ x ∧ z ∨ y ∧ z)

Ripple-carry addition

def DescriptiveComplexity.MinPos {A : Type} (Le : A → A → Prop) (Posn : A → Prop) (p : A) : Prop

p is a lowest position.

Equations

• DescriptiveComplexity.MinPos Le Posn p = (Posn p ∧ ∀ (q : A), Posn q → Le p q)

def DescriptiveComplexity.MaxPos {A : Type} (Le : A → A → Prop) (Posn : A → Prop) (p : A) : Prop

p is a highest position.

Equations

• DescriptiveComplexity.MaxPos Le Posn p = (Posn p ∧ ∀ (q : A), Posn q → Le q p)

def DescriptiveComplexity.SuccPos {A : Type} (Le : A → A → Prop) (Posn : A → Prop) (p q : A) : Prop

q is the next position above p.

Equations

• DescriptiveComplexity.SuccPos Le Posn p q = (Posn p ∧ Posn q ∧ Le p q ∧ p ≠ q ∧ ∀ (r : A), Posn r → Le p r → Le r q → r = p ∨ r = q)

theorem DescriptiveComplexity.IsLinOrd.reverse {A : Type} {Le : A → A → Prop} (hlin : IsLinOrd Le) : IsLinOrd fun (a b : A) => Le b a

The reverse of a linear order is a linear order.

theorem DescriptiveComplexity.exists_predPos {A : Type} [Finite A] {Le : A → A → Prop} {Posn : A → Prop} (hlin : IsLinOrd Le) {p : A} (hp : Posn p) (hmin : ¬MinPos Le Posn p) : ∃ (q : A), SuccPos Le Posn q p

Every position that is not the lowest has one immediately below it.

theorem DescriptiveComplexity.binNum_ripple {A : Type} [Finite A] {Le : A → A → Prop} (hlin : IsLinOrd Le) {a b s : A → Prop} (n : ℕ) (Posn c : A → Prop) (cin cout : Prop) : {p : A | Posn p}.ncard = n → (∀ (p : A), Posn p → (s p ↔ Xor (a p) (Xor (b p) (c p)))) → (∀ (p q : A), SuccPos Le Posn p q → (c q ↔ maj (a p) (b p) (c p))) → (∀ (p : A), MinPos Le Posn p → (c p ↔ cin)) → (∀ (p : A), MaxPos Le Posn p → (cout ↔ maj (a p) (b p) (c p))) → ((∀ (p : A), ¬Posn p) → (cout ↔ cin)) → (binNum Le Posn s + 2 ^ n * if cout then 1 else 0) = binNum Le Posn a + binNum Le Posn b + if cin then 1 else 0

Ripple-carry addition is addition. If s is the bitwise sum of a and b with carries c – each bit the exclusive or of the three, each carry the majority of the three below – then the decoded numbers add up, the carry in at the bottom and the carry out at the top accounting for the difference.

theorem DescriptiveComplexity.binNum_lt_two_pow {A : Type} [Finite A] {Le : A → A → Prop} (hlin : IsLinOrd Le) (n : ℕ) (Posn : A → Prop) : {p : A | Posn p}.ncard = n → ∀ (b : A → Prop), binNum Le Posn b < 2 ^ n

A decoded number is smaller than 2 to the number of positions.

theorem DescriptiveComplexity.exists_ripple {A : Type} [Finite A] {Le : A → A → Prop} (hlin : IsLinOrd Le) (n : ℕ) (Posn a b : A → Prop) (cin : Prop) : {p : A | Posn p}.ncard = n → (binNum Le Posn a + binNum Le Posn b + if cin then 1 else 0) < 2 ^ n → ∃ (s : A → Prop) (c : A → Prop), (∀ (p : A), Posn p → (s p ↔ Xor (a p) (Xor (b p) (c p)))) ∧ (∀ (p q : A), SuccPos Le Posn p q → (c q ↔ maj (a p) (b p) (c p))) ∧ (∀ (p : A), MinPos Le Posn p → (c p ↔ cin)) ∧ (∀ (p : A), MaxPos Le Posn p → ¬maj (a p) (b p) (c p)) ∧ binNum Le Posn s = binNum Le Posn a + binNum Le Posn b + if cin then 1 else 0

A ripple-carry certificate exists. Whenever the sum fits in the available positions, the bitwise sum and the carries that witness it can be produced – this is the certificate that the Σ₁ definition of a binary-weighted problem guesses.

theorem DescriptiveComplexity.binNum_inj_on {A : Type} [Finite A] {Le : A → A → Prop} (hlin : IsLinOrd Le) (n : ℕ) (Posn : A → Prop) : {p : A | Posn p}.ncard = n → ∀ (b b' : A → Prop), binNum Le Posn b = binNum Le Posn b' → ∀ (p : A), Posn p → (b p ↔ b' p)

The decoding is injective on the positions: two sets of bits with the same value agree wherever it matters.

theorem DescriptiveComplexity.binNum_lt_iff {A : Type} [Finite A] {Le : A → A → Prop} (hlin : IsLinOrd Le) (n : ℕ) (Posn : A → Prop) : {p : A | Posn p}.ncard = n → ∀ (b b' : A → Prop), binNum Le Posn b < binNum Le Posn b' ↔ ∃ (p : A), Posn p ∧ ¬b p ∧ b' p ∧ ∀ (q : A), Posn q → Le p q → q ≠ p → (b q ↔ b' q)

Comparison by the highest differing position: one decoded number is smaller than another exactly when there is a position carrying 0 in the first and 1 in the second above which the two agree. Unlike the value itself, this is a first-order reading of <, which is what a kernel comparing two guessed numbers writes.