# Contributing to EconCSLib

EconCSLib accepts focused paper formalizations and reusable library, tooling,
and documentation improvements. Start with the contributor landing page:
[`docs/NEW_CONTRIBUTOR_WORKFLOW.md`](docs/NEW_CONTRIBUTOR_WORKFLOW.md).

The contribution process is provisional. Before substantial paper work,
coordinate the intended source version and scope with Nikhil Garg at
ngarg@cornell.edu.

## The One-Paper Pull Request

A pull request that adds or repairs one paper can use the paper-scoped lane. It
is responsible only for that paper, not for auditing or refreshing existing
formalizations.

Run the environment check once:

```bash
python3 scripts/paper_contribution.py doctor
```

For a new paper, first obtain the exact source version being formalized. Keep
those bytes outside the repository, not in Git. The example below assumes that
you have copied or downloaded the artifact into a user-owned working directory;
do not run `init-spec` until the `test` succeeds.

```bash
PAPER=ABC24ShortTitle
PAPER_URL=https://arxiv.org/abs/2401.01234
SOURCE_VERSION='arXiv v1, 2024-01-03'
WORK_DIR="${HOME}/econcslib-review/$PAPER"
SOURCE_ARTIFACT="$WORK_DIR/paper.pdf"
STATEMENT_SPEC="$WORK_DIR/statement-spec.json"

mkdir -p "$WORK_DIR"
# Put the exact source bytes at "$SOURCE_ARTIFACT" before continuing.
test -f "$SOURCE_ARTIFACT"
python3 scripts/paper_contribution.py init-spec \
  "$SOURCE_ARTIFACT" \
  --version "$SOURCE_VERSION" \
  --output "$STATEMENT_SPEC"
```

**STOP before running `new`.** Open `$STATEMENT_SPEC` and replace every
`REPLACE ...` value and `replace_with_lean_name` with the complete information
for a real paper-facing target. Add one target object per named result in scope.
The following guard must print nothing and succeed:

```bash
! grep -nE 'REPLACE|replace_with_lean_name' "$STATEMENT_SPEC"
```

Only then create the scaffold:

```bash
python3 scripts/paper_contribution.py new "$PAPER_URL" \
  --folder "$PAPER" \
  --title "A Short Formalization Example" \
  --authors "Ada Author and Bao Collaborator" \
  --version "$SOURCE_VERSION" \
  --statement-spec "$STATEMENT_SPEC"
```

Do not stage either `$SOURCE_ARTIFACT` or `$STATEMENT_SPEC`. Without
`--statement-spec`, the scaffold is still valid
but `PaperInterface.lean` starts intentionally empty rather than making
placeholder mathematical claims.

During development, run the fast paper check. Once publication is approved,
set `status.json` `repository_visibility` to `public`, run the paper-local
status synchronization, stage and commit the candidate, then prepare the
public pull request:

```bash
python3 scripts/paper_contribution.py check "$PAPER" --fast
python3 scripts/sync_paper_status.py --paper "$PAPER"
git add -- "papers/$PAPER" "papers/$PAPER.lean" lakefile.toml
git commit -m "Formalize $PAPER"
python3 scripts/paper_contribution.py prepare-pr "$PAPER" --base upstream/main
```

`prepare-pr` checks the committed base-to-`HEAD` scope and runs the full
source-present paper closeout once. `check --base upstream/main` is also
available after committing; it never treats uncommitted paths as part of the
candidate scope.

For a repair to an existing paper, do not run `new` or edit `lakefile.toml`.
Work within that paper's folder and root import, then use the same fast check,
paper-local sync, source-present full check, commit, and `prepare-pr` sequence.
Existing cross-paper Lean dependencies may compile as dependencies, but they are
not re-audited. The committed `--base`/`prepare-pr` check asks Lean for both
module closures and rejects any dependency module not already present at the
trusted base.

## Paper-Scoped Ownership

A one-paper pull request may own only:

- `papers/<PaperName>/**`
- `papers/<PaperName>.lean`
- the exact additive `[[lean_lib]]` registration for `<PaperName>` in
  `lakefile.toml`

The Lake edit may only add the paper's focused target. It must not modify other
targets or add the paper to broad default targets.

Do not include these generated aggregate files in a paper pull request:

- `papers/status.json`
- `papers/human_status.json`
- `docs/PAPER_STATUS.md`
- `site/index.html`

Maintainers or an integration job regenerate those surfaces after the paper is
accepted. This avoids cross-paper merge conflicts and makes existing paper
status irrelevant to the contribution check.

