The binary increment on a block's atoms

DescriptiveComplexity.Exponential.OrdFormula writes the order on an expanded universe as a first-order sentence over the base. Walking that universe needs one thing more: its covering relation, and the two endpoints of the order. An assignment is read as a binary number – the set of atoms it makes true, most significant at the smallest atom – so the immediate successor is the schoolchild's increment: find the greatest atom the assignment misses, put it in, and take out every atom above it.

This file proves that at the level of sets over a finite linearly ordered index (DescriptiveComplexity.setSucc_iff: the increment is the covering relation of DescriptiveComplexity.setLinearOrder), gives the two endpoints their sentences (DescriptiveComplexity.SOBlock.botAssignF, DescriptiveComplexity.SOBlock.topAssignF), and writes the increment down as a sentence over the base plus two copies of the block (DescriptiveComplexity.SOBlock.succAssignF), by the same quantification over positions that DescriptiveComplexity.SOBlock.ordLtF already uses.

The padding trap, and the honest atoms

A padded atom (DescriptiveComplexity.SOBlock.AtomIx) is a relation variable with a tuple of the block's maximal arity, of which DescriptiveComplexity.SOBlock.atomSet reads only the first B.arity i coordinates – so the sets in the image of atomSet are exactly the padding-invariant ones, and the binary increment of such a set is in general not one: it flips a single padded atom, while padding-invariance forces every padded atom with the same truncation to move together. The successor of an assignment is therefore not the increment of its padded atom set.

The order is unaffected – two assignments differ first at a padded atom exactly when they differ first at the real atom Σ i, Fin (B.arity i) → A it truncates to – and the honest atoms are what this file works with. Over them an assignment is an arbitrary subset (DescriptiveComplexity.SOBlock.realSet is a bijection), so the set-level increment applies unchanged, and DescriptiveComplexity.SOBlock.assignSucc_iff reads it back as the immediate successor in the order the expanded universe carries. The two indices are matched by DescriptiveComplexity.SOBlock.atomSet_lt_iff_realSet, whose whole content is that a real atom has a least padded representative – the tuple padded with the least element of A – so that comparing representatives is comparing real atoms.

Accordingly the sentence takes its lexicographic comparisons on the truncated selectors: DescriptiveComplexity.lexSelLtF accepts a selector of any width, so the atoms it compares are the real ones.

The increment, on subsets of a finite linear order

def DescriptiveComplexity.SetSucc {I : Type} [LinearOrder I] (S T : I → Prop) : Prop

The binary increment of a set: at some index the first is out and the second in, they agree strictly below it, and above it the first is in and the second out.

Equations

• DescriptiveComplexity.SetSucc S T = ∃ (p : I), (∀ q < p, S q ↔ T q) ∧ ¬S p ∧ T p ∧ ∀ (q : I), p < q → S q ∧ ¬T q

def DescriptiveComplexity.SetCovBy {I : Type} [LinearOrder I] [Finite I] (S T : I → Prop) : Prop

Covering in the binary-number order, spelled with the order as a plain relation: DescriptiveComplexity.setLinearOrder is not an instance, and the function type I → Prop carries a competing pointwise order of its own, so ⋖ would resolve to the wrong one.

Equations

• DescriptiveComplexity.SetCovBy S T = (S < T ∧ ∀ (U : I → Prop), S < U → ¬U < T)

theorem DescriptiveComplexity.setLinearOrder_bot_le {I : Type} [LinearOrder I] [Finite I] (S : I → Prop) : (fun (x : I) => False) ≤ S

Nothing is below the empty set: the order compares at the least differing index, where being out is being smaller.

theorem DescriptiveComplexity.setLinearOrder_le_top {I : Type} [LinearOrder I] [Finite I] (S : I → Prop) : S ≤ fun (x : I) => True

Nothing is above the full set.

theorem DescriptiveComplexity.setSucc_iff {I : Type} [LinearOrder I] [Finite I] (S T : I → Prop) : SetSucc S T ↔ SetCovBy S T

