v1.2.0 – for Mathlib v4.33.0

Requires Mathlib v4.33.0 and toolchain leanprover/lean4:v4.33.0.

The exponential classes, and a machine model for AC⁰. Every class in the table
now has its complete problems and, where one is claimed, its machine model
proved equal to the logic that defines it.

The exponential classes

Read the polynomial-level logics over a universe one exponential larger and the
whole ladder above PSPACE follows. An exponential expansion maps a finite
ordered structure to the tagged assignments of a second-order block, and
ComplexityClass.exp reads a class there.

• EXPTIME = SO(LFP) = PTIME.exp (EXPTIME_eq_PTIME_exp), and equivalently
  SO-GAME, a second-order alternating game (exptime_eq_soGame). Its
  machine is the alternating polynomial-space one:
  APSPACE = EXPTIME (atmAcceptSpace_EXPTIME_complete).
• EXPSPACE = SO(PFP) = PSPACE.exp (EXPSPACE_eq_PSPACE_exp), complete for
  the wide machine in bounded space, deterministic and not
  (dwideAcceptSpace_EXPSPACE_complete, wideAcceptSpace_EXPSPACE_complete).
• NEXPTIME is NP read over an expansion, and equivalently ∃SO[new, exp],
  value invention bounded exponentially
  (mem_NEXPTIME_iff_sigmaSONewExpDefinable); complete for acceptance by a
  wide machine within its clock (wideRegAccept_NEXPTIME_complete).
• Tilings, the cheap second complete problem of each: tiling a 2ⁿ × 2ⁿ
  square is NEXPTIME-complete (wideTiling_NEXPTIME_complete) and tiling a
  corridor of width 2ⁿ is EXPSPACE-complete (wideCorridor_EXPSPACE_complete),
  with the polynomial CORRIDOR in PSPACE (corridor_mem_PSPACE).
• PSPACE = NL.exp (PSPACE_eq_NL_exp) pins the operator at the one level
  where the library independently knows the answer, in both directions.
• EPR, the ∃*∀* fragment: the problem, its small-model property and its
  NEXPTIME membership (epr_mem_NEXPTIME). Its hardness is not formalized.
• GAME, alternating reachability, is PTIME-complete (game_PTIME_complete).

AC⁰, and the machine model it was missing

• AC⁰ is the logic FO(≤, +, ×) over the ranks of a finite order, with no
  circuit model involved: FO(≤) ⊊ AC⁰ by EVEN
  (exists_ac0Definable_not_foDefinable, even_ac0Definable), and AC⁰ ⊆ PTIME.
• AC⁰ ⊆ LOGSPACE (ac0Definable_mem_LOGSPACE), by a deterministic
  multi-head automaton that computes the numeric predicates instead of reading
  them — plusP by a walk that parks its own marker, timesP by scanning
  candidates past plusP, and evalArithP evaluating a whole sentence over them.
• A machine model, and both halves of Immerman's Thm 1.17: alternating
  logarithmic time equals FO(≤, BIT) equals AC⁰ (ac0Definable_iff_ltDecidable),
  the Bit Sum Lemma included, by guessing the carries of one block.
• PARITY joins the catalog: in LOGSPACE (parity_mem_LOGSPACE) and not
  first-order, since EVEN reduces to it. Not to be confused with EVEN, the
  parity of the universe, which is AC⁰.
• FO(≤) ⊆ FO(DTC) closes the bottom end of the ladder.

Also in this release

• Documentation pass over the whole library: typography, US spelling, no
  planning labels or roadmap pointers left in any published docstring, and the
  README and landing-page class tables brought back into agreement.
• The package is indexed on
  Reservoir,
  so it can be required by name (see below).
• Moved to the stable Mathlib v4.33.0 pin, and cleared the warnings it
  brought.

Use

From Reservoir, in a lakefile.lean:

require "PierreSenellart" / "descriptive-complexity" @ "~1.2.0"

or from git:

require "descriptive-complexity" from git
  "https://github.com/PierreSenellart/descriptive-complexity" @ "v1.2.0"

See the compatibility table
for which version to use with which Mathlib.

Full changelog: v1.1.0...v1.2.0