Reorganize documentation and project governance

.github/ISSUE_TEMPLATE/bug.yml

@@ -0,0 +1,66 @@
+name: Bug report
+description: Report a reproducible Lean, build, documentation, or executable-example defect.
+title: "bug: "
+labels:
+  - bug
+body:
+  - type: markdown
+    attributes:
+      value: |
+        Do not include vulnerability details or secrets here. Follow `SECURITY.md` for security reports.
+  - type: input
+    id: commit
+    attributes:
+      label: Ript commit
+      description: Full commit SHA where the problem occurs.
+      placeholder: 40-character SHA
+    validations:
+      required: true
+  - type: input
+    id: module
+    attributes:
+      label: Module or document
+      placeholder: Ript/... or docs/...
+    validations:
+      required: true
+  - type: textarea
+    id: reproduction
+    attributes:
+      label: Minimal reproduction
+      description: Include the exact command and smallest source or documentation example.
+    validations:
+      required: true
+  - type: textarea
+    id: expected
+    attributes:
+      label: Expected behavior
+    validations:
+      required: true
+  - type: textarea
+    id: actual
+    attributes:
+      label: Actual behavior and output
+    validations:
+      required: true
+  - type: dropdown
+    id: boundary
+    attributes:
+      label: Affected boundary
+      options:
+        - Lean theorem or type
+        - Executable example
+        - Build or CI
+        - Documentation
+        - Public API
+        - Unsure
+    validations:
+      required: true
+  - type: checkboxes
+    id: checks
+    attributes:
+      label: Checks
+      options:
+        - label: I used the pinned toolchain from `lean-toolchain`.
+          required: true
+        - label: I searched existing issues and the research/conjecture records.
+          required: true

.github/ISSUE_TEMPLATE/config.yml

@@ -0,0 +1,8 @@
+blank_issues_enabled: true
+contact_links:
+  - name: Security report
+    url: https://github.com/miuchan/ript/security
+    about: Use a private security report when available; do not publish exploit details.
+  - name: Documentation hub
+    url: https://github.com/miuchan/ript/blob/main/docs/README.md
+    about: Find setup, architecture, status, governance, and contribution guides.

.github/ISSUE_TEMPLATE/research.yml

@@ -0,0 +1,40 @@
+name: Research or formalization proposal
+description: Propose a theorem, model, representation result, or architectural research slice.
+title: "research: "
+labels:
+  - enhancement
+body:
+  - type: textarea
+    id: statement
+    attributes:
+      label: Mathematical objective
+      description: State the intended result and hypotheses precisely enough to review.
+    validations:
+      required: true
+  - type: textarea
+    id: alignment
+    attributes:
+      label: Alignment with the research goal
+      description: Explain which RESEARCH_GOAL, BLUEPRINT, MODEL_MATRIX, or CONJECTURES boundary this advances.
+    validations:
+      required: true
+  - type: textarea
+    id: evidence
+    attributes:
+      label: Existing evidence and dependencies
+      description: Link relevant Lean declarations, Mathlib APIs, papers, or known gaps.
+    validations:
+      required: true
+  - type: textarea
+    id: slice
+    attributes:
+      label: Proposed kernel-checkable slice
+      description: Identify definitions, theorems, examples, audits, and documentation expected in one PR.
+    validations:
+      required: true
+  - type: textarea
+    id: boundary
+    attributes:
+      label: Non-goals and open directions
+    validations:
+      required: true

.github/PULL_REQUEST_TEMPLATE.md

@@ -0,0 +1,31 @@
+## Outcome
+
+<!-- What becomes true after this change? Keep this statement no stronger than the evidence. -->
+
+## Scope and remaining boundary
+
+<!-- List what is intentionally included and what remains unproved, unsupported, or out of scope. -->
+
+## Verification
+
+<!-- Paste the exact commands run and their outcomes. -->
+
+- [ ] Focused build or document check
+- [ ] `./scripts/quality-gate.sh`
+- [ ] GitHub `Lean quality gate`
+
+## Trust and compatibility
+
+- Axiom footprint:
+- Executable behavior change:
+- Public API or theorem-statement change:
+- Migration impact:
+
+## Documentation
+
+- [ ] Architecture/status/model/conjecture records updated where applicable
+- [ ] All affected language mirrors updated
+- [ ] New flagship declarations added to AxiomChecks and `AXIOMS.md`
+- [ ] Remaining research is recorded without weakening the stated goal
+
+See [CONTRIBUTING.md](../CONTRIBUTING.md) for the complete merge policy.

CONTRIBUTING.md

