# Glossary

The words the skills use, each in one line, grouped by the skill that owns them; the skill says the rest.

## The setup

- **research-init, formal-init** — the skill, one per plugin, that sets a project up: it probes, proposes, writes what is absent and nothing that exists, and reports; `/research:research-init`, `/formal:formal-init`.
- **probe** — the report `setup probe` (the research side) or `formal probe` (the prover side) prints: the environment, the project, the kit's version, the proposals and a coverage line; it writes and installs nothing.
- **required, recommended, optional** — the probe's three words for an item: without a required one the flow does not run; a recommended one is proposed; an optional one serves what the project does.

## The flow

- **record** — one Markdown file with YAML front matter and a prose body, of one of four kinds; the records, not the chat, are the memory between sessions.
- **idea** — a raw signal worth attention: one sentence and a source; most die.
- **task** — a unit of work one owner can finish within its size; closed, it moves to the archive.
- **question** — a precisely stated question or conjecture with kill criteria: what the project wants to know; `decomposed` is its state once refined into tasks.
- **finding** — a checkable claim whose evidence a machine resolves: a declaration in a manifest, a document's numbered statement or table row, or a self-asserting probe.
- **transition** — the one way a record's state changes: `capture`, `task`, `frame`, `refine`, `draw`, `return`, `make`, `abort`, `answer`, `kill`, `park`, `unpark`, `rank`, `checked`, `set`; the fields a transition owns are never edited by hand.
- **capture, frame, refine** — an idea is captured from outside; ideas are framed into a question and are then `consumed`; a question is refined into tasks, sub-questions and ideas, which is the commitment point.
- **draw, make, abort, return** — a ready task is drawn under an owner's hand; it is made (done, with its resolution) or aborted (abandoned, with a reason), or returned to ready.
- **kill** — an idea, a ready task or an open question abandoned with a dated reason, kept findable.
- **kill criteria** — what would count as an answer to a question, or what would show it not worth asking, fixed when it is framed.
- **park** — an open question set aside with a date, a reason and, where known, the triggers that revive it; never for lacking a route.
- **hand, hand limit** — the active tasks an owner holds, and how many at once `flow.toml` allows.
- **owner** — a name in `flow.toml`'s `[hand]`: the working agent and the person by default; a decision owner holds the owner-only tasks.
- **owner-only work, decision** — a task of a decision kind: what only the person can do or should decide; never ranked, and a decision gates a landing, never a start.
- **the ranked list, the next list** — the records with a rank, in `INDEX.md`: the schedule of the work, worked from the top, refreshed when the owner asks or it is empty.
- **first move, why now** — what a ranked record says: why it is ranked and what its first step is; "none yet" is a legal first move.
- **rider** — a ready or active task marked as riding the next piece of work handed to another owner; the index lists it under "Rider for the next hand-over".
- **direction** — the owner's dated statement of what interests them, in the directions file: a hint that ranks items first, never a gate.
- **the inbox** — the slot at the top of the directions file where the owner leaves mail for the next session, which processes it first and empties it.
- **the log** — dated entries, newest first, each opening with a State paragraph; the top one is what a cold session trusts.
- **the registry** — the one place the project's deliverables and their order are stated; the ranked list orders the work, the registry the products.
- **evidence, status** — a finding's evidence items and the status they imply: `verified` (a declaration resolves in the manifest), `stated` (a document's statement or row), `empirical` (a probe), `refuted` (a guard or a probe as counterexample); the names are the project's.
- **declaration manifest** — a text file a prover's build regenerates, one `Module.Path name` line per declaration; the evidence resolver for declarations.
- **probe** — a self-asserting script, exiting non-zero when its own checks fail, listed in the project's probes register.
- **shard** — the subdirectory of findings named after the document that registers them.
- **do-not-reopen** — a tag on a question the index lists under "Settled, do not re-open" whatever its state, so a settled matter is seen before it is asked again.
- **legacy** — the `origin` of a record imported from before the flow, the one record written by hand; it gains its kill criteria at its first round.
- **text gates** — the project's own checks on prose, such as a linter or a one-sentence-per-line rule, run on a draft before a body or a row is written.
- **coverage line** — the last line of a check, saying which resolvers it looked at, so a green says what it did not look at (also `library`).

## The library

