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.

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

@[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 }

inductive FirstOrder.Language.markedSetRel : ℕ → Type

The relation symbols of the language.

• mark : markedSetRel 1

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

@[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

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

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.parCount {A : Type} [FirstOrder.Language.markedSet.Structure A] [LinearOrder A] [Finite A] (x : A) : ℕ

The number of marked elements up to and including x.

Equations

• DescriptiveComplexity.parCount x = {y : A | y ≤ x ∧ y ∈ DescriptiveComplexity.Marked A}.ncard

noncomputable def DescriptiveComplexity.parMode {A : Type} [FirstOrder.Language.markedSet.Structure A] [LinearOrder A] [Finite A] (x : A) : Bool

The mode carried at x: whether an even number of marked elements has been seen so far.

Equations

• DescriptiveComplexity.parMode x = decide (Even (DescriptiveComplexity.parCount x))

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.realize_parStep {A : Type} [FirstOrder.Language.markedSet.Structure A] [LinearOrder A] (m m' : Bool) (x y : Fin 1 → A) : (parStep m m').Realize (Sum.elim x y) ↔ x 0 ⋖ y 0 ∧ (m' = !m ∧ y 0 ∈ Marked A ∨ m' = m ∧ y 0 ∉ Marked A)

theorem DescriptiveComplexity.step_parSpec_iff {A : Type} [FirstOrder.Language.markedSet.Structure A] [LinearOrder A] (m m' : Bool) (x y : Fin 1 → A) : parSpec.Step (m, x) (m', y) ↔ x 0 ⋖ y 0 ∧ (m' = !m ∧ y 0 ∈ Marked A ∨ m' = m ∧ y 0 ∉ Marked A)

theorem DescriptiveComplexity.isSrc_parSpec_iff {A : Type} [FirstOrder.Language.markedSet.Structure A] [LinearOrder A] (m : Bool) (x : Fin 1 → A) : parSpec.IsSrc (m, x) ↔ (∀ (a : A), x 0 ≤ a) ∧ (m = true ∧ x 0 ∉ Marked A ∨ m = false ∧ x 0 ∈ Marked A)

theorem DescriptiveComplexity.isTgt_parSpec_iff {A : Type} [FirstOrder.Language.markedSet.Structure A] [LinearOrder A] (m : Bool) (x : Fin 1 → A) : parSpec.IsTgt (m, x) ↔ m = true ∧ ∀ (a : A), a ≤ x 0

theorem DescriptiveComplexity.parCount_isMin_marked {A : Type} [FirstOrder.Language.markedSet.Structure A] [LinearOrder A] [Finite A] {z : A} (hz : ∀ (a : A), z ≤ a) (hm : z ∈ Marked A) : parCount z = 1

The prefix of a minimum is the minimum itself, when it is marked.

theorem DescriptiveComplexity.parCount_isMin_not_marked {A : Type} [FirstOrder.Language.markedSet.Structure A] [LinearOrder A] [Finite A] {z : A} (hz : ∀ (a : A), z ≤ a) (hm : z ∉ Marked A) : parCount z = 0

The prefix of an unmarked minimum is empty.

theorem DescriptiveComplexity.parCount_covBy_marked {A : Type} [FirstOrder.Language.markedSet.Structure A] [LinearOrder A] [Finite A] {w z : A} (h : w ⋖ z) (hm : z ∈ Marked A) : parCount z = parCount w + 1

The prefix grows by one along a cover onto a marked element.

theorem DescriptiveComplexity.parCount_covBy_not_marked {A : Type} [FirstOrder.Language.markedSet.Structure A] [LinearOrder A] [Finite A] {w z : A} (h : w ⋖ z) (hm : z ∉ Marked A) : parCount z = parCount w

The prefix is unchanged along a cover onto an unmarked element.

theorem DescriptiveComplexity.parMode_isMin_marked {A : Type} [FirstOrder.Language.markedSet.Structure A] [LinearOrder A] [Finite A] {z : A} (hz : ∀ (a : A), z ≤ a) (hm : z ∈ Marked A) : parMode z = false

The mode of a marked minimum is odd.

theorem DescriptiveComplexity.parMode_isMin_not_marked {A : Type} [FirstOrder.Language.markedSet.Structure A] [LinearOrder A] [Finite A] {z : A} (hz : ∀ (a : A), z ≤ a) (hm : z ∉ Marked A) : parMode z = true

The mode of an unmarked minimum is even.

theorem DescriptiveComplexity.parMode_covBy_marked {A : Type} [FirstOrder.Language.markedSet.Structure A] [LinearOrder A] [Finite A] {w z : A} (h : w ⋖ z) (hm : z ∈ Marked A) : parMode z = !parMode w

The mode flips along a cover onto a marked element.

theorem DescriptiveComplexity.parMode_covBy_not_marked {A : Type} [FirstOrder.Language.markedSet.Structure A] [LinearOrder A] [Finite A] {w z : A} (h : w ⋖ z) (hm : z ∉ Marked A) : parMode z = parMode w

The mode is unchanged along a cover onto an unmarked element.

theorem DescriptiveComplexity.reach_parSpec {A : Type} [FirstOrder.Language.markedSet.Structure A] [LinearOrder A] [Finite A] {x₀ : A} (h₀ : ∀ (a : A), x₀ ≤ a) (x : A) : parSpec.Reach (parMode x₀, fun (x : Fin parSpec.k) => x₀) (parMode x, fun (x_1 : Fin parSpec.k) => x)

The walk reaches every element, in the mode its prefix prescribes.

theorem DescriptiveComplexity.parMode_of_reach {A : Type} [FirstOrder.Language.markedSet.Structure A] [LinearOrder A] [Finite A] {x₀ : A} (p : parSpec.Node A) : parSpec.Reach (parMode x₀, fun (x : Fin parSpec.k) => x₀) p → p.1 = parMode (p.2 0)

The mode of a reachable node is the parity of its prefix: the invariant that reads the walk backwards.

theorem DescriptiveComplexity.accepts_parSpec_iff {A : Type} [FirstOrder.Language.markedSet.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : parSpec.Accepts A ↔ Even (Marked A).ncard

The walk accepts exactly the structures whose marked subset is even: it visits every element once, from the minimum to the maximum, so the mode it ends in is the parity of the whole marked subset.

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.

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

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

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.