The increment is the covering relation of the binary-number order on subsets.

The honest atom index

An assignment is an arbitrary subset of the real atoms Σ i, Fin (arity i) → A – unlike the padded atoms, where only the padding-invariant subsets occur – so the increment of §the module docstring applies to the real ones unchanged. The two index types order assignments the same way, which is DescriptiveComplexity.SOBlock.atomSet_lt_iff_realSet: a real atom has a least padded representative, the one padded with the least element of A, and comparing those representatives is comparing the real atoms.

@[reducible, inline]

abbrev DescriptiveComplexity.SOBlock.RealIx (B : SOBlock) (A : Type) : Type

The real atoms of a block: a relation variable together with a tuple of its own arity. An assignment is an arbitrary subset of these.

Equations

• B.RealIx A = ((i : B.ι) × (Fin (B.arity i) → A))

def DescriptiveComplexity.SOBlock.realSet (B : SOBlock) {A : Type} (ρ : B.Assignment A) : B.RealIx A → Prop

The real atoms an assignment makes true – the assignment itself, uncurried, so this is a bijection onto the subsets.

Equations

• B.realSet ρ P = ρ P.fst P.snd

noncomputable def DescriptiveComplexity.SOBlock.realOf (B : SOBlock) {A : Type} (p : B.AtomIx A) : B.RealIx A

The real atom a padded one stands for.

Equations

• B.realOf p = ⟨p.1, fun (j : Fin (B.arity p.1)) => p.2 (Fin.castLE ⋯ j)⟩

