From 78649f7e2c9aaefa37693598b7718b2c94221b23 Mon Sep 17 00:00:00 2001
From: Xinze-Li-Moqian <70414198+Xinze-Li-Moqian@users.noreply.github.com>
Date: Tue, 21 Jul 2026 10:38:59 -0400
Subject: [PATCH] chore: add review rubric + PR template (governance)

A fixed, repeatable review checklist (.github/REVIEW.md) and a PR template
(.github/PULL_REQUEST_TEMPLATE.md), so reviews score named dimensions
(correctness / reuse / API / naming / generality + adoption-specific
fidelity / layer / axiom-clean / #112 exposure) instead of ad-hoc judgment.
Machine gates stay in CI; the rubric covers what CI can't.
---
 .github/PULL_REQUEST_TEMPLATE.md | 20 ++++++++++++++
 .github/REVIEW.md                | 45 ++++++++++++++++++++++++++++++++
 2 files changed, 65 insertions(+)
 create mode 100644 .github/PULL_REQUEST_TEMPLATE.md
 create mode 100644 .github/REVIEW.md

diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md
new file mode 100644
index 00000000..f1c70dce
--- /dev/null
+++ b/.github/PULL_REQUEST_TEMPLATE.md
@@ -0,0 +1,20 @@
+<!-- Reviewer checklist: .github/REVIEW.md -->
+
+## What
+
+<!-- One sentence: what this PR adds or changes. -->
+
+## Checklist
+
+- [ ] Builds green (`lake build`), **no new `sorry`**
+- [ ] One concern per PR; bottom-up on the dependency cone
+- [ ] Docstrings tagged (`**Math.**` / `**Eng.**` / `**Mixed.**`)
+- [ ] Reuse checked — not already in Mathlib or OpenGALib
+- [ ] Facade theorems: `#print axioms` clean — only `propext`, `Classical.choice`, `Quot.sound`
+
+### Adoption PRs (porting from `feat/hopf-rinow`)
+
+- [ ] Faithful port — matches the `feat/hopf-rinow` version, no silent edits
+- [ ] Not a file flagged in #112 (§3.4 `Equation.lean`, §3.1 `HopfRinow.lean`), or its prerequisite fix is in
+
+<!-- Adopted from feat/hopf-rinow? Credit original authors with `Co-authored-by:` trailers. -->
diff --git a/.github/REVIEW.md b/.github/REVIEW.md
new file mode 100644
index 00000000..57440215
--- /dev/null
+++ b/.github/REVIEW.md
@@ -0,0 +1,45 @@
+# Review guide
+
+How to review a pull request here. A PR should be approved because it passed a
+**fixed, repeatable checklist** — not because it "looked fine". A PR merges when
+the machine gates are green **and** the human dimensions pass.
+
+## Machine gates — CI covers these, don't re-check by hand
+
+If CI is green, these are satisfied:
+
+- **Builds** — `lake build` succeeds.
+- **No `sorry`** — `main` is sorry-free (hard gate; sorry-WIP lives on a
+  development branch).
+- **Linters** — MathTag (docstring tags), AnchorPurity, Naming (no bare
+  initialisms like `CLM`).
+- **Unused imports** — `shake` baseline.
+
+## Human dimensions — the actual focus
+
+| Dimension | What to check |
+|---|---|
+| **Correctness** | Statement is non-vacuous; hypotheses are sound and not so strong the result is empty; the conclusion is the intended one. A predicate must mean what its name says (e.g. a "geodesic" predicate should imply continuity). |
+| **Reuse** | Not already in Mathlib or elsewhere in OpenGALib. For a "fills a Mathlib gap" lemma, confirm the gap is real. |
+| **API** | Hypotheses are minimal; instances vs explicit args used correctly; signatures are clean. |
+| **Naming** | Mathlib conventions; the name matches what is actually proved — a name must not over-claim. |
+| **Generality** | Not over-specialized; stated at the natural level of generality. |
+
+## Adoption PRs — porting a file from `feat/hopf-rinow`
+
+Most PRs toward v0.1.0 port one proven file from `feat/hopf-rinow`. Additionally:
+
+- **Faithful port** — the file matches its `feat/hopf-rinow` version; no silent
+  edits crept in (`git diff mathnetwork/feat/hopf-rinow -- <file>`).
+- **Correct layer** — a genuine leaf: every import is already on `main`
+  (bottom-up along the dependency cone).
+- **Axiom-clean** — for facade theorems, `#print axioms` shows only
+  `propext, Classical.choice, Quot.sound` — no `sorryAx`, no stray axiom.
+- **[#112](../../issues/112) exposure** — the file is not one flagged there
+  (§3.4 `Geodesic/Equation.lean`, §3.1 `Geodesic/HopfRinow.lean`); if it is,
+  the prerequisite fix must already be in.
+
+## Roles
+
+Cut PRs: @LehengChen · Review: @AxelDlv00, @JxChen24 · Approve & merge:
+@Spring-1211. See milestone [v0.1.0 — Hopf–Rinow](../../milestone/1).