# Lean glossary for TCSlib readers

A short reference for terms that appear in this repository's declaration
names and docstrings and that are Lean or Mathlib jargon rather than
mathematics. The audience is a reader fluent in theoretical computer science
but not in Lean; each entry says just enough to make the sources readable.
It is not a Lean tutorial — for that, see
[Theorem Proving in Lean 4](https://lean-lang.org/theorem_proving_in_lean4/)
and the
[Mathlib naming conventions](https://leanprover-community.github.io/contribute/naming.html).

Entries are grouped by theme and alphabetized within each group.
For the repository's process vocabulary (audit gates, admissions, sketches),
see `workflow.md` and `policy.md`; this file covers only the language.

## 1. Declaration keywords and syntax

* **`abbrev`** — a definition marked *reducible*: automation (`simp`,
  `decide`, unification) unfolds it freely, where a plain `def` is left
  opaque. Example: `FeedForward.GateOp.id` is an `abbrev` precisely so that
  identity-wire layers evaluate away under `simp`.
* **anonymous constructor `⟨…⟩`** — builds whatever the expected type calls
  for, listing its components in order: `⟨a, k, hS⟩` proves
  `∃ a k, …` by supplying witnesses and a proof, and
  `⟨Fin 1, fun x ↦ 1 - x 0⟩` builds a `GateOp` field by field.
* **dot notation** — `C.size` means `Circuit.size C` for `C : Circuit n`:
  the function is looked up in the namespace of the argument's type. This is
  why namespace placement matters — `F.onlyUsesGates S` works because
  `onlyUsesGates` lives in the `FeedForward` namespace.
* **`Fact`** — a wrapper that turns an ordinary proposition into a
  typeclass, so that instance search can carry it: `[Fact (Nat.Prime p)]`
  (in `ACpGates.lean` and the rest of the Razborov–Smolensky chain) is how
  `ZMod p` knows it is a field.
* **`instance` and square-bracket arguments** — `[Fintype ι]` is a
  *typeclass* assumption, filled in automatically by instance search rather
  than passed explicitly at call sites; `instance` declarations register
  what the search may use.
* **`namespace` / `open`** — namespaces prefix declaration names
  (`BoolCircuit.Circuit`); `open BoolCircuit` lets a file omit the prefix,
  and `open X in` scopes that to a single declaration.
* **`private` / `protected`** — `private`: invisible outside the defining
  file; this repo uses it deliberately for template-not-API material (e.g.
  `counterTM` in `TimeConstructible.lean`, a worked construction that
  nothing downstream may cite). `protected`: usable only with its namespace
  prefix, even under `open`.
* **`_root_.`** — anchors a name at the top level, ignoring the enclosing
  `namespace` blocks; used when a declaration inside one namespace must
  land in (or refer unambiguously to) another.
* **`structure` / `inductive`** — `structure` declares a record of named
  fields (`NDTM`, `FeedForward`), built with `where` or `⟨…⟩`; `inductive`
  declares a datatype generated by constructors (`Circuit` as a tree of
  `.lit` and `.node`).
* **`universe u v` / `Type u` / `Type*`** — bookkeeping for the hierarchy
  of type sizes (`Type*` means "any universe"). Needed for Lean's
  consistency; safe for a reader to ignore.

## 2. Propositions, booleans, and computability

* **`Classical`** — enables nonconstructive reasoning: `open scoped
  Classical` (e.g. in `UnaryLanguages.lean`) grants every proposition a
  decidability instance by fiat. Definitions that rely on it become
  `noncomputable`, which is harmless here (see below).
* **`decide`** — a tactic that proves a decidable proposition by actually
  running its decision procedure; `by decide` and the `simp +decide` and
  `cases b <;> decide` idioms all delegate to computation.
* **`Decidable` / `DecidableEq` / `DecidablePred`** — typeclass evidence
  that a proposition (resp. an equality test, a predicate) can be computed
  to a yes/no answer; required by `decide`, by `if … then … else` inside
  definitions, and by `Finset.filter`.
* **`noncomputable`** — marks a definition whose body uses choice or mere
  existence, so Lean generates no executable code for it. Proofs about it
  are completely unaffected: `universalCircuit`, `padFamily`, and
  `FeedForward.size` (via `Nat.card`) are all noncomputable and all fully
  reasoned about.
* **`Prop` vs `Bool`** — `Prop` is the type of mathematical statements;
  `Bool` is the two-element *data* type that machines and circuits compute
  with. A `Bool` becomes a statement only by comparison, which is why
  acceptance definitions read `(C.circuit w.length).eval w.get = true`
  rather than asserting the eval bare.

## 3. Totalization and encoding idioms

* **fallback / canonical** — the repository's total-decoder convention: a
  `decode` function never fails, mapping ill-formed strings to a fixed
  harmless `fallback` value, and a round-trip lemma
  (`decode_serialize`, `codeCanonical_eq`, `decodeSigma_encodeSigma`)
  pins down the well-formed strings. Three parallel instances:
  `Formulas/CNFEncoding.lean`, the machine-code `CodeParser`, and the
  circuit `Encoding.lean`.
* **fuel** — an extra `ℕ` argument that decreases at every recursive call,
  making termination structurally obvious to Lean — in TCS terms, an
  explicit potential function for the recursion, passed as an argument.
  The caller supplies a generous budget (typically `x.length`), and it is
  purely a termination device with no algorithmic meaning. Examples:
  `parseClause : ℕ → …` in `CNFEncoding.lean`; `readCircuit`/`readChildren`
  in `Encoding.lean`.
* **`Option α` / `some` / `none`** — "an `α`, or failure": how partial
  steps (parsers, `prevVisit`'s `.max?`) are typed before the fallback
  convention makes the top-level function total.
* **Sigma / `(n : ℕ) × Circuit n`** — a dependent pair (Σ-type): the type
  of the second component depends on the value of the first, here a width
  `n` bundled with a circuit on exactly `n` inputs. Hence the names
  `encodeSigma`/`decodeSigma`. Built with `⟨n, C⟩`.

## 4. Proof-facing vocabulary

* **definitional equality / `rfl` / `Iff.rfl`** — equality that holds by
  mere unfolding of definitions. A lemma proved by `Iff.rfl`
  (`mem_PPoly_iff`, `mem_language_iff`) has no mathematical content; it
  exists to re-state a definition in the form other proofs want to consume.
* **`simp` / `@[simp]` / "simp normal form"** — `simp` is the rewriting
  tactic; the `@[simp]` attribute marks an equation to be applied
  automatically left-to-right. A docstring calling a lemma "the simp form"
  means it is phrased so that rewriting moves goals toward it.
* **`sorry` / admission** — `sorry` closes any goal without proof, and the
  compiler flags every declaration that depends on one. This repository
  uses them deliberately in its statement-first workflow — an *admission*
  is a sorry whose formal statement has been externally audited while its
  proof is pending. The discipline (who may add one, how they are
  tracked and discharged) is in `workflow.md`; this entry is only the
  vocabulary.

## 5. Mathlib types and conventions

* **coercions `↑` / nested casts** — automatic type-changing maps, printed
  `↑x` or written explicitly as `((x : Fin 2) : ℕ)`. Chains move a value
  through intermediate types: `(((x i : Fin 2) : ℕ) : ZMod p)` in
  `modGateOp` carries a bit through `ℕ` into the prime field.
* **`Fin n`** — the canonical `n`-element type `{0, …, n−1}`; circuit
  inputs are functions `Fin n → Bool`. The FeedForward gate alphabet is
  `Fin 2`, and `finTwoEquiv : Fin 2 ≃ Bool` converts at the boundary
  (`PPoly.lean`).
* **`Fintype` vs `Finite` vs `Nat.card`** — `Fintype α` is an explicit,
  computable enumeration of `α`; `Finite α` is mere finiteness (a `Prop`);
  `Nat.card α` is the cardinality, by convention `0` for infinite types —
  which is why `FeedForward.size` is total yet `noncomputable`.
* **`Language α`** — Mathlib's name for `Set (List α)`: a language is
  simply a set of strings, used with ordinary `∈`. The campaign works over
  `Language Bool` (from `Mathlib.Computability.Language`, first imported in
  `ClassP/DTIME.lean`).
* **naming grammar** — Mathlib's conventions decode most names on sight:
  `mem_X_iff` unfolds membership in `X`; `X_of_Y` reads "X follows from Y";
  `X_iff_Y` is an equivalence; a trailing `'` is a variant; `h`-prefixed
  identifiers (`hc`, `hL`) are hypotheses. Casing carries meaning:
  `UpperCamelCase` for types and `Prop`-valued predicates
  (`TimeConstructible`, `HasPolylogDepth`), `lowerCamelCase` for data
  (`stdGateOps`, `encodeSigma`), `snake_case` phrases for theorem names —
  so `mem_NP_iff_exists_length_le` reads as "membership in `NP` iff there
  exists a certificate of bounded length".
* **set-builder / `⋃`** — `{L | P L}` is the set of all `L` satisfying `P`
  (how classes like `NP` and `PPoly` are packaged as sets); `⋃ i, s i` is
  indexed union (`iUnion` in lemma names), as in
  `NC = ⋃ i ∈ Set.Ici 1, NCLevel i`.