PARITY: the parity of a marked subset

The problem the switching lemma is about, and the one DescriptiveComplexity.EVEN must not be confused with. The vocabulary is a single unary predicate, so an instance is a finite set with a marked subset, and the question is whether the marked subset has an even number of elements.

Why it is here, given that EVEN is already here

DescriptiveComplexity.EVEN asks the parity of the universe – of the input's length – and that is AC⁰: an AC⁰ circuit family is indexed by the length, and in the logic the numeric predicates read the top rank (DescriptiveComplexity.even_ac0Definable). PARITY asks the parity of part of the input, and is the classical example of a problem outside AC⁰ (Ajtai 1983; Furst, Saxe & Sipser 1984; Håstad 1986). Keeping both in the catalog is what makes the distinction concrete rather than a warning in a docstring.

What is proved here is the easy side of that separation, and it is worth having on its own:

• PARITY is in LOGSPACE (DescriptiveComplexity.parity_mem_LOGSPACE), by one deterministic walk along the order: carry a bit, flip it at each marked element. The walk is DescriptiveComplexity.parSpec, its mode is the parity of the marked elements seen so far, and it is functional outright (DescriptiveComplexity.functional_parSpec), so determinizing changes nothing (DescriptiveComplexity.TCSpec.det_accepts_iff).
• PARITY is not first-order definable, even order-invariantly (DescriptiveComplexity.parity_not_foDefinable): EVEN is the special case where everything is marked, an FO reduction of one line (DescriptiveComplexity.evenParityInterp), and first-order definability travels backward along reductions.

What would finish the story, and is not here

AC⁰ ⊊ LOGSPACE is now one theorem away: PARITY ∉ AC⁰. That theorem is the switching lemma (Håstad 1986), a major formalization on its own, and nothing in this library proves any AC⁰ lower bound. The gap is deliberate and documented; what is recorded here is that the other three sides of the square – PARITY in LOGSPACE, PARITY not in FO(≤), EVEN in AC⁰, AC⁰ inside PTIME – are theorems.

inductive FirstOrder.Language.markedSetRel : ℕ → Type

The relation symbols of the language.

• mark : markedSetRel 1

  mark x: the element x belongs to the marked subset.

@[instance_reducible]

instance FirstOrder.Language.instDecidableEqMarkedSetRel {a✝ : ℕ} : DecidableEq (markedSetRel a✝)

Equations

• FirstOrder.Language.instDecidableEqMarkedSetRel = FirstOrder.Language.instDecidableEqMarkedSetRel.decEq

def FirstOrder.Language.markedSet : Language

The relational vocabulary of a marked subset: a finite set with a distinguished subset of it.

Equations

• FirstOrder.Language.markedSet = { Functions := fun (x : ℕ) => Empty, Relations := FirstOrder.Language.markedSetRel }

instance FirstOrder.Language.instIsRelationalMarkedSet : Language.markedSet.IsRelational

@[reducible, inline]

abbrev FirstOrder.Language.markedSetMark : Language.markedSet.Relations 1

mark x: the element x belongs to the marked subset.

Equations

• FirstOrder.Language.markedSetMark = FirstOrder.Language.markedSetRel.mark

def FirstOrder.Language.instDecidableEqMarkedSetRel.decEq {a✝ : ℕ} (x✝ x✝¹ : markedSetRel a✝) : Decidable (x✝ = x✝¹)

Equations

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

@[reducible, inline]

abbrev FirstOrder.Language.markedSetMarkO : (Language.markedSet.sum Language.order).Relations 1

The marking symbol, in the ordered expansion. Sum-language symbols are referenced through an abbreviation with a declared type, never as a raw Sum.inl, or rw fails to match at implicit transparency.

Equations

• FirstOrder.Language.markedSetMarkO = Sum.inl FirstOrder.Language.markedSetMark

The problem

def DescriptiveComplexity.Marked (A : Type) [FirstOrder.Language.markedSet.Structure A] : Set A

The marked subset of a structure.

Equations

• DescriptiveComplexity.Marked A = {x : A | FirstOrder.Language.Structure.RelMap FirstOrder.Language.markedSetMark ![x]}

@[simp]

theorem DescriptiveComplexity.mem_marked_iff {A : Type} [FirstOrder.Language.markedSet.Structure A] (x : A) : x ∈ Marked A ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.markedSetMark ![x]

def DescriptiveComplexity.PARITY : DecisionProblem FirstOrder.Language.markedSet

PARITY: the marked subset has an even number of elements. Contrast DescriptiveComplexity.EVEN, which asks this of the universe: that one is AC⁰, this one is the classical AC⁰ lower bound.

Equations

• DescriptiveComplexity.PARITY = { Holds := fun (A : Type) (x : FirstOrder.Language.markedSet.Structure A) => Even (DescriptiveComplexity.Marked A).ncard, iso_invariant := ⋯ }