- **card** — one file per referred work: its fields, how it was read, our notes, its extracts, its copy.
- **key** — a card's pinned name, the first author's surname and the year by default, `--key` for another; a record cites a work as `lib:<key>`.
- **register (a work)** — `library register`: a new card for a work; distinct from registering a result, below.
- **read grade** — `unread`, `skimmed`, `parts`, `full`: a claim about the reader, not the work; a resolver's answer is never a read.
- **via** — the card a work is known through when it was not read itself.
- **extract** — what a work says at a place: a locator, the words quoted or restated, the author's caveat, the rule on what may be claimed; cited as `lib:<key>#<id>`.
- **copy, kept copy, the store** — a work's file: in the ignored store with the address it can be fetched from again, or in the tracked kept directory when nothing can, where it is redistributed with the repository, so `keep` writes there only with `--redistributable`.
- **resolver** — an online interface the library asks for a work's fields: arXiv, DOI, Crossref, OpenAlex and the others `docs/network.md` lists; never asked by a check.
- **watch** — a standing look for new works citing or related to a card, run by hand, keeping what it has seen and no clock.
- **candidate** — a work a watch surfaced and nobody has registered, kept in the candidates file until it is registered or set aside.
- **seeded** — a card loaded from an older list of works rather than registered for a citation, marked so.
- **internal document** — a document of the project itself with a card of an internal kind naming its tracked file; cited by key, never from a document's reference entries.
- **reference entry** — a line of a document's `## References` section, tied to exactly one card by title, first author and year.

## The method

- **landing** — bringing a result into the record and the documents: the finding, the registration in a document, the log entry, in one change.
- **register (a result), registration** — writing a landed result into a document as a specific numbered statement with its rows and boundary; where and whether is the project's rule.
- **summary sites** — the places a result is restated in short — the headline, the abstract, the contributions, the status label, the registry — which a correction must reach as well as the detailed site.
- **status label** — the words beside a statement saying how it is established — proved, machine-checked with what stays elementary, conditional on a named hypothesis, open.
- **pricing a target** — estimating what a piece of work costs and what it changes before committing to it.
- **currency** — the quantity a bound is measured in (a description length, a count, a time); on a wall the currency may change, and the change is disclosed.
- **bill** — a bound's cost accounting: the terms that add up to what a construction pays, each held by some object and each a count or a clock.
- **wall** — a reason a formal target cannot be reached as stated, named by kind: expressivity, elaboration, missing-upstream, misstated (with a prover).
- **tree-derived figure** — a count read off the artifact (declarations, guards, modules), stated only where the project's figure check recomputes it.
- **root session** — the session that holds the conversation and writes the documents and records; the prover session is the other, with none of its context.

## The formal plugin

- **handoff, handback** — the prompt a prover session is given and the report it returns, landed only after verification at the tree.
- **commission, commissioned** — what a handoff asks the prover session to produce: the declarations named on its `Commissioned:` line, which the landing looks up in the manifests.
- **guard, guard family** — a checked expectation beside a theorem (`#guard_msgs` over `#print axioms` in Lean) that a declaration's axioms, or a named instance's value, are as stated; a family is the set of instances that pin a theorem's hypotheses as load-bearing.
- **witness, joint-satisfiability witness** — a `<theorem>_nonvacuous` declaration showing a theorem's hypotheses hold at once, commissioned beside any theorem with two or more; a theorem with none is the finding.
- **refute first** — the prover session's opening move: a bounded computation at the smallest parameters where the commissioned statement can be computed, reported either way.
- **instantiation of an existing generic** — a landed declaration that is an existing generic theorem at one instance (`mul_comm_int` under `mul_comm`), the shape a report compresses into a clause.
- **drift, drift list** — the document sites a landing makes false or stale — figures, boundaries, citations — reported verbatim by the prover session and swept by the root session.
- **read-back packet** — a landed statement with the project-local definitions it names, docstrings and comments stripped, for a reader who has not seen the document.
- **binder tiers** — VERBATIM, ADAPTER, IMPLIED, UNANCHORED: what each binder of a landed declaration is against the document's statement.
- **sink-first** — a bundle lands its composite statement, the one nothing in the bundle depends on, before its predecessors are proved.

## The dashboard

- **component** — a skill whose CLI answers `--json pages`, which the dashboard mounts.