# EconCSLib Documentation

This directory has two kinds of documentation.

## Human-Facing

These files are for readers who want to understand the project, paper status,
or what a completed formalization proves without reading proof internals.

- [../README.md](../README.md): short project overview and review path.
- [REVIEW_DASHBOARD.md](REVIEW_DASHBOARD.md): theorem-statement review
  dashboard workflow.
- [VALIDATION_MODEL.md](VALIDATION_MODEL.md): how to read Lean proof status,
  human statement review, LLM audit status, and public paper labels.
- [PAPER_STATUS.md](PAPER_STATUS.md): generated paper citation, status labels
  linked to validation reports, human-review, Lean LOC, and note table.
- `../papers/<PaperName>/status.json`: paper-local machine-readable source of
  truth for status, review rows, and artifact paths.
- [../papers/human_status.json](../papers/human_status.json): generated compact
  human-facing status JSON for public summaries.
- [../papers/status.json](../papers/status.json): generated aggregate paper
  status.
- [NEW_CONTRIBUTOR_WORKFLOW.md](NEW_CONTRIBUTOR_WORKFLOW.md): first-time
  contributor workflow using public `main` as a base, private development, and
  a public-safe pull request when ready.
- [paper-formalization-quickstart/README.md](paper-formalization-quickstart/README.md):
  concise prompt and steering guide for starting or managing a paper
  formalization.
- [PUBLIC_REPOSITORY_WORKFLOW.md](PUBLIC_REPOSITORY_WORKFLOW.md): public/private
  repository split, completed-paper imports, and private partial-paper policy.
- [PRIVATE_DEVELOPMENT_WORKFLOW.md](PRIVATE_DEVELOPMENT_WORKFLOW.md):
  public-based private repository workflow and private-to-public paper PR path.
- [PUBLIC_RELEASE_CHECKLIST.md](PUBLIC_RELEASE_CHECKLIST.md): checks before a
  public announcement or broad external contribution request.
- [REPOSITORY_LAUNCH_PLAN.md](REPOSITORY_LAUNCH_PLAN.md): current launch plan
  for the public/private split and Pages activation.
- [PAGES_PUBLISHING.md](PAGES_PUBLISHING.md): static-site publishing steps for
  GitHub Pages.
- Paper-level `FINAL_VALIDATION_REPORT.md`, `PaperInterface.lean`, and
  `docs/DependencyDAG.pdf` files under `papers/<PaperName>/`.

## Agent And Maintainer-Facing

These files are operational references for formalization agents and maintainers.
They may assume Lean familiarity and may be more detailed.

- [AGENT_FORMALIZATION_WORKFLOW.md](AGENT_FORMALIZATION_WORKFLOW.md): how to
  start, run, audit, and finish a paper formalization with an agent.
- [ARCHITECTURE.md](ARCHITECTURE.md): repository structure, paper-folder
  contract, paper-facing ledger rules, and maintenance notes.
- [ECONCSLIB_DOMAIN_INDEX.md](ECONCSLIB_DOMAIN_INDEX.md): reusable library
  modules by domain.
- [LEAN_STYLE.md](LEAN_STYLE.md): Lean style conventions.
- [LIBRARY_PROVENANCE.md](LIBRARY_PROVENANCE.md): how to audit reusable
  certificate/source-boundary APIs and paper wrapper obligations.
- [UPSTREAM_LEAN_SOURCES.md](UPSTREAM_LEAN_SOURCES.md): imported and potential
  upstream Lean sources to scout before creating local APIs.
- [STATUS.md](STATUS.md): controlled vocabulary for paper status rows.
- [THEOREM_ERGONOMICS.md](THEOREM_ERGONOMICS.md): theorem statement and
  interface conventions.
- [PROBABILITY_LIBRARY_ROADMAP.md](PROBABILITY_LIBRARY_ROADMAP.md) and
  [OPTIMIZATION_LIBRARY_ROADMAP.md](OPTIMIZATION_LIBRARY_ROADMAP.md): reusable
  library roadmaps.
- [ECONCS_LIBRARY_EXTRACTION_PLAN.md](ECONCS_LIBRARY_EXTRACTION_PLAN.md):
  cross-paper extraction and cleanup plan for probability, rankings,
  stochastic processes, continuous analysis, and design optimization.
- [LARGE_DEVIATIONS_LIBRARY_PLAN.md](LARGE_DEVIATIONS_LIBRARY_PLAN.md):
  shared LDP, Chernoff, Laplace-principle, and binary-rate extraction plan for
  the GGSG19, GJ18, and GJ19 paper scaffolds.

Agent skills live under [`skills/`](../skills/). Use
[`skills/econcs-formalizer/`](../skills/econcs-formalizer/) for paper workflow,
audit, and closeout rules, and
[`skills/econcs-prover/`](../skills/econcs-prover/) for Lean theorem proving
and proof repair.