theorem DescriptiveComplexity.parity_holds_iff (A : Type) [FirstOrder.Language.markedSet.Structure A] : PARITY.Holds A ↔ Even (Marked A).ncard

The value of PARITY, unfolded.

PARITY is a deterministic walk

One bit, one element, one pass along the order: the mode is the parity of the marked elements up to and including the current one, so it flips exactly at a marked element. Both the successor and the new mode are determined by the current node, which is why the walk is functional and the determinization is free.

noncomputable def DescriptiveComplexity.markF {α : Type} (x : α) : (FirstOrder.Language.markedSet.sum FirstOrder.Language.order).Formula α

x is marked, as a formula over the ordered expansion.

Equations

• DescriptiveComplexity.markF x = FirstOrder.Language.markedSetMarkO.formula₁ (FirstOrder.Language.var x)

@[simp]

theorem DescriptiveComplexity.realize_markF {A : Type} [FirstOrder.Language.markedSet.Structure A] [LinearOrder A] {α : Type} (x : α) (v : α → A) : (markF x).Realize v ↔ v x ∈ Marked A

noncomputable def DescriptiveComplexity.parStep (m m' : Bool) : (FirstOrder.Language.markedSet.sum FirstOrder.Language.order).Formula (Fin 1 ⊕ Fin 1)

The transition of the parity walk: step to the immediate successor, and flip the mode exactly when the element stepped onto is marked.

Equations

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

noncomputable def DescriptiveComplexity.parSrc (m : Bool) : (FirstOrder.Language.markedSet.sum FirstOrder.Language.order).Formula (Fin 1)

The walk starts at the minimum, in the mode that element prescribes: even unless the minimum is itself marked.

Equations

• DescriptiveComplexity.parSrc m = DescriptiveComplexity.minF 0 ⊓ if m = true then FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.markF 0) else DescriptiveComplexity.markF 0

noncomputable def DescriptiveComplexity.parTgt (m : Bool) : (FirstOrder.Language.markedSet.sum FirstOrder.Language.order).Formula (Fin 1)

The walk accepts at the maximum, in the even mode.

Equations

• DescriptiveComplexity.parTgt m = if m = true then DescriptiveComplexity.maxF 0 else ⊥

noncomputable def DescriptiveComplexity.parSpec : TCSpec FirstOrder.Language.markedSet

PARITY as a single walk: one element, one bit, flipped at the marked elements.

Equations

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

theorem DescriptiveComplexity.functional_parSpec {A : Type} [FirstOrder.Language.markedSet.Structure A] [LinearOrder A] [Finite A] : parSpec.Functional A

The walk is functional: the successor of an element is unique in a finite linear order, and the new mode is determined by its markedness.

theorem DescriptiveComplexity.parity_dtcDefinable : DTCDefinable PARITY

PARITY is FO(DTC) definable, by the deterministic parity walk: the determinization changes nothing, the walk being functional.

theorem DescriptiveComplexity.parity_mem_LOGSPACE : LOGSPACE.Mem PARITY

PARITY is in LOGSPACE. With DescriptiveComplexity.parity_not_foDefinable below, and the AC⁰ layer, this is three of the four sides of AC⁰ ⊊ LOGSPACE; the fourth is PARITY ∉ AC⁰, which this library does not prove. Registered in the Lax archive as Lax945089.ParityInLogSpace.parity_mem_LOGSPACE.

EVEN is the special case where everything is marked

noncomputable def DescriptiveComplexity.evenParityInterp : FOInterpretation FirstOrder.Language.empty FirstOrder.Language.markedSet Unit 1

The interpretation marking every element: EVEN read as an instance of PARITY, one dimension and one tag.

Equations

• DescriptiveComplexity.evenParityInterp = { relFormula := fun {x : ℕ} (x_1 : FirstOrder.Language.markedSet.Relations x) (x_2 : Fin x → Unit) => ⊤ }

theorem DescriptiveComplexity.marked_evenParityInterp (A : Type) [FirstOrder.Language.empty.Structure A] : Marked (evenParityInterp.Map A) = Set.univ

Every point of the interpreted structure is marked.

noncomputable def DescriptiveComplexity.even_fo_reduction_parity : FOReduction EVEN PARITY

EVEN reduces to PARITY: mark everything.

Equations

• DescriptiveComplexity.even_fo_reduction_parity = { Tag := Unit, tagFinite := ⋯, tagNonempty := ⋯, dim := 1, toInterpretation := DescriptiveComplexity.evenParityInterp, correct := ⋯ }

theorem DescriptiveComplexity.parity_not_foDefinable : ¬FODefinable PARITY

PARITY is not first-order definable, even order-invariantly: EVEN is not (DescriptiveComplexity.even_not_foDefinable), and it reduces to PARITY. Registered in the Lax archive as Lax945089.ParityInLogSpace.parity_not_foDefinable.