noncomputable def DescriptiveComplexity.SOBlock.padMin (B : SOBlock) {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (i : B.ι) (u : Fin (B.arity i) → A) : Fin (blockArityBound B) → A

A tuple of the arity of i, padded out with the least element – the least padded representative of a real atom.

Equations

• B.padMin i u k = if h : ↑k < B.arity i then u ⟨↑k, h⟩ else DescriptiveComplexity.minEl✝ A

noncomputable def DescriptiveComplexity.SOBlock.keyIx (B : SOBlock) {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (P : B.RealIx A) : B.AtomIx A

The least padded representative of a real atom.

Equations

• B.keyIx P = (P.fst, B.padMin P.fst P.snd)

theorem DescriptiveComplexity.SOBlock.atomSet_eq_realSet (B : SOBlock) {A : Type} (ρ : B.Assignment A) (p : B.AtomIx A) : B.atomSet ρ p = B.realSet ρ (B.realOf p)

theorem DescriptiveComplexity.SOBlock.realSet_surjective (B : SOBlock) {A : Type} : Function.Surjective B.realSet

theorem DescriptiveComplexity.SOBlock.padMin_apply_of_lt (B : SOBlock) {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (i : B.ι) (u : Fin (B.arity i) → A) (k : Fin (blockArityBound B)) (hk : ↑k < B.arity i) : B.padMin i u k = u ⟨↑k, hk⟩

theorem DescriptiveComplexity.SOBlock.padMin_apply_of_ge (B : SOBlock) {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (i : B.ι) (u : Fin (B.arity i) → A) (k : Fin (blockArityBound B)) (hk : ¬↑k < B.arity i) : B.padMin i u k = DescriptiveComplexity.minEl✝ A

theorem DescriptiveComplexity.SOBlock.padMin_castLE (B : SOBlock) {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (i : B.ι) (u : Fin (B.arity i) → A) (j : Fin (B.arity i)) : B.padMin i u (Fin.castLE ⋯ j) = u j

@[simp]

theorem DescriptiveComplexity.SOBlock.realOf_keyIx (B : SOBlock) {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (P : B.RealIx A) : B.realOf (B.keyIx P) = P

theorem DescriptiveComplexity.SOBlock.keyIx_injective (B : SOBlock) {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : Function.Injective B.keyIx

@[instance_reducible]

noncomputable def DescriptiveComplexity.SOBlock.realIxLinearOrder (B : SOBlock) (A : Type) [LinearOrder A] [Finite A] [Nonempty A] : LinearOrder (B.RealIx A)

The real atoms are linearly ordered, by their least padded representatives.

Equations

• B.realIxLinearOrder A = LinearOrder.lift' B.keyIx ⋯

theorem DescriptiveComplexity.SOBlock.realIx_lt_iff (B : SOBlock) {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (P Q : B.RealIx A) : P < Q ↔ B.atomLt (B.keyIx P) (B.keyIx Q)

theorem DescriptiveComplexity.SOBlock.padMin_lt_iff (B : SOBlock) {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (i : B.ι) (u v : Fin (B.arity i) → A) : toLex (B.padMin i u) < toLex (B.padMin i v) ↔ toLex u < toLex v

Comparing least padded representatives is comparing the tuples they pad.

theorem DescriptiveComplexity.SOBlock.keyIx_realOf_le (B : SOBlock) {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (p : B.AtomIx A) : B.keyIx (B.realOf p) ≤ p

The least padded representative is least: no padded atom of the same real atom is below it.

theorem DescriptiveComplexity.SOBlock.atomSet_lt_iff_realSet (B : SOBlock) {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (ρ σ : B.Assignment A) : B.atomSet ρ < B.atomSet σ ↔ B.realSet ρ < B.realSet σ

The two atom indices order assignments the same way.

theorem DescriptiveComplexity.SOBlock.assignSucc_iff (B : SOBlock) {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (ρ σ : B.Assignment A) : SetSucc (B.realSet ρ) (B.realSet σ) ↔ B.atomSet ρ < B.atomSet σ ∧ ∀ (τ : B.Assignment A), B.atomSet ρ < B.atomSet τ → ¬B.atomSet τ < B.atomSet σ

The successor of an assignment is the increment at its real atoms: the right-hand side says that no assignment lies strictly between.

The increment as a sentence

noncomputable def DescriptiveComplexity.SOBlock.ivarsAbove (B : SOBlock) (i : B.ι) : List B.ι

The relation variables strictly above i, in the arbitrary order on the block's index type – the mirror of DescriptiveComplexity.SOBlock.ivarsBelow, and the atoms the increment clears.

Equations

• B.ivarsAbove i = List.filter (fun (j : B.ι) => decide (i < j)) B.ivars

theorem DescriptiveComplexity.SOBlock.mem_ivarsAbove (B : SOBlock) (i j : B.ι) : j ∈ B.ivarsAbove i ↔ i < j

noncomputable def DescriptiveComplexity.SOBlock.succAssignF (L : FirstOrder.Language) (B : SOBlock) : ((L.sum FirstOrder.Language.order).sum (B.replicate 2).lang).Sentence

The increment, as a sentence: at some atom the first copy is false and the second true; the copies agree strictly below it; and strictly above it the first is true and the second false. Each of the two conditions on the other atoms splits, as in DescriptiveComplexity.SOBlock.ordLtF, into a static part over the earlier (or later) relation variables and a lexicographic part at the same variable – taken on the truncated tuples, so that it compares real atoms and not their padded representatives (see the padding trap above).

Equations

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

theorem DescriptiveComplexity.SOBlock.forall_trunc_iff (B : SOBlock) {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (i : B.ι) (P : (Fin (B.arity i) → A) → Prop) : (∀ (y : Fin (blockArityBound B) → A), P fun (j : Fin (B.arity i)) => y (Fin.castLE ⋯ j)) ↔ ∀ (v : Fin (B.arity i) → A), P v

Quantifying a padded tuple is quantifying its truncation: every tuple of the arity of i is the truncation of one, namely of its least padded representative.

theorem DescriptiveComplexity.SOBlock.agree_below_real (B : SOBlock) {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (ρs : Fin 2 → B.Assignment A) (i : B.ι) (u : Fin (B.arity i) → A) : ((∀ j ∈ B.ivarsBelow i, ∀ (v : Fin (B.arity j) → A), ρs 0 j v ↔ ρs 1 j v) ∧ ∀ (v : Fin (B.arity i) → A), toLex v < toLex u → (ρs 0 i v ↔ ρs 1 i v)) ↔ ∀ (Q : B.RealIx A), B.atomLt (B.keyIx Q) (B.keyIx ⟨i, u⟩) → (B.realSet (ρs 0) Q ↔ B.realSet (ρs 1) Q)

The two agreement conjuncts say exactly “the copies agree at every real atom strictly below the witnessed one”.

theorem DescriptiveComplexity.SOBlock.clear_above_real (B : SOBlock) {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (ρs : Fin 2 → B.Assignment A) (i : B.ι) (u : Fin (B.arity i) → A) : ((∀ j ∈ B.ivarsAbove i, ∀ (v : Fin (B.arity j) → A), ρs 0 j v ∧ ¬ρs 1 j v) ∧ ∀ (v : Fin (B.arity i) → A), toLex u < toLex v → ρs 0 i v ∧ ¬ρs 1 i v) ↔ ∀ (Q : B.RealIx A), B.atomLt (B.keyIx ⟨i, u⟩) (B.keyIx Q) → B.realSet (ρs 0) Q ∧ ¬B.realSet (ρs 1) Q

The two clearing conjuncts say exactly “the first copy holds and the second does not, at every real atom strictly above the witnessed one”.

theorem DescriptiveComplexity.SOBlock.realize_succAssignF_aux {L : FirstOrder.Language} (B : SOBlock) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (ρs : Fin 2 → B.Assignment A) : A ⊨ succAssignF L B ↔ ∃ (i : B.ι) (u : Fin (B.arity i) → A), ((∀ j ∈ B.ivarsBelow i, ∀ (v : Fin (B.arity j) → A), ρs 0 j v ↔ ρs 1 j v) ∧ ∀ (v : Fin (B.arity i) → A), toLex v < toLex u → (ρs 0 i v ↔ ρs 1 i v)) ∧ ¬ρs 0 i u ∧ ρs 1 i u ∧ (∀ j ∈ B.ivarsAbove i, ∀ (v : Fin (B.arity j) → A), ρs 0 j v ∧ ¬ρs 1 j v) ∧ ∀ (v : Fin (B.arity i) → A), toLex u < toLex v → ρs 0 i v ∧ ¬ρs 1 i v

What the increment sentence says, spelled out at real atoms.

theorem DescriptiveComplexity.SOBlock.realize_succAssignF {L : FirstOrder.Language} (B : SOBlock) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (ρs : Fin 2 → B.Assignment A) : A ⊨ succAssignF L B ↔ SetSucc (B.realSet (ρs 0)) (B.realSet (ρs 1))

The increment sentence is the successor of an assignment: it holds of two assignments exactly when the second is the increment of the first at their real atoms – which, by DescriptiveComplexity.SOBlock.assignSucc_iff, is exactly the immediate successor in the order the expanded universe carries.

The two endpoints

noncomputable def DescriptiveComplexity.SOBlock.botAssignF (L : FirstOrder.Language) (B : SOBlock) (c : Fin 2) : ((L.sum FirstOrder.Language.order).sum (B.replicate 2).lang).Sentence

The copy c of the block holds of no padded atom.

Equations

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

noncomputable def DescriptiveComplexity.SOBlock.topAssignF (L : FirstOrder.Language) (B : SOBlock) (c : Fin 2) : ((L.sum FirstOrder.Language.order).sum (B.replicate 2).lang).Sentence

The copy c of the block holds of every padded atom.

Equations

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

theorem DescriptiveComplexity.SOBlock.realize_botAssignF {L : FirstOrder.Language} (B : SOBlock) {A : Type} [L.Structure A] [LinearOrder A] (ρs : Fin 2 → B.Assignment A) (c : Fin 2) : A ⊨ botAssignF L B c ↔ B.atomSet (ρs c) = fun (x : B.AtomIx A) => False

theorem DescriptiveComplexity.SOBlock.realize_topAssignF {L : FirstOrder.Language} (B : SOBlock) {A : Type} [L.Structure A] [LinearOrder A] (ρs : Fin 2 → B.Assignment A) (c : Fin 2) : A ⊨ topAssignF L B c ↔ B.atomSet (ρs c) = fun (x : B.AtomIx A) => True

def DescriptiveComplexity.SOBlock.topAssign (B : SOBlock) (A : Type) : B.Assignment A

The assignment holding of everything – the greatest one.

Equations

• B.topAssign A x✝¹ x✝ = True

The endpoints and the successor, at the points of an expansion

What a machine walking an expanded universe asks of its order (DescriptiveComplexity.HeadMove): which point is least, which is greatest, and which is the immediate successor of which. Tag first and then the assignment, so each answer splits: the tag part is static – finitely many tags, compared at formula-construction time – and the assignment part is the increment above. The lexicographic bookkeeping is DescriptiveComplexity.prodLex_le_iff and its siblings, with one caveat: a point's second component is an assignment, not an arbitrary set, so the witnesses put between two points must be assignments too – the empty one, the full one, and the ones the walk itself carries.

theorem DescriptiveComplexity.ExpExpansion.pointLe_iff {L : FirstOrder.Language} (X : ExpExpansion L) (A : Type) [LinearOrder A] [Finite A] [Nonempty A] (p q : X.Point A) : p ≤ q ↔ p.1 < q.1 ∨ p.1 = q.1 ∧ X.B.atomSet p.2 ≤ X.B.atomSet q.2

theorem DescriptiveComplexity.ExpExpansion.pointLt_iff {L : FirstOrder.Language} (X : ExpExpansion L) (A : Type) [LinearOrder A] [Finite A] [Nonempty A] (p q : X.Point A) : p < q ↔ p.1 < q.1 ∨ p.1 = q.1 ∧ X.B.atomSet p.2 < X.B.atomSet q.2

theorem DescriptiveComplexity.ExpExpansion.pointIsBot_iff {L : FirstOrder.Language} (X : ExpExpansion L) (A : Type) [LinearOrder A] [Finite A] [Nonempty A] (p : X.Point A) : (∀ (q : X.Point A), p ≤ q) ↔ (∀ (t : X.Tag), p.1 ≤ t) ∧ X.B.atomSet p.2 = fun (x : X.B.AtomIx A) => False

The least point: the least tag, holding of nothing.

theorem DescriptiveComplexity.ExpExpansion.pointIsTop_iff {L : FirstOrder.Language} (X : ExpExpansion L) (A : Type) [LinearOrder A] [Finite A] [Nonempty A] (p : X.Point A) : (∀ (q : X.Point A), q ≤ p) ↔ (∀ (t : X.Tag), t ≤ p.1) ∧ X.B.atomSet p.2 = fun (x : X.B.AtomIx A) => True

The greatest point: the greatest tag, holding of everything.

theorem DescriptiveComplexity.ExpExpansion.pointCovBy_iff {L : FirstOrder.Language} (X : ExpExpansion L) (A : Type) [LinearOrder A] [Finite A] [Nonempty A] (p q : X.Point A) : (p < q ∧ ∀ (r : X.Point A), ¬(p < r ∧ r < q)) ↔ p.1 = q.1 ∧ SetSucc (X.B.realSet p.2) (X.B.realSet q.2) ∨ p.1 < q.1 ∧ (∀ (t : X.Tag), ¬(p.1 < t ∧ t < q.1)) ∧ (X.B.atomSet p.2 = fun (x : X.B.AtomIx A) => True) ∧ X.B.atomSet q.2 = fun (x : X.B.AtomIx A) => False

The successor of a point: either the tag stays and the assignment is incremented, or the tag steps and the assignment rolls over from full to empty.