Complexitylib.lean

/-
Copyright (c) 2025 Samuel Schlesinger. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Samuel Schlesinger
-/

module
public import Complexitylib.Models
public import Complexitylib.Metacomplexity
public import Complexitylib.Encoding
public import Complexitylib.Asymptotics
public import Complexitylib.TimeConstructible
public import Complexitylib.Classes
public import Complexitylib.Languages
public import Complexitylib.SAT
public import Complexitylib.Circuits
public import Complexitylib.BooleanAnalysis
public import Complexitylib.DescriptiveComplexity
public import Complexitylib.Interop
public import Complexitylib.Algebraic
public import Complexitylib.RationalHitting
public import Complexitylib.RationalHitting.PolynomialTime
public import Complexitylib.Tactic.PolyTime

/-!
# Complexitylib

The root module: importing it brings in the library's complete public
surface. Import an area module (`Complexitylib.Models`,
`Complexitylib.Classes`, …) instead to keep dependencies smaller.

## Headline theorems

Machine-checked with no `sorry` and no custom axioms — CI audits every
Complexitylib declaration for dependencies beyond `propext`,
`Classical.choice`, and `Quot.sound` (`scripts/AxiomGuard.lean`).

**Cook–Levin: SAT is NP-complete.**
- `Complexity.SAT.NPComplete_language` — `NPComplete SAT.language`
- `Complexity.SAT.language_mem_NP` — `SAT.language ∈ NP`
- `Complexity.SAT.pairLang_witness_mem_P` — the SAT verifier runs in
  polynomial time

**Universal simulation.**
- `Complexity.TM.UTMBody.utmTM_universal` — a fixed machine simulates any
  encoded machine with explicit time overhead (Arora–Barak Theorem 1.9)
- `Complexity.TM.UTMBody.utmTM_universal_padded` — the padded-encoding
  variant

**Deterministic time hierarchy.**
- `Complexity.time_hierarchy_weak` — more time decides strictly more
  languages, in a concrete clock-constructible formulation
- `Complexity.time_hierarchy_weak_ssubset`, `Complexity.DTIME_pow_ssubset`
  — strict polynomial separations such as
  `DTIME((n+1)^a) ⊂ DTIME((n+1)^(2a+5))`

**Structural containments.** `Complexity.P_subset_NP`,
`Complexity.P_subset_PSPACE`, `Complexity.P_subset_PPoly`,
`Complexity.UniformPPoly_subset_P`,
`Complexity.PAdvice_subset_PPoly`, `Complexity.PPoly_subset_PAdvice`,
`Complexity.RP_subset_NP`, `Complexity.BPP_subset_PPoly`,
`Complexity.BPP_subset_PAdvice`, and `Complexity.BPP_subset_PP`. The nonuniform
equivalence lives in `Complexitylib.Classes.PPoly.Advice`, while randomized
hardwiring and its advice corollary live in
`Complexitylib.Classes.Randomized.PPoly`; the broader time/space index is
`Complexitylib.Classes.Containments`.

**Circuit lower bounds.** Shannon's counting bound, gate-elimination
(`Circuit.card_essentialInputs_le_mul_size`), Schnorr's XOR bound
(`Complexity.sizeComplexity_xorBool_ge`), Valiant's depth reduction
(`Complexity.Valiant.depth_reduction`), and the Razborov–Smolensky bound: parity
is not in `AC0[3]` (`Complexity.xorBool_not_mem_AC0Mod_three`).

**Barrington's theorem.** `Complexity.barrington_equivalence` identifies
logarithmic-depth Boolean formula families with polynomial-length width-`5`
permutation branching-program families.

**CSLib interoperability.** `Complexity.mem_P_iff_decidableInTimeAndSpace`
identifies `P` with polynomial time on CSLib's multi-tape machines, and
`Complexity.mem_L_of_isRegular` places CSLib's regular languages in `L`.
`Complexity.mem_PPoly_iff_cslib` characterizes `P/poly` by CSLib's De Morgan
circuits, and `Complexity.lupanov_sizeComplexity` transfers Lupanov's
`(1 + ε) 2ⁿ / n` upper bound from CSLib.
-/