@@ -1,47 +1,101 @@
 # Contributing to Ript
 
-[English](docs/en/CONTRIBUTING.md) ·
-[简体中文](docs/zh-CN/CONTRIBUTING.md) ·
-[日本語](docs/ja/CONTRIBUTING.md) ·
-[Esperanto](docs/eo/CONTRIBUTING.md)
+[English](docs/en/CONTRIBUTING.md) · [简体中文](docs/zh-CN/CONTRIBUTING.md) ·
+[日本語](docs/ja/CONTRIBUTING.md) · [Esperanto](docs/eo/CONTRIBUTING.md)
 
-Ript treats proof trust, explicit dependencies, and reproducible computation as
-merge requirements rather than review conventions.
+Ript accepts proof, model, example, documentation, and tooling contributions.
+Proof trust, explicit dependencies, reproducibility, and accurate public claims
+are merge requirements.
 
-## Required quality gate
+## Before starting
 
-Run the complete gate from the repository root before opening a pull request:
+1. Read [Project scope](docs/en/PROJECT_SCOPE.md),
+   [Architecture](docs/en/ARCHITECTURE.md), and the current
+   [Research status](docs/en/RESEARCH_STATUS.md).
+2. Search existing issues and `CONJECTURES.md`.
+3. Open an issue before changing scope, public theorem statements, architecture,
+   trusted dependencies, governance, security policy, or licensing.
+4. Base work on current `main`; keep unrelated changes out of the branch.
+
+Security-sensitive reports follow [SECURITY.md](SECURITY.md), not public issue
+discussion.
+
+## Development workflow
 
 ```bash
+git switch -c <focused-branch>
+lake exe cache get
+lake build <affected.module>
 ./scripts/quality-gate.sh
 ```
 
-The gate rejects proof placeholders, project-specific axioms, unsafe
-declarations, compiler-trust escapes, broad `Mathlib` imports, implicit Lean
-identifiers, stale root-module imports, declaration-linter failures, executable
-behavior changes, build warnings, and undocumented theorem assumptions. It then
-performs a full kernel build.
+Keep commits reviewable. A pull request should explain the mathematical or
+documentation outcome, verification commands, axiom footprint, compatibility
+impact, and exact remaining boundary. Draft PRs are welcome; merge requires a
+green `Lean quality gate` and maintainer approval.
 
-CI exposes these checks as the stable `Lean quality gate` job. A change is ready
-to merge only when that job passes.
+## Lean and proof policy
 
-## Proof and dependency policy
-
-- Put unproved research statements in `CONJECTURES.md`; do not declare them as
-  theorems or axioms.
+- No `sorry`, `admit`, project-specific axioms, compiler-trust escapes, or
+  unsafe library declarations.
+- Keep `set_option autoImplicit false` in implementation modules.
 - Import the narrowest practical Mathlib modules.
-- Keep `set_option autoImplicit false` in every implementation module.
-- Add flagship theorems to both `Ript/Audit/AxiomChecks.lean` and `AXIOMS.md`.
-- If executable behavior changes intentionally, update the example assertion in
-  `scripts/check-examples.sh` in the same change.
+- Put reusable missing infrastructure under `Ript/ForMathlib/` with a narrow
+  boundary.
+- Do not present finite enumeration or `#eval` as a general theorem.
+- Record unproved statements in `CONJECTURES.md`; never weaken a theorem while
+  retaining a stronger name.
+- Add flagship declarations to `Ript/Audit/AxiomChecks.lean` and `AXIOMS.md`.
+
+## Executable and model changes
+
+- Keep executable finite data upstream from quotients and chosen semantic
+  representatives.
+- Preserve optional capability boundaries: tensor does not imply copy,
+  discard, causality, convexity, thermal, dagger, or quantum structure.
+- State whether a result is representation, soundness, conservativity,
+  sufficiency, or completeness; do not use one generic completeness claim.
+- Update `scripts/check-examples.sh` only when changed output is intentional and
+  supported by the corresponding Lean declarations.
 
 ## Documentation policy
 
