# ArkLib Agent Wiki

This directory is the deeper companion to `AGENTS.md`.
Use `AGENTS.md` for the one-screen overview and this wiki for details that are too specific or
too changeable to keep at the repo root.
For reusable cross-cutting workflows that are not tied to one repo area, see
[`../skills/README.md`](../skills/README.md).

## Start Here

- [`quickstart.md`](quickstart.md) - canonical agent command and validation playbook.
- [`repo-map.md`](repo-map.md) - where to edit and how the main subtrees relate.
- [`generated-files.md`](generated-files.md) - derived outputs and their sources of truth.
- [`module-system.md`](module-system.md) - Lean's module system: the canonical file shape, the
  error-to-fix table, what the boundary buys, and what tightening is still on the table.
- [`blueprint-and-citations.md`](blueprint-and-citations.md) - blueprint workflow, paper
  references, and citation keys.
- [`knowledge-base.md`](knowledge-base.md) - when to use `docs/kb/` and how it relates to the
  agent wiki and bibliography.
- [`coding-theory-conventions.md`](coding-theory-conventions.md) - notation in scope, which
  numeric type each quantity uses, and the naming and layout choices local to
  `ArkLib/Data/CodingTheory/`.
- [`polynomial-conventions.md`](polynomial-conventions.md) - semantic axes for nested bivariate
  and trivariate polynomial representations.
- [`proximity-error-conventions.md`](proximity-error-conventions.md) - the proximity-gap,
  correlated-agreement, and mutual-correlated-agreement APIs and their numeric types.
- [`interaction-naming.md`](interaction-naming.md) - intrinsic meanings and migration of typed
  interaction sources, named oracle contexts, and sequential composition.
- [`ring-switching-consumers.md`](ring-switching-consumers.md) - instantiate the packing,
  batching, shared protocol and opening contracts for a consumer.
- [`sequential-composition.md`](sequential-composition.md) - legacy theorem selection for shared-state
  execution, completeness, and round-by-round soundness.
- [`probability-conventions.md`](probability-conventions.md) - namespace and export conventions
  for reusable helpers in `ArkLib/Data/Probability/`.
- [`porting-conventions.md`](porting-conventions.md) - where port history lives, naming and
  layout rules, and the review checklist for code ported from another snapshot.
- [`../design/README.md`](../design/README.md) - normative typed interaction and oracle-reduction
  architecture, current implementation status, and staged migration plan.
- [`../kb/audits/open-problems-list-decoding-and-correlated-agreement.md`](../kb/audits/open-problems-list-decoding-and-correlated-agreement.md)
  - paper-to-ArkLib status matrix for *Open Problems in List Decoding and Correlated Agreement*.

## Maintenance Contract

- `AGENTS.md` is the canonical root guide.
- Keep one primary owner topic per page. The current pages are:
  - `quickstart.md` for commands, validation, and when to run which checks.
  - `repo-map.md` for repo structure and main work areas.
  - `generated-files.md` for derived outputs and source-of-truth rules.
  - `module-system.md` for the module-system conventions every file under `ArkLib/` follows.
  - `blueprint-and-citations.md` for blueprint workflow, references, and citation updates.
  - `knowledge-base.md` for when and how agents should use `docs/kb/`.
  - `coding-theory-conventions.md` for notation, types and local conventions in `CodingTheory/`.
  - `polynomial-conventions.md` for nested polynomial axes and semantic evaluation/degree APIs.
  - `proximity-error-conventions.md` for the public APIs and numeric types of the proximity-error
    notions in `CodingTheory/ProximityGap/`.
  - `interaction-naming.md` for typed interaction API meanings and name migrations.
  - `ring-switching-consumers.md` for ring-switching consumer instantiation.
  - `sequential-composition.md` for legacy composition APIs and their hypotheses.
  - `probability-conventions.md` for namespace/export conventions in `Data/Probability/`.
  - `porting-conventions.md` for port history, naming, layout and the port review checklist.
- Add new pages when a recurring topic no longer fits cleanly in an existing guide.
- If a PR changes commands, repo structure, generated-file behavior, or the paper workflow,
  update the matching page in the same PR, or add a new page when that is the cleaner split.
- Keep these files committed so worktrees and delegated agents see the same guidance.
- Promote recurring, repo-specific agent learnings here once they prove stable.
- Prefer links to canonical docs over copying their contents. In particular, general Lean style
  lives in `CONTRIBUTING.md`: a page here should add what is local to its area, not restate the
  style guide.
- Keep these pages present-tense and free of commit-, PR- or session-specific detail: no review
  records, no dated plans, no "as of" snapshots. Anything that only makes sense next to one
  branch belongs in that branch's PR description, not here.

## Canonical Project Docs

- [`../../README.md`](../../README.md) - project overview.
- [`../../CONTRIBUTING.md`](../../CONTRIBUTING.md) - style, naming, docstrings, citations, and
  large contributions.
- [`../../ROADMAP.md`](../../ROADMAP.md) - status: what is complete, in progress, and planned.
- [`../../BACKGROUND.md`](../../BACKGROUND.md) - background theory and references, and how
  ArkLib's oracle reductions compare with the literature.