After merging a paper PR, a maintainer should immediately open the mechanical
aggregate-only update produced by:

```bash
git switch -c maintenance/refresh-paper-status main
python3 scripts/sync_paper_status.py --aggregate-only
git add -- docs/PAPER_STATUS.md papers/human_status.json papers/status.json site/index.html
git commit -m "Refresh paper status projections"
```

That follow-up owns only the four aggregate JSON, Markdown, and site
projections. Its trusted CI lane checks their exact generated bytes without
initializing Lean or rerunning semantic audits for unchanged papers. A stale
projection is only a warning on the intervening `main` push; malformed inputs
still fail, and manual/release validation remains strict.

Changes under `EconCSLib/`, `scripts/`, `skills/`, `config/`, or `.github/`,
changes to multiple paper folders, and non-additive Lake changes use the
integration lane. They may require broader builds or dependency audits because
their effects are shared. Keep them out of a one-paper pull request whenever
possible.

## Paper Contribution Contract

A completed paper contribution should provide a compact human-facing surface:

- `PaperInterface.lean` with the paper's definitions and named theoretical
  statements in source order;
- proof implementation modules, normally beginning with `MainTheorems.lean`;
- `Assumptions.lean` for source-stated assumptions that are not derived in
  Lean;
- `README.md`, `FINAL_VALIDATION_REPORT.md`, and
  `docs/FORMALIZATION_PLAN.md`;
- `status.json` and the paper-local machine audit evidence;
- `docs/DependencyDAG.tex` and its rendered PDF when the paper reaches a review
  boundary; and
- `papers/<PaperName>.lean` plus a focused Lake target.

`PaperInterface.lean` is the review surface, not the proof implementation file.
Do not hide extra premises in records, certificates, wrappers, or helper
theorems. Every non-derived paper-facing premise must either be source-backed
and exposed through `Assumptions.lean` or remain an explicit partial boundary.

The normal source scope is named theoretical content: named or numbered
definitions, lemmas, propositions, theorems, and corollaries. Computational
examples, figures, captions, and empirical results are outside normal theorem
coverage unless a deeper all-prose review was explicitly requested.

Do not claim `formalized` while a reviewed theorem contains `sorry`, `admit`, a
new unreviewed axiom, or a conclusion-bearing non-source assumption. Record
minor source typos and endpoint-preserving proof repairs in the validation
report; do not silently change the advertised theorem.

## Source Files And Audit Evidence

Keep source PDFs, TeX archives, and extracted text out of a one-paper pull
request. Publishing licensed source material is a separate integration
decision. The paper scaffold keeps source material untracked while recording
the source version and SHA-256 identity needed by the audit evidence.

The full local `check <PaperName>` must run with the pinned source bytes
present. That source-grounded closeout is the mathematical acceptance boundary.
Pull-request CI checks only the changed paper and can structurally validate
source receipts in a public checkout where the source bytes are intentionally
absent; CI does not upgrade an incomplete local source audit into acceptance.

## Pull-Request Review

`prepare-pr` compares the branch with the named base and rejects unrelated
paths in the paper-scoped lane. Pull-request CI derives scope from the Git diff;
a checkbox or label cannot make shared changes paper-local.

The paper lane also inspects every commit since the merge base. Rebase the
branch rather than merging main into it. Recognizable source PDFs, archives,
and extracted-source files committed and later deleted are still present in
public Git history and are blocked, not treated as a clean final diff. This is
a guard against accidents, not a license review or a semantic detector for
arbitrarily renamed text; contributors remain responsible for rebuilding a
clean branch if any third-party source bytes entered its history.

For a one-paper pull request, CI builds and audits only `<PaperName>`. Existing
paper failures are not part of that result. Shared library, workflow, audit
engine, protocol, or multi-paper changes escalate to integration checks.

In the pull-request description, identify:

- the paper folder and exact source version;
- the claimed formalization status;
- any additional assumptions, source corrections, or remaining boundaries;
- the local full-check command and result; and
- whether any shared code changed.

## Other Contributions

Reusable library contributions belong under `EconCSLib/` and should be
paper-independent. Tooling and protocol contributions belong in their existing
`scripts/`, `skills/`, `config/`, or `.github/` owners. These are integration
changes because they can affect more than one paper; document the targeted and
broader checks run in the pull request.

Unless explicitly marked otherwise, submitted Lean code, scripts,
documentation, and site source are contributed under the Apache License,
Version 2.0. The repository license does not grant redistribution rights for
third-party paper sources.