-- Keep every logical page mirrored under `docs/en`, `docs/zh-CN`, `docs/ja`,
-  and `docs/eo` with the same relative path.
-- Update all four language versions when a public claim, command, status, or
-  trust boundary changes.
-- Keep root `AXIOMS.md`, `BLUEPRINT.md`, `CONJECTURES.md`, and
-  `MODEL_MATRIX.md` as the machine-facing canonical records.
-- After changing the axiom inventory, run
-  `./scripts/sync-doc-reference-tables.sh` before the quality gate.
+- Mirror each maintained page at the same path under `docs/en`, `docs/zh-CN`,
+  `docs/ja`, and `docs/eo`.
+- Update all affected languages when commands, claims, status, or trust
+  boundaries change.
+- Keep root `BLUEPRINT.md`, `MODEL_MATRIX.md`, `AXIOMS.md`, and
+  `CONJECTURES.md` as canonical machine-facing records.
+- Run `./scripts/sync-doc-reference-tables.sh` after axiom-table changes.
+- Prefer task-oriented navigation and concise overview pages; durable theorem
+  detail belongs in canonical references.
+
+## Required checks
+
+The complete pre-merge command is:
+
+```bash
+./scripts/quality-gate.sh
+```
+
+It runs source/document policy checks, root-import coverage, the full kernel
+build, declaration lint, executable examples, and the axiom allowlist. Do not
+weaken a check to make a change pass.
+
+## Pull-request checklist
+
+- [ ] The change has one clear purpose and documents its remaining boundary.
+- [ ] Affected modules build with the pinned toolchain.
+- [ ] `./scripts/quality-gate.sh` passes locally.
+- [ ] New flagship theorems have audited and documented assumptions.
+- [ ] Executable-output changes have intentional regression evidence.
+- [ ] Architecture, status, model matrix, conjectures, and all languages are
+      updated where applicable.
+- [ ] No unrelated, generated, secret, or private files are included.
+
+## Review and decisions
+
+Review checks both theorem statements and proofs; kernel acceptance alone does
+not validate modeling intent. The maintainer may request narrower scope,
+additional examples, a theorem rename, an explicit conjecture, or specialist
+review. See [GOVERNANCE.md](GOVERNANCE.md) for decision authority and stability.

GOVERNANCE.md

@@ -0,0 +1,66 @@
+# Governance
+
+[English](docs/en/GOVERNANCE.md) · [简体中文](docs/zh-CN/GOVERNANCE.md) ·
+[日本語](docs/ja/GOVERNANCE.md) · [Esperanto](docs/eo/GOVERNANCE.md)
+
+Ript is a maintainer-led formal research project. Governance is optimized for
+mathematical accuracy, kernel-checkable evidence, explicit scope boundaries,
+and reproducible decisions.
+
+## Roles
+
+- **Maintainer:** owns repository administration, scope, releases, security
+  coordination, and final merge decisions.
+- **Contributor:** proposes issues, proofs, models, documentation, or tooling
+  through reviewable changes and follows the trust and quality policies.
+- **Reviewer:** evaluates mathematical statements, Lean implementation,
+  dependencies, audits, executable evidence, and public claims. Review is a
+  responsibility, not a permanent title.
+
+The current repository owner is listed on the
+[GitHub project](https://github.com/miuchan/ript).
+
+## Decision order
+
+When evidence conflicts, decisions follow this order:
+
+1. Lean kernel acceptance under the pinned toolchain;
+2. explicit theorem types and `#print axioms` output;
+3. canonical records: `RESEARCH_GOAL.md`, `BLUEPRINT.md`, `MODEL_MATRIX.md`,
+   `AXIOMS.md`, and `CONJECTURES.md`;
+4. architecture, research-status, examples, and other explanatory prose.
+
+Passing CI is necessary but does not prove that a theorem states the intended
+mathematics. Review must check both the statement and its evidence.
+
+## Change process
+
+- Discuss scope-changing or architecture-changing work in an issue first.
+- Keep pull requests focused and state proved, executable, and open boundaries.
+- Require the complete quality gate and green protected CI before merge.
+- Record new flagship assumptions and update every affected language.
+- Use conjecture records instead of weakening a theorem or adding an axiom.
+
+The maintainer may request additional review for changes to the trusted core,
+public theorem statements, model semantics, security policy, or licensing.
+
+## Releases and compatibility
+
+There is no stable release train or compatibility guarantee. Reproducible
+research must pin a commit SHA. A future release policy must define API
+stability, migration notes, archival identifiers, and support windows before a
+version is called stable.
+
+## Community standards
+
+Be precise, constructive, and respectful. Critique statements and evidence,
+not people. Harassment, discrimination, doxxing, credential exposure, and
+deliberate misrepresentation of proof status are not accepted. Conduct or
+security-sensitive concerns should use the private path in `SECURITY.md` when
+possible.
+
+## Licensing boundary
+
+No open-source license has been selected. Governance and contribution do not
+themselves grant reuse rights. Selecting or changing a license requires an
+explicit maintainer decision and a dedicated repository change.