From 26624a8d2774eeff6fd450d98b79db82f861351b Mon Sep 17 00:00:00 2001 From: Amamiya Miu Date: Sat, 22 Aug 2026 22:34:11 +0800 Subject: [PATCH] docs: reorganize project documentation --- .github/ISSUE_TEMPLATE/bug.yml | 66 ++++++++++++++++ .github/ISSUE_TEMPLATE/config.yml | 8 ++ .github/ISSUE_TEMPLATE/research.yml | 40 ++++++++++ .github/PULL_REQUEST_TEMPLATE.md | 31 ++++++++ CONTRIBUTING.md | 116 ++++++++++++++++++++-------- GOVERNANCE.md | 66 ++++++++++++++++ README.md | 90 ++++++++++----------- SECURITY.md | 52 +++++++++++++ docs/README.md | 49 ++++++------ docs/en/ARCHITECTURE.md | 18 +++++ docs/en/CONTRIBUTING.md | 80 ++++++++++++------- docs/en/GETTING_STARTED.md | 2 + docs/en/GOVERNANCE.md | 38 +++++++++ docs/en/PROJECT_SCOPE.md | 12 ++- docs/en/README.md | 86 +++++++++------------ docs/en/RESEARCH_STATUS.md | 20 ++++- docs/en/SECURITY.md | 37 +++++++++ docs/eo/ARCHITECTURE.md | 13 ++++ docs/eo/CONTRIBUTING.md | 77 ++++++++++-------- docs/eo/GETTING_STARTED.md | 2 + docs/eo/GOVERNANCE.md | 37 +++++++++ docs/eo/PROJECT_SCOPE.md | 9 +++ docs/eo/README.md | 79 ++++++++----------- docs/eo/RESEARCH_STATUS.md | 20 ++++- docs/eo/SECURITY.md | 30 +++++++ docs/ja/ARCHITECTURE.md | 10 +++ docs/ja/CONTRIBUTING.md | 54 ++++++++----- docs/ja/GETTING_STARTED.md | 2 + docs/ja/GOVERNANCE.md | 29 +++++++ docs/ja/PROJECT_SCOPE.md | 7 ++ docs/ja/README.md | 67 +++++++--------- docs/ja/RESEARCH_STATUS.md | 16 +++- docs/ja/SECURITY.md | 27 +++++++ docs/zh-CN/ARCHITECTURE.md | 9 +++ docs/zh-CN/CONTRIBUTING.md | 57 +++++++++----- docs/zh-CN/GETTING_STARTED.md | 2 + docs/zh-CN/GOVERNANCE.md | 28 +++++++ docs/zh-CN/PROJECT_SCOPE.md | 9 ++- docs/zh-CN/README.md | 58 ++++++-------- docs/zh-CN/RESEARCH_STATUS.md | 14 +++- docs/zh-CN/SECURITY.md | 28 +++++++ scripts/check-doc-locales.sh | 12 +++ 42 files changed, 1140 insertions(+), 367 deletions(-) create mode 100644 .github/ISSUE_TEMPLATE/bug.yml create mode 100644 .github/ISSUE_TEMPLATE/config.yml create mode 100644 .github/ISSUE_TEMPLATE/research.yml create mode 100644 .github/PULL_REQUEST_TEMPLATE.md create mode 100644 GOVERNANCE.md create mode 100644 SECURITY.md create mode 100644 docs/en/GOVERNANCE.md create mode 100644 docs/en/SECURITY.md create mode 100644 docs/eo/GOVERNANCE.md create mode 100644 docs/eo/SECURITY.md create mode 100644 docs/ja/GOVERNANCE.md create mode 100644 docs/ja/SECURITY.md create mode 100644 docs/zh-CN/GOVERNANCE.md create mode 100644 docs/zh-CN/SECURITY.md diff --git a/.github/ISSUE_TEMPLATE/bug.yml b/.github/ISSUE_TEMPLATE/bug.yml new file mode 100644 index 0000000..fcbafae --- /dev/null +++ b/.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 diff --git a/.github/ISSUE_TEMPLATE/config.yml b/.github/ISSUE_TEMPLATE/config.yml new file mode 100644 index 0000000..082966e --- /dev/null +++ b/.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. diff --git a/.github/ISSUE_TEMPLATE/research.yml b/.github/ISSUE_TEMPLATE/research.yml new file mode 100644 index 0000000..74e87c5 --- /dev/null +++ b/.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 diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md new file mode 100644 index 0000000..dd32688 --- /dev/null +++ b/.github/PULL_REQUEST_TEMPLATE.md @@ -0,0 +1,31 @@ +## Outcome + + + +## Scope and remaining boundary + + + +## Verification + + + +- [ ] 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. diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 65ab433..f76c818 100644 --- a/CONTRIBUTING.md +++ b/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 +lake exe cache get +lake build ./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. diff --git a/GOVERNANCE.md b/GOVERNANCE.md new file mode 100644 index 0000000..c051b85 --- /dev/null +++ b/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. diff --git a/README.md b/README.md index 13769f5..eca3573 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ # Ript -**A kernel-checked Lean 4 foundation for resource-indexed process theories.** +**Kernel-checked foundations for resource-indexed information processes.** [English](docs/en/README.md) · [简体中文](docs/zh-CN/README.md) · [日本語](docs/ja/README.md) · [Esperanto](docs/eo/README.md) @@ -8,62 +8,64 @@ [![Quality Gate](https://github.com/miuchan/ript/actions/workflows/ci.yml/badge.svg)](https://github.com/miuchan/ript/actions/workflows/ci.yml) ![Lean 4.33.0](https://img.shields.io/badge/Lean-4.33.0-0d6efd) ![mathlib 4.33.0](https://img.shields.io/badge/mathlib-4.33.0-a42e2b) -![Research status](https://img.shields.io/badge/status-early--stage%20research-orange) +![Status](https://img.shields.io/badge/status-early--stage%20research-orange) +![License](https://img.shields.io/badge/license-not%20selected-lightgrey) -Ript formalizes typed processes whose behavior and resource use compose. It -connects executable finite models with kernel-checked results about resource -bounds, soundness, completeness, and structure-preserving semantics. -Its first literal six-model slice interprets one Boolean process signature in -probabilistic, quantum, causal, computational, semantic, and thermal models. - -Its governing research objective is to construct a computable, -machine-verifiable, univalent, higher-categorical theory of -resource-constrained information processes in which classical probability, -quantum processes, causal models, computation, semantic information, and -thermodynamics arise as distinct models, together with representation and -completeness theorems relating those models. The repository contains the -compiled layers toward that objective; the objective as a whole is not yet a -proved theorem. +Ript is a Lean 4 research library for typed processes whose behavior and +resource use compose. It keeps executable finite syntax separate from +quotient-based semantic layers and connects classical probability, quantum +processes, causal models, computation, task-relative semantic information, +and thermodynamics through structure-preserving interpretations. > [!IMPORTANT] -> Ript is early-stage research software. Compiled results are kernel checked; -> the public API and research frontier are still evolving. +> Ript is early-stage research software. Kernel-checked declarations are real +> proofs, but the public API and the global research theorem are not complete. + +## Verified today -## Get started +- executable sequential, monoidal, adaptive, dependent, and parallel syntax + with exact costs and budgets; +- soundness, term-model relative completeness, free/initial semantics, and + several model-specific representation or completeness theorems; +- concrete finite probabilistic, quantum, causal, computational, semantic, + decision, and thermodynamic models with nontrivial executable examples; +- a total resource-model bicategory and internally interpreted univalent, + simplicial, and complete-Segal foundations; +- a full generated-hammock mapping-space presentation, direct target nerve + equivalences, and a terminating semantics-preserving reduction layer. -Install [elan](https://github.com/leanprover/elan), then build the pinned Lean -and Mathlib project: +The active frontier is raw critical-pair joinability, classical reduced +hammock invariance, a standard weak-equivalence interface, and the final global +Dwyer--Kan/Rezk theorem. See [Research status](docs/en/RESEARCH_STATUS.md). + +## Quick start ```bash git clone https://github.com/miuchan/ript.git cd ript lake exe cache get -lake build +./scripts/quality-gate.sh ``` -For prerequisites, executable examples, dependency setup, reproducibility, and -troubleshooting, follow [Getting started](docs/en/GETTING_STARTED.md). - -## Find what you need +The repository pins Lean and Mathlib. Follow [Getting started](docs/en/GETTING_STARTED.md) +for prerequisites, focused commands, examples, dependency use, and troubleshooting. -- **What is implemented?** See the - [model capability matrix](docs/en/reference/MODEL_MATRIX.md). -- **What is proved or still open?** See the - [research status](docs/en/RESEARCH_STATUS.md). -- **How is the library organized?** Read the - [architecture guide](docs/en/ARCHITECTURE.md). -- **What are the trust and maturity boundaries?** Read - [project scope and trust](docs/en/PROJECT_SCOPE.md). -- **Where are the exact research records?** Use the - [formal blueprint](docs/en/reference/BLUEPRINT.md), - [axiom inventory](docs/en/reference/AXIOMS.md), and - [conjecture register](docs/en/reference/CONJECTURES.md). -- **Not sure where to begin?** Open the [documentation hub](docs/README.md). +## Documentation -## Contributing +- **Learn the system:** [Project scope](docs/en/PROJECT_SCOPE.md) · + [Architecture](docs/en/ARCHITECTURE.md) +- **Inspect current evidence:** [Research status](docs/en/RESEARCH_STATUS.md) · + [Model matrix](docs/en/reference/MODEL_MATRIX.md) +- **Audit exact claims:** [Blueprint](docs/en/reference/BLUEPRINT.md) · + [Axioms](docs/en/reference/AXIOMS.md) · + [Conjectures](docs/en/reference/CONJECTURES.md) +- **Work on Ript:** [Contributing](CONTRIBUTING.md) · [Governance](GOVERNANCE.md) · + [Security](SECURITY.md) +- **Choose another language:** [Documentation hub](docs/README.md) -Read the [contributing guide](docs/en/CONTRIBUTING.md), then run -`./scripts/quality-gate.sh` before opening a pull request. +## Reuse and citation -Ript is built with [Lean 4](https://lean-lang.org/) and -[Mathlib](https://github.com/leanprover-community/mathlib4). +Pin a full commit SHA for reproducible research and record the audited theorem +assumptions. No open-source license has been selected: public availability does +not currently grant permission to copy, modify, or redistribute the code. See +[Project scope and trust](docs/en/PROJECT_SCOPE.md) for the exact boundary. diff --git a/SECURITY.md b/SECURITY.md new file mode 100644 index 0000000..bb1ecee --- /dev/null +++ b/SECURITY.md @@ -0,0 +1,52 @@ +# Security policy + +[English](docs/en/SECURITY.md) · [简体中文](docs/zh-CN/SECURITY.md) · +[日本語](docs/ja/SECURITY.md) · [Esperanto](docs/eo/SECURITY.md) + +Ript is a formal research library, not a hosted service. Security work focuses +on the integrity of the proof boundary, executable examples, dependency and CI +supply chain, and unsafe behavior in code that consumers may execute. + +## Supported versions + +Only the current `main` branch is supported. Ript has no stable releases or +backport policy. Reports should name the exact commit SHA and pinned toolchain. + +## Report privately + +Use GitHub's **Security** tab and private vulnerability reporting when it is +available. If GitHub does not offer a private form, open a public issue that +contains only a request for a private contact channel—do not include exploit +details, credentials, or unpublished vulnerability information. + +Include: + +- affected commit and module; +- impact and realistic threat scenario; +- minimal reproduction or proof of concept; +- whether the issue affects kernel trust, generated executable code, CI, + dependencies, or documentation only; +- any known mitigation. + +## What counts as a security issue + +- a proof-trust escape, hidden project axiom, unsafe declaration, or way to + bypass the documented quality gate; +- executable code that violates its stated input or resource boundary; +- compromised or unpinned CI/dependency behavior; +- accidental secret or private-data exposure; +- a dependency vulnerability that is reachable from Ript's supported use. + +A disagreement about a mathematical model, an unproved conjecture already +listed as open, or an API instability is normally a research or bug report, +not a security vulnerability. + +## Response and disclosure + +The maintainer will acknowledge and triage reports on a best-effort basis; +early-stage research software has no guaranteed service-level agreement. Fixes +must preserve the same kernel, axiom-audit, and CI requirements as other +changes. Coordinate public disclosure until a fix or documented mitigation is +available. + +Never include secrets in an issue, pull request, test fixture, or Lean trace. diff --git a/docs/README.md b/docs/README.md index f85ce30..3480a11 100644 --- a/docs/README.md +++ b/docs/README.md @@ -1,40 +1,41 @@ # Ript documentation · Ript 文档 · Ript ドキュメント · Dokumentaro de Ript -Every maintained document is available through the same mirrored path in four -languages. Choose a language to enter the documentation set. +The documentation is mirrored at the same paths in English, Simplified +Chinese, Japanese, and Esperanto. Select a language, then navigate by task. -所有维护中的文档都按相同路径提供四种语言版本，请选择语言进入文档集。 +文档按相同路径提供英语、简体中文、日语和世界语版本。请选择语言，再按任务阅读。 -保守対象の全ドキュメントは、同じパス構成で四言語版を提供します。言語を選択してください。 +ドキュメントは英語・簡体字中国語・日本語・エスペラントで同じパス構成です。言語を選び、 +目的別に進んでください。 -Ĉiu prizorgata dokumento disponeblas laŭ la sama spegulita vojo en kvar lingvoj. -Elektu lingvon por eniri la dokumentaron. +La sama dokumentstrukturo disponeblas en la angla, simpligita ĉina, japana kaj +Esperanto. Elektu lingvon kaj poste taskon. -## Languages · 语言 · 言語 · Lingvoj +## Choose a language · 选择语言 · 言語を選択 · Elektu lingvon - [English](en/README.md) - [简体中文](zh-CN/README.md) - [日本語](ja/README.md) - [Esperanto](eo/README.md) -## Mirrored structure · 镜像结构 · ミラー構成 · Spegulita strukturo +## Documentation map -Each locale contains `README.md`, `GETTING_STARTED.md`, `ARCHITECTURE.md`, -`PROJECT_SCOPE.md`, `RESEARCH_STATUS.md`, `CONTRIBUTING.md`, and a `reference/` -directory containing `MODEL_MATRIX.md`, `BLUEPRINT.md`, `AXIOMS.md`, and -`CONJECTURES.md`. +| Goal | English | 简体中文 | 日本語 | Esperanto | +|---|---|---|---|---| +| Build and run examples | [Guide](en/GETTING_STARTED.md) | [指南](zh-CN/GETTING_STARTED.md) | [ガイド](ja/GETTING_STARTED.md) | [Gvidilo](eo/GETTING_STARTED.md) | +| Understand scope and trust | [Scope](en/PROJECT_SCOPE.md) | [范围](zh-CN/PROJECT_SCOPE.md) | [範囲](ja/PROJECT_SCOPE.md) | [Amplekso](eo/PROJECT_SCOPE.md) | +| Understand the codebase | [Architecture](en/ARCHITECTURE.md) | [架构](zh-CN/ARCHITECTURE.md) | [構成](ja/ARCHITECTURE.md) | [Arkitekturo](eo/ARCHITECTURE.md) | +| See the current frontier | [Status](en/RESEARCH_STATUS.md) | [状态](zh-CN/RESEARCH_STATUS.md) | [状況](ja/RESEARCH_STATUS.md) | [Stato](eo/RESEARCH_STATUS.md) | +| Contribute | [Guide](en/CONTRIBUTING.md) | [指南](zh-CN/CONTRIBUTING.md) | [ガイド](ja/CONTRIBUTING.md) | [Gvidilo](eo/CONTRIBUTING.md) | +| Understand decisions | [Governance](en/GOVERNANCE.md) | [治理](zh-CN/GOVERNANCE.md) | [ガバナンス](ja/GOVERNANCE.md) | [Regado](eo/GOVERNANCE.md) | +| Report a vulnerability | [Security](en/SECURITY.md) | [安全](zh-CN/SECURITY.md) | [セキュリティ](ja/SECURITY.md) | [Sekureco](eo/SECURITY.md) | -每个语言目录都包含上述六篇入口与指南，并在 `reference/` 中包含模型矩阵、形式化蓝图、公理清单和 -猜想登记册。各语言路径一一对应，页面顶部可以直接切换语言。 +## Authoritative records -各言語ディレクトリには六つの入口・ガイドと、モデル行列、形式化ブループリント、公理一覧、 -予想台帳を収めた `reference/` があります。各ページ上部から同じ文書の言語を切り替えられます。 +The root [`BLUEPRINT.md`](../BLUEPRINT.md), [`MODEL_MATRIX.md`](../MODEL_MATRIX.md), +[`AXIOMS.md`](../AXIOMS.md), and [`CONJECTURES.md`](../CONJECTURES.md) are +machine-facing canonical records. English reference pages mirror their full +content; localized references preserve identifiers and proved/open boundaries. -Ĉiu lingva dosierujo enhavas la ses enirejajn kaj gvidajn paĝojn, plus -`reference/` kun la modelmatrico, formala plano, aksioma inventaro kaj registro -de konjektoj. La lingvoŝaltilo ĉe la supro konservas la saman dokumenton. - -The root `AXIOMS.md`, `BLUEPRINT.md`, `CONJECTURES.md`, and `MODEL_MATRIX.md` -remain machine-facing canonical records used by validation scripts. Their -English mirrors preserve the full canonical content; localized reference pages -preserve the same status boundaries and formal identifiers. +Lean declarations and audit output take precedence over prose. A public claim +change must update all four maintained languages in the same pull request. diff --git a/docs/en/ARCHITECTURE.md b/docs/en/ARCHITECTURE.md index a13ed6d..a8917a1 100644 --- a/docs/en/ARCHITECTURE.md +++ b/docs/en/ARCHITECTURE.md @@ -152,6 +152,22 @@ Localization work is split by strength: - unproved coherence or essential-surjectivity fields are never replaced by axioms. +The current mapping-space stack has three explicit presentations: + +1. binary marked-zigzag words with quotient 2-cells; +2. independent right-associated linear hammock rows; +3. generated non-groupoidal hammock paths combining executable refinements + with arbitrary aligned raw cells. + +All three are categorically equivalent to the actual localization-target local +hom-categories. Their nerve comparisons have explicit simplicial homotopy +inverses, and the generated comparison factors strictly through the linear +one. A terminating administrative reduction removes units/nesting, fuses +adjacent moves, and cancels executable refinement inverses while preserving +quotient semantics. Raw critical-pair joinability, the full classical +arbitrary-grid move system, and standard weak-equivalence packaging remain +research boundaries. + ## Internal univalent interpretation `Ript/Univalent/` is downstream from the ordinary process theory. It defines: @@ -192,6 +208,8 @@ Ript separates project communication from formal status: - `BLUEPRINT.md` records dependencies and theorem-level status; - `CONJECTURES.md` contains statements not yet proved; - `AXIOMS.md` records actual kernel assumptions. +- `GOVERNANCE.md` records decision authority and stability policy; +- `SECURITY.md` records private reporting and the supported trust boundary. When these disagree, Lean declarations and machine-checked audit output take precedence. Documentation changes should reconcile the human-facing files in diff --git a/docs/en/CONTRIBUTING.md b/docs/en/CONTRIBUTING.md index c8973df..ff72856 100644 --- a/docs/en/CONTRIBUTING.md +++ b/docs/en/CONTRIBUTING.md @@ -3,43 +3,67 @@ [English](CONTRIBUTING.md) · [简体中文](../zh-CN/CONTRIBUTING.md) · [日本語](../ja/CONTRIBUTING.md) · [Esperanto](../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. +Trust, explicit dependencies, reproducibility, and accurate claims are merge +requirements. -## Required quality gate +## Before starting -Run the complete gate from the repository root before opening a pull request: +Read [Scope](PROJECT_SCOPE.md), [Architecture](ARCHITECTURE.md), and +[Research status](RESEARCH_STATUS.md); search issues and the +[Conjecture register](reference/CONJECTURES.md). Discuss changes to scope, +public theorem statements, architecture, trusted dependencies, governance, +security, or licensing before implementation. Security reports follow +[Security policy](SECURITY.md). + +## Workflow ```bash +git switch -c +lake exe cache get +lake build ./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. - -CI exposes these checks as the stable `Lean quality gate` job. A change is ready -to merge only when that job passes. +Keep branches and commits focused. PRs must state the outcome, verification, +axiom footprint, compatibility impact, and remaining boundary. Drafts are +welcome; merge requires green CI and maintainer approval. -## Proof and dependency policy +## Proof and implementation policy -- Put unproved research statements in `CONJECTURES.md`; do not declare them as - theorems or axioms. -- 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. +- No proof placeholders, project axioms, trust escapes, or unsafe declarations. +- Keep `autoImplicit false`; use narrow Mathlib imports. +- Put reusable missing infrastructure in `Ript/ForMathlib/`. +- Keep executable data upstream from quotients and chosen representatives. +- Preserve capability boundaries and use domain-accurate theorem names. +- Put unfinished statements in `CONJECTURES.md`. +- Audit flagship declarations in `Ript/Audit/AxiomChecks.lean` and `AXIOMS.md`. +- Update executable assertions only for intentional, proved behavior changes. ## 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 maintained pages under all four locales. Update every affected language +when a command, claim, status, or trust boundary changes. Canonical root +blueprint, model, axiom, and conjecture records remain machine-facing sources. +Run `./scripts/sync-doc-reference-tables.sh` after axiom-table changes. + +## Required gate + +```bash +./scripts/quality-gate.sh +``` + +The gate checks source and docs policy, root imports, the full kernel build, +declaration lint, executable examples, and audited assumptions. Never weaken a +check to make a change pass. + +## PR checklist + +- [ ] One clear purpose and an explicit remaining boundary. +- [ ] Focused and full builds pass with the pinned toolchain. +- [ ] Flagship assumptions and executable changes are audited. +- [ ] Architecture, status, references, and all affected locales are current. +- [ ] No unrelated, generated, secret, or private files are included. + +Review evaluates statements and modeling intent as well as proof terms. See +[Governance](GOVERNANCE.md) for authority and stability policy. diff --git a/docs/en/GETTING_STARTED.md b/docs/en/GETTING_STARTED.md index bef33d5..bfaff32 100644 --- a/docs/en/GETTING_STARTED.md +++ b/docs/en/GETTING_STARTED.md @@ -181,3 +181,5 @@ the new output is intentional and proved by the corresponding example module. - [Architecture](ARCHITECTURE.md) for module and dependency boundaries. - [Research status](RESEARCH_STATUS.md) for the current mathematical frontier. - [Formal blueprint](reference/BLUEPRINT.md) for theorem-level status. +- [Contributing](CONTRIBUTING.md) for the development and review workflow. +- [Governance](GOVERNANCE.md) and [Security](SECURITY.md) for project policy. diff --git a/docs/en/GOVERNANCE.md b/docs/en/GOVERNANCE.md new file mode 100644 index 0000000..9e9721b --- /dev/null +++ b/docs/en/GOVERNANCE.md @@ -0,0 +1,38 @@ +# Governance + +[English](GOVERNANCE.md) · [简体中文](../zh-CN/GOVERNANCE.md) · +[日本語](../ja/GOVERNANCE.md) · [Esperanto](../eo/GOVERNANCE.md) + +Ript is a maintainer-led formal research project. Decisions prioritize +mathematical accuracy, kernel-checkable evidence, explicit boundaries, and +reproducibility. + +## Roles + +- The maintainer owns scope, repository administration, releases, security, + and final merge decisions. +- Contributors propose focused, reviewable proofs, models, documentation, and + tooling. +- Reviewers evaluate theorem statements, Lean code, dependencies, audits, + executable evidence, and public claims. + +## Authority and decisions + +Conflicts are resolved in this order: pinned Lean kernel acceptance; theorem +types and axiom output; canonical goal/blueprint/model/axiom/conjecture records; +then explanatory documentation. CI is necessary but does not replace +mathematical review. + +Discuss scope or architecture changes first, keep pull requests focused, run +the complete quality gate, update all affected languages and audits, and keep +unfinished work in the conjecture register. + +## Stability and community + +There is no stable release or API guarantee; pin a commit SHA. Be precise, +constructive, and respectful. Harassment, discrimination, doxxing, credential +exposure, and misrepresentation of proof status are not accepted. + +No open-source license has been selected. A license decision requires an +explicit maintainer change. See the canonical root [governance](../../GOVERNANCE.md) +and [security policy](SECURITY.md). diff --git a/docs/en/PROJECT_SCOPE.md b/docs/en/PROJECT_SCOPE.md index 61ed677..a987862 100644 --- a/docs/en/PROJECT_SCOPE.md +++ b/docs/en/PROJECT_SCOPE.md @@ -53,6 +53,14 @@ interchange, and pentagon/triangle coherence. The [model capability matrix](reference/MODEL_MATRIX.md) records only implemented and compiled operations. +The highest compiled localization layer now gives a full generated-hammock +presentation of every local mapping category, direct categorical-nerve +equivalences to the actual localization targets, explicit simplicial homotopy +inverses, and a terminating semantics-preserving administrative reduction. +This is an audited project-local Dwyer--Kan core. It is not yet a comparison +with the classical reduced arbitrary-grid hammock construction or a standard +global Rezk weak-equivalence theorem. + ## Trust model Ript forbids: @@ -92,8 +100,10 @@ will be replaced by the chosen license if the project adopts one. ## Authoritative records -- [Research status](RESEARCH_STATUS.md): concise proved/open boundary. +- [Research status](RESEARCH_STATUS.md): current narrative proved/open boundary. - [Formal blueprint](reference/BLUEPRINT.md): theorem types and dependency ledger. - [Axiom inventory](reference/AXIOMS.md): audited kernel assumptions. - [Conjecture register](reference/CONJECTURES.md): open research statements. - [Contributing guide](CONTRIBUTING.md): proof and merge policy. +- [Governance](GOVERNANCE.md): decision authority and stability. +- [Security](SECURITY.md): reporting and supported trust boundary. diff --git a/docs/en/README.md b/docs/en/README.md index 5de7c5b..1ef96aa 100644 --- a/docs/en/README.md +++ b/docs/en/README.md @@ -1,68 +1,58 @@ -# Ript - -**A kernel-checked Lean 4 foundation for resource-indexed process theories.** +# Ript documentation [English](README.md) · [简体中文](../zh-CN/README.md) · [日本語](../ja/README.md) · [Esperanto](../eo/README.md) -[![Quality Gate](https://github.com/miuchan/ript/actions/workflows/ci.yml/badge.svg)](https://github.com/miuchan/ript/actions/workflows/ci.yml) -![Lean 4.33.0](https://img.shields.io/badge/Lean-4.33.0-0d6efd) -![mathlib 4.33.0](https://img.shields.io/badge/mathlib-4.33.0-a42e2b) -![Research status](https://img.shields.io/badge/status-early--stage%20research-orange) +Ript is a kernel-checked Lean 4 research library for resource-indexed +information processes. It connects executable finite syntax with +probabilistic, quantum, causal, computational, semantic-information, decision, +and thermodynamic models while keeping optional capabilities separate. -Ript formalizes typed processes whose behavior and resource use compose. It -connects executable finite models with kernel-checked results about resource -bounds, soundness, completeness, and structure-preserving semantics. -Its first literal six-model slice interprets one Boolean process signature in -probabilistic, quantum, causal, computational, semantic, and thermal models. +> [!IMPORTANT] +> The repository contains substantial proved infrastructure, but remains +> early-stage research. The final global theorem and a stable API are open. -Its governing research objective is to construct a computable, -machine-verifiable, univalent, higher-categorical theory of -resource-constrained information processes in which classical probability, -quantum processes, causal models, computation, semantic information, and -thermodynamics arise as distinct models, together with representation and -completeness theorems relating those models. The repository contains the -compiled layers toward that objective; the objective as a whole is not yet a -proved theorem. +## Current snapshot -> [!IMPORTANT] -> Ript is early-stage research software. Compiled results are kernel checked; -> the public API and research frontier are still evolving. +- exact resource-sensitive syntax, budgets, soundness, relative completeness, + and free semantics compile; +- all six model families have concrete instances and checked nontrivial + examples; +- models and resource-changing morphisms form verified bicategorical layers; +- internally univalent and complete-Segal foundations are downstream of the + executable core; +- generated hammock mapping spaces are equivalent to the actual localization + targets, with explicit nerve homotopy inverses and terminating reductions. -## Get started +The current frontier is critical-pair joinability, classical reduced-hammock +invariance, standard weak-equivalence packaging, and the global Rezk theorem. -Install [elan](https://github.com/leanprover/elan), then build the pinned Lean -and Mathlib project: +## Start here ```bash git clone https://github.com/miuchan/ript.git cd ript lake exe cache get -lake build +./scripts/quality-gate.sh ``` -For prerequisites, executable examples, dependency setup, reproducibility, and -troubleshooting, follow [Getting started](GETTING_STARTED.md). - -## Find what you need +Continue with [Getting started](GETTING_STARTED.md). -- **What is implemented?** See the - [model capability matrix](reference/MODEL_MATRIX.md). -- **What is proved or still open?** See the - [research status](RESEARCH_STATUS.md). -- **How is the library organized?** Read the - [architecture guide](ARCHITECTURE.md). -- **What are the trust and maturity boundaries?** Read - [project scope and trust](PROJECT_SCOPE.md). -- **Where are the exact research records?** Use the - [formal blueprint](reference/BLUEPRINT.md), - [axiom inventory](reference/AXIOMS.md), and - [conjecture register](reference/CONJECTURES.md). +## Read by task -## Contributing +- **Understand the project:** [Scope and trust](PROJECT_SCOPE.md) · + [Architecture](ARCHITECTURE.md) +- **See what is proved:** [Research status](RESEARCH_STATUS.md) · + [Model matrix](reference/MODEL_MATRIX.md) +- **Audit exact evidence:** [Blueprint](reference/BLUEPRINT.md) · + [Axioms](reference/AXIOMS.md) · [Conjectures](reference/CONJECTURES.md) +- **Participate:** [Contributing](CONTRIBUTING.md) · + [Governance](GOVERNANCE.md) · [Security](SECURITY.md) +- **Switch language:** [Multilingual documentation hub](../README.md) -Read [CONTRIBUTING.md](CONTRIBUTING.md), then run -`./scripts/quality-gate.sh` before opening a pull request. +## Maturity and reuse -Ript is built with [Lean 4](https://lean-lang.org/) and -[Mathlib](https://github.com/leanprover-community/mathlib4). +Use a full commit SHA for reproducibility. There are no stable releases or API +compatibility guarantees. No open-source license has been selected, so public +source availability does not grant reuse rights; see +[Project scope](PROJECT_SCOPE.md#licensing). diff --git a/docs/en/RESEARCH_STATUS.md b/docs/en/RESEARCH_STATUS.md index 3f0a103..f5e6bfc 100644 --- a/docs/en/RESEARCH_STATUS.md +++ b/docs/en/RESEARCH_STATUS.md @@ -3,10 +3,28 @@ [English](RESEARCH_STATUS.md) · [简体中文](../zh-CN/RESEARCH_STATUS.md) · [日本語](../ja/RESEARCH_STATUS.md) · [Esperanto](../eo/RESEARCH_STATUS.md) -This page is a concise research map, not the theorem ledger. Exact theorem +This page is the maintained narrative research map, not the theorem ledger. Exact theorem types, dependencies, source files, and assumptions live in [`BLUEPRINT.md`](reference/BLUEPRINT.md) and [`AXIOMS.md`](reference/AXIOMS.md). +## Current snapshot + +**Verified:** executable resource-sensitive syntax and budgets; soundness, +relative completeness, and free semantics; concrete six-family model slices; +fixed and changing-resource model bicategories; internal univalent and +complete-Segal foundations; full generated-hammock mapping categories with +direct target nerve equivalences; and a terminating semantics-preserving +administrative reduction with irreducible reducts. + +**Open:** raw critical-pair joinability and local confluence, the remaining +classical arbitrary-grid hammock moves, reduced-hammock homotopical invariance, +a standard derived weak-equivalence interface, and the final global +Dwyer--Kan/Rezk theorem. The governing objective remains active. + +Use the [model matrix](reference/MODEL_MATRIX.md) for capability-level answers, +the [blueprint](reference/BLUEPRINT.md) for theorem-level evidence, and the +[conjecture register](reference/CONJECTURES.md) for unproved directions. + ## Status vocabulary Ript uses only these formal status labels in the blueprint: diff --git a/docs/en/SECURITY.md b/docs/en/SECURITY.md new file mode 100644 index 0000000..7d9e395 --- /dev/null +++ b/docs/en/SECURITY.md @@ -0,0 +1,37 @@ +# Security policy + +[English](SECURITY.md) · [简体中文](../zh-CN/SECURITY.md) · +[日本語](../ja/SECURITY.md) · [Esperanto](../eo/SECURITY.md) + +Ript is a formal research library, not a hosted service. Security covers proof +trust, executable examples, dependency and CI integrity, and unsafe behavior +that could affect consumers. + +## Supported versions + +Only current `main` is supported. Include the exact commit SHA and pinned Lean +toolchain in every report; there is no release backport policy. + +## Private reporting + +Use GitHub's **Security** tab and private vulnerability reporting when +available. Otherwise open a public issue containing only a request for a +private channel. Never publish exploit details, credentials, or private data. + +Include the affected module and commit, impact, realistic threat scenario, +minimal reproduction, affected trust boundary, and known mitigation. + +## Security scope + +Security issues include trust escapes, hidden axioms, unsafe declarations, +quality-gate bypasses, reachable dependency/CI compromise, executable boundary +violations, secret exposure, and private-data leaks. A documented conjecture, +modeling disagreement, or unstable API is normally a research or bug report. + +## Response and disclosure + +Reports are handled on a best-effort basis without a guaranteed SLA. Fixes +must pass the normal kernel, audit, and CI requirements. Coordinate disclosure +until a fix or mitigation is available. + +See the canonical root [security policy](../../SECURITY.md). diff --git a/docs/eo/ARCHITECTURE.md b/docs/eo/ARCHITECTURE.md index a0e7afb..4606d77 100644 --- a/docs/eo/ARCHITECTURE.md +++ b/docs/eo/ARCHITECTURE.md @@ -117,6 +117,17 @@ Lokalizado estas dividita laŭ forto: - aparta preciza predikato de la bikategoria universala eco; - neniu anstataŭigo de nepruvita kohereco aŭ esenca surĵeteco per aksiomoj. +La nuna mapspaca stako havas tri eksplicitajn prezentojn: duumaj marked- +zigzag-vortoj kun kvocientaj 2-ĉeloj, sendependaj dekstre-asociaj linearaj +hammock-vicoj, kaj negrupoida generita hammock-vojaro kun plenumeblaj +refinement-oj kaj arbitraj aligned krudaj ĉeloj. Ĉiuj estas kategorie +ekvivalentaj al la faktaj lokaj hom-kategorioj de la lokaliza celo; la nervaj +komparoj havas eksplicitajn homotopiajn inversojn, kaj la generita komparo +strikte faktoriĝas tra la lineara. Finiĝanta administra redukto forigas unuojn +kaj nestadon, kunfandas apudajn movojn kaj nuligas refinement-inversojn dum ĝi +konservas kvocientan semantikon. Kruda critical-pair joinability, la plena +klasika arbitra-krada movaro kaj norma malfort-ekvivalenta pako restas malfermaj. + ## Interna univalenta interpreto `Ript/Univalent/` difinas profundajn interfackodojn, apartajn sintaksojn por @@ -143,6 +154,8 @@ kaj matricaj pruvoj troviĝas en semantikaj tavoloj kaj povas esti nekomputeblaj - `reference/BLUEPRINT.md`: dependecoj kaj teoremnivela stato; - `reference/CONJECTURES.md`: nepruvitaj asertoj; - `reference/AXIOMS.md`: realaj kernaj supozoj. +- `GOVERNANCE.md`: decida aŭtoritato kaj stabileca politiko; +- `SECURITY.md`: privata raportado kaj la subtenata fidolimo. Se ili malkongruas, Lean-deklaroj kaj maŝine kontrolita audito superas. La sama tirpeto devas rekunordigi la dokumentaron. diff --git a/docs/eo/CONTRIBUTING.md b/docs/eo/CONTRIBUTING.md index 83dcd92..f700b1c 100644 --- a/docs/eo/CONTRIBUTING.md +++ b/docs/eo/CONTRIBUTING.md @@ -3,42 +3,55 @@ [English](../en/CONTRIBUTING.md) · [简体中文](../zh-CN/CONTRIBUTING.md) · [日本語](../ja/CONTRIBUTING.md) · [Esperanto](CONTRIBUTING.md) -Ript traktas pruvan fidon, eksplicitajn dependecojn kaj reprodukteblan -komputadon kiel kunfandajn postulojn, ne nur reviziajn kutimojn. +Ript akceptas kontribuojn pri pruvoj, modeloj, ekzemploj, dokumentoj kaj iloj. +Fido, eksplicitaj dependecoj, reprodukteblo kaj precizaj asertoj estas +kunfandaj postuloj. -## Deviga kvalita kontrolo +## Antaŭ ol komenci -Rulu en la radiko de la deponejo: +Legu [Amplekson](PROJECT_SCOPE.md), [Arkitekturon](ARCHITECTURE.md) kaj +[Esploran staton](RESEARCH_STATUS.md); serĉu issues kaj la +[konjektregistron](reference/CONJECTURES.md). Diskutu ŝanĝojn de amplekso, +publikaj teoremoj, arkitekturo, fiddependecoj, regado, sekureco aŭ permesilo +antaŭ realigo. Sekurecaj raportoj sekvas [Sekurecon](SECURITY.md). + +## Laborfluo ```bash +git switch -c +lake exe cache get +lake build ./scripts/quality-gate.sh ``` -La kontrolo rifuzas pruvtruojn, projektajn aksiomojn, nesekurajn deklarojn, -evitojn de kompilila fido, tro larĝajn `Mathlib`-importojn, implicitajn Lean- -identigilojn, malnovajn radikajn importojn, deklarajn erarojn, ŝanĝitan ruleblan -konduton, konstruajn avertojn kaj nedokumentitajn teoremajn supozojn. Poste ĝi -faras plenan kernan konstruon. - -CI prezentas la samajn kontrolojn kiel `Lean quality gate`. Ŝanĝo estas preta -por kunfando nur kiam tiu tasko sukcesas. - -## Politiko pri pruvoj kaj dependecoj - -- metu nepruvitajn esplorasertojn en `CONJECTURES.md`, ne en teoremojn aŭ aksiomojn; -- importu la plej mallarĝajn praktikajn Mathlib-modulojn; -- konservu `set_option autoImplicit false` en ĉiu realiga modulo; -- aldonu ĉefajn teoremojn al `Ript/Audit/AxiomChecks.lean` kaj `AXIOMS.md`; -- se rulebla konduto intence ŝanĝiĝas, ĝisdatigu la aserton en - `scripts/check-examples.sh` en la sama ŝanĝo. - -## Dokumentara politiko - -- konservu ĉiun logikan paĝon laŭ la sama relativa vojo sub `docs/en`, - `docs/zh-CN`, `docs/ja` kaj `docs/eo`; -- ĝisdatigu ĉiujn kvar lingvojn kiam publika aserto, komando, stato aŭ fidolimo - ŝanĝiĝas; -- konservu la radikajn `AXIOMS.md`, `BLUEPRINT.md`, `CONJECTURES.md` kaj - `MODEL_MATRIX.md` kiel maŝinajn kanonajn registrojn; -- post ŝanĝo de la aksioma inventaro rulu - `./scripts/sync-doc-reference-tables.sh` antaŭ la kvalita kontrolo. +Tenu branĉojn kaj commit-ojn fokusaj. PR devas klarigi rezulton, kontroladon, +aksiomojn, kongruecon kaj restantajn limojn. Kunfando postulas verdan CI kaj +aprobon de la prizorganto. + +## Pruva kaj realiga politiko + +- neniuj pruvtruoj, projektaj aksiomoj, fid-evitoj aŭ unsafe-deklaroj; +- konservu `autoImplicit false` kaj mallarĝajn Mathlib-importojn; +- metu ĝeneralan mankantan bazon en `Ript/ForMathlib/`; +- tenu ruleblajn datumojn kontraŭflue de kvocientoj kaj elektitaj reprezentantoj; +- konservu kapablolimojn kaj domajn-precizajn teoremnomojn; +- registru nefinitajn asertojn en `CONJECTURES.md`; +- auditu ĉefajn deklarojn en AxiomChecks kaj `AXIOMS.md`. + +## Dokumentoj kaj kontrolo + +Spegulu paĝojn laŭ la sama vojo en kvar lingvoj kaj sinkronigu publikajn +ŝanĝojn. Post aksiomaj ŝanĝoj rulu `./scripts/sync-doc-reference-tables.sh`. +La deviga `./scripts/quality-gate.sh` kontrolas dokumentojn, radikajn importojn, +plenan konstruon, lint, ekzemplojn kaj aksiomojn. + +## PR-listo + +- [ ] unu celo kaj klara restanta limo; +- [ ] fokusita kaj plena konstruoj sukcesas; +- [ ] ĉefaj supozoj kaj ruleblaj ŝanĝoj estas audititaj; +- [ ] arkitekturo, stato, referencoj kaj lingvoj estas aktualaj; +- [ ] neniuj nerilataj, generitaj, sekretaj aŭ privataj dosieroj. + +Revizio kontrolas ankaŭ la teoreman aserton kaj modelan intencon. Vidu +[Regadon](GOVERNANCE.md). diff --git a/docs/eo/GETTING_STARTED.md b/docs/eo/GETTING_STARTED.md index c4f358a..3c32f87 100644 --- a/docs/eo/GETTING_STARTED.md +++ b/docs/eo/GETTING_STARTED.md @@ -178,3 +178,5 @@ se la nova eliro estas intenca kaj pruvita de la koncerna ekzempla modulo. - [Arkitekturo](ARCHITECTURE.md) - [Esplora stato](RESEARCH_STATUS.md) - [Formala plano](reference/BLUEPRINT.md) +- [Kontribua gvidilo](CONTRIBUTING.md) +- [Regado](GOVERNANCE.md) kaj [Sekureco](SECURITY.md) diff --git a/docs/eo/GOVERNANCE.md b/docs/eo/GOVERNANCE.md new file mode 100644 index 0000000..eb4b448 --- /dev/null +++ b/docs/eo/GOVERNANCE.md @@ -0,0 +1,37 @@ +# Regado + +[English](../en/GOVERNANCE.md) · [简体中文](../zh-CN/GOVERNANCE.md) · +[日本語](../ja/GOVERNANCE.md) · [Esperanto](GOVERNANCE.md) + +Ript estas prizorgant-gvidata formala esplorprojekto. Decidoj prioritatas +matematikan ĝustecon, kern-kontroleblan pruvon, klarajn limojn kaj +reprodukteblon. + +## Roloj + +- la prizorganto respondecas pri amplekso, administrado, eldonoj, sekureco kaj + finaj kunfandoj; +- kontribuantoj proponas fokusitajn, revizieblajn pruvojn, modelojn, dokumentojn + aŭ ilojn; +- reviziantoj kontrolas teoremojn, Lean-kodon, dependecojn, auditojn, ruleblan + pruvon kaj publikajn asertojn. + +## Aŭtoritato kaj decidoj + +Konfliktoj sekvas ĉi tiun ordon: Lean-kerno kun la fiksita ilĉeno; teoremaj +tipoj kaj aksiomaj eligoj; kanonaj goal/blueprint/model/axiom/conjecture- +registroj; poste klariga prozo. CI estas necesa sed ne anstataŭas matematikan +revizion. + +Diskutu ampleksajn aŭ arkitekturajn ŝanĝojn unue, tenu PR-on fokusa, rulu la +plenan kontrolon, ĝisdatigu ĉiujn trafitajn lingvojn kaj auditojn, kaj registru +nefaritan laboron kiel konjekton. + +## Stabileco kaj komunumo + +Ne ekzistas stabila eldono aŭ API-garantio; fiksu commit-SHA. Estu preciza, +konstruema kaj respektema. Ĉikano, diskriminacio, privata-datuma aŭ akreditaĵa +malkaŝo kaj intenca misprezento de pruvstato ne estas akceptataj. + +Neniu malfermfonta permesilo estas elektita. Vidu la [radikan regadon](../../GOVERNANCE.md) +kaj [sekurecan politikon](SECURITY.md). diff --git a/docs/eo/PROJECT_SCOPE.md b/docs/eo/PROJECT_SCOPE.md index d49162e..ec0c11b 100644 --- a/docs/eo/PROJECT_SCOPE.md +++ b/docs/eo/PROJECT_SCOPE.md @@ -46,6 +46,13 @@ identec-semantikon. Ordigitaj adiciaj rimedŝanĝoj ligas malsamajn rimedalgebro en totalan bikategorion. La [modelkapabla matrico](reference/MODEL_MATRIX.md) registras nur realigitajn kaj kompilitajn operaciojn. +La plej alta kompilita lokaliza tavolo nun donas plenan generitan hammock- +prezenton de ĉiu loka mapkategorio, rektajn kategoria-nervajn ekvivalentojn al +la faktaj lokalizaj celoj, eksplicitajn simpliciajn homotopiajn inversojn kaj +finiĝantan semantik-konservan administran redukton. Tio estas auditita +projekta Dwyer--Kan-kerno, ne ankoraŭ komparo kun la klasika reduktita arbitra- +krada hammock aŭ norma tutmonda Rezk-malforta ekvivalento. + ## Fidmodelo Ript malpermesas: @@ -85,3 +92,5 @@ ne donas permeson kopii, modifi aŭ redistribui ĝin. Formala permesilo anstata - [Aksioma inventaro](reference/AXIOMS.md) - [Registro de konjektoj](reference/CONJECTURES.md) - [Kontribua gvidilo](CONTRIBUTING.md) +- [Regado](GOVERNANCE.md) +- [Sekureco](SECURITY.md) diff --git a/docs/eo/README.md b/docs/eo/README.md index d6f4ea4..7d71043 100644 --- a/docs/eo/README.md +++ b/docs/eo/README.md @@ -1,65 +1,54 @@ -# Ript - -**Kern-kontrolita Lean 4-fundamento por rimed-indeksitaj procezteorioj.** +# Dokumentaro de Ript [English](../en/README.md) · [简体中文](../zh-CN/README.md) · [日本語](../ja/README.md) · [Esperanto](README.md) -[![Quality Gate](https://github.com/miuchan/ript/actions/workflows/ci.yml/badge.svg)](https://github.com/miuchan/ript/actions/workflows/ci.yml) -![Lean 4.33.0](https://img.shields.io/badge/Lean-4.33.0-0d6efd) -![mathlib 4.33.0](https://img.shields.io/badge/mathlib-4.33.0-a42e2b) -![Esplora stato](https://img.shields.io/badge/status-early--stage%20research-orange) +Ript estas kern-kontrolita Lean 4-esplorbiblioteko por rimed-indeksitaj +informprocezoj. Ĝi ligas ruleblan finian sintakson kun probablaj, kvantumaj, +kaŭzaj, komputaj, semantik-informaj, decidaj kaj termodinamikaj modeloj, dum +laŭvolaj kapabloj restas apartaj. -Ript formaligas tipizitajn procezojn, kies konduto kaj rimeduzo kunmetiĝas. Ĝi -ligas ruleblajn finiajn modelojn al kern-kontrolitaj rezultoj pri rimedlimoj, -valideco, kompleteco kaj struktur-konserva semantiko. -La unua efektiva ses-modela tranĉo interpretas unu Bulean procezan signaturon -en probablaj, kvantumaj, kaŭzaj, komputaj, semantikaj kaj termikaj modeloj. +> [!IMPORTANT] +> La deponejo enhavas multe da veraj pruvoj, sed restas frufaza esploro. La +> fina tutmonda teoremo kaj stabila API ankoraŭ ne ekzistas. -La centra esplorcelo de Ript estas konstrui komputeblan, maŝine kontroleblan, -univalentan kaj pli-alt-kategorian teorion de rimed-limigitaj informprocezoj, en -kiu klasika probablo, kvantumaj procezoj, kaŭzaj modeloj, komputado, semantika -informo kaj termodinamiko aperas kiel malsamaj modeloj, kun reprezentaj kaj -kompletecaj teoremoj kiuj ilin rilatigas. La deponejo enhavas la kompilitajn -tavolojn direkte al tiu celo; la tuta celo ankoraŭ ne estas pruvita teoremo. +## Nuna stato -> [!IMPORTANT] -> Ript estas frufaza esplora programaro. La kompilitaj rezultoj estas -> kern-kontrolitaj; la publika API kaj la esplora fronto ankoraŭ evoluas. +- rimed-sentema sintakso, buĝetoj, valideco, relativa kompleteco kaj libera + semantiko kompiliĝas; +- ĉiuj ses modelfamilioj havas konkretajn okazojn kaj kontrolitajn ekzemplojn; +- modeloj kaj rimedŝanĝaj morfioj formas kontrolitajn bikategoriajn tavolojn; +- interna univalento kaj complete-Segal-fundamentoj restas laŭflue de la + rulebla kerno; +- generitaj hammock-mapspacoj ekvivalentas al la faktaj lokalizaj celoj kaj + havas eksplicitajn nervajn homotopiajn inversojn kaj finiĝantan redukton. -## Rapida komenco +La fronto estas critical-pair joinability, klasika reduced-hammock-invarianto, +norma malfort-ekvivalenta pako kaj la tutmonda Rezk-teoremo. -Instalu [elan](https://github.com/leanprover/elan), poste konstruu la projekton -kun ĝiaj fiksitaj versioj de Lean kaj Mathlib: +## Komencu ĉi tie ```bash git clone https://github.com/miuchan/ript.git cd ript lake exe cache get -lake build +./scripts/quality-gate.sh ``` -Por postuloj, ruleblaj ekzemploj, dependaĵa uzo, reproduktebleco kaj -problemsolvado, sekvu la [komencan gvidilon](GETTING_STARTED.md). - -## Trovu tion, kion vi bezonas +Daŭrigu per la [komenca gvidilo](GETTING_STARTED.md). -- **Kio estas realigita?** Vidu la [matricon de modelkapabloj](reference/MODEL_MATRIX.md). -- **Kio estas pruvita aŭ ankoraŭ malferma?** Vidu la - [esploran staton](RESEARCH_STATUS.md). -- **Kiel la biblioteko estas organizita?** Legu la - [arkitekturan gvidilon](ARCHITECTURE.md). -- **Kiuj estas la fidaj kaj maturecaj limoj?** Legu - [projektan amplekson kaj fidon](PROJECT_SCOPE.md). -- **Kie estas la precizaj esplorregistroj?** Uzu la - [formalan planon](reference/BLUEPRINT.md), - [aksioman inventaron](reference/AXIOMS.md) kaj - [registron de konjektoj](reference/CONJECTURES.md). +## Legu laŭ tasko -## Kontribuado +- **Kompreni:** [Amplekso kaj fido](PROJECT_SCOPE.md) · [Arkitekturo](ARCHITECTURE.md) +- **Vidi pruvojn:** [Esplora stato](RESEARCH_STATUS.md) · [Modelmatrico](reference/MODEL_MATRIX.md) +- **Auditi:** [Plano](reference/BLUEPRINT.md) · [Aksiomoj](reference/AXIOMS.md) · + [Konjektoj](reference/CONJECTURES.md) +- **Partopreni:** [Kontribui](CONTRIBUTING.md) · [Regado](GOVERNANCE.md) · + [Sekureco](SECURITY.md) +- **Ŝanĝi lingvon:** [Plurlingva dokumentara nabo](../README.md) -Legu la [kontribuan gvidilon](CONTRIBUTING.md) kaj rulu -`./scripts/quality-gate.sh` antaŭ ol malfermi tirpeton. +## Matureco kaj reuzo -Ript estas konstruita per [Lean 4](https://lean-lang.org/) kaj -[Mathlib](https://github.com/leanprover-community/mathlib4). +Fiksu plenan commit-SHA por reprodukteblo. Ne ekzistas stabila eldono aŭ API- +garantio. Neniu malfermfonta permesilo estas elektita; publika videbleco ne +donas rajton kopii, ŝanĝi aŭ redistribui. diff --git a/docs/eo/RESEARCH_STATUS.md b/docs/eo/RESEARCH_STATUS.md index 49d29f2..7857c02 100644 --- a/docs/eo/RESEARCH_STATUS.md +++ b/docs/eo/RESEARCH_STATUS.md @@ -3,10 +3,28 @@ [English](../en/RESEARCH_STATUS.md) · [简体中文](../zh-CN/RESEARCH_STATUS.md) · [日本語](../ja/RESEARCH_STATUS.md) · [Esperanto](RESEARCH_STATUS.md) -Ĉi tiu paĝo estas konciza esplormapo, ne la teorema registro. Ekzaktaj tipoj, +Ĉi tiu paĝo estas prizorgata rakonta esplormapo, ne la teorema registro. Ekzaktaj tipoj, dependecoj, fontoj kaj supozoj troviĝas en la [formala plano](reference/BLUEPRINT.md) kaj la [aksioma inventaro](reference/AXIOMS.md). +## Nuna resumo + +**Kontrolita:** rulebla rimed-sentema sintakso kaj buĝetoj; valideco, relativa +kompleteco kaj libera semantiko; konkretaj ses-modelaj tranĉoj; fiks- kaj +ŝanĝ-rimedaj modelaj bikategorioj; interna univalento kaj complete-Segal- +fundamentoj; plenaj generitaj hammock-mapkategorioj kun rektaj celaj nervaj +ekvivalentoj; kaj finiĝanta semantik-konserva administra redukto kun +nereblaj reduktaĵoj. + +**Malferma:** kruda critical-pair joinability kaj loka kunflueco, ceteraj +klasikaj arbitra-kradaj hammock-movoj, reduced-hammock homotopia invarianto, +norma derivita malfort-ekvivalenta interfaco kaj la fina tutmonda +Dwyer--Kan/Rezk-teoremo. La reganta esplorcelo restas aktiva. + +Uzu la [modelmatricon](reference/MODEL_MATRIX.md) por kapabloj, la +[planon](reference/BLUEPRINT.md) por teoremaj pruvoj kaj la +[konjektregistron](reference/CONJECTURES.md) por nepruvitaj direktoj. + ## Statusvortoj - `DEFINED` — interfaco aŭ konstruo ekzistas; diff --git a/docs/eo/SECURITY.md b/docs/eo/SECURITY.md new file mode 100644 index 0000000..4b07db7 --- /dev/null +++ b/docs/eo/SECURITY.md @@ -0,0 +1,30 @@ +# Sekureca politiko + +[English](../en/SECURITY.md) · [简体中文](../zh-CN/SECURITY.md) · +[日本語](../ja/SECURITY.md) · [Esperanto](SECURITY.md) + +Ript estas formala esplorbiblioteko, ne gastigita servo. Sekureco ampleksas +pruvan fidon, ruleblajn ekzemplojn, dependecon kaj CI-integron, kaj nesekuran +konduton kiu povus damaĝi uzantojn. + +## Subteno + +Nur la nuna `main` estas subtenata. Raporto devas nomi la plenan commit-SHA kaj +la fiksitan Lean-ilĉenon; ne ekzistas retroporta politiko. + +## Privata raportado + +Uzu privatan vundeblan raportadon en la GitHub **Security**-langeto se ĝi +disponeblas. Alie malfermu nur minimuman publikan peton por privata kanalo; ne +publikigu ekspluaton, akreditaĵojn aŭ privatajn datumojn. + +Inkludu modulon kaj commit, efikon, realisman minacon, minimuman reprodukton, +trafitan fidolimon kaj konatan mildigon. + +## Amplekso kaj respondo + +Fid-evitoj, kaŝitaj aksiomoj, unsafe-deklaroj, kontrolpordaj preteriroj, +atingeblaj dependeco/CI-kompromisoj, ruleblaj limrompoj kaj sekreta elfluo estas +sekurecaj. Registrita konjekto, modela malkonsento aŭ malstabila API ordinare ne +estas. Respondo estas laŭeble sen SLA; korekto devas pasi la normalajn kernajn, +auditajn kaj CI-kontrolojn. Vidu la [radikan politikon](../../SECURITY.md). diff --git a/docs/ja/ARCHITECTURE.md b/docs/ja/ARCHITECTURE.md index b7b7598..db4f9e0 100644 --- a/docs/ja/ARCHITECTURE.md +++ b/docs/ja/ARCHITECTURE.md @@ -107,6 +107,14 @@ Ript は、実行可能な有限モデルが商、測度論、高次圏、内部 - 独立に定義された厳密な双圏的普遍性述語 - 未証明の整合性や本質的全射性を公理で代用しない方針 +現在の mapping-space スタックには、二分 marked-zigzag word/商 2-cell、独立な右結合 linear +hammock 行、実行可能 refinement と任意 aligned raw cell を組み合わせる非群胚 generated hammock +path の三表示があります。すべて実際の局所化対象の local hom-category と圏同値で、nerve 比較は +明示的単体ホモトピー逆を持ち、generated 比較は linear 比較を厳密に経由します。停止する +administrative reduction は単位・入れ子を除去し、隣接 move を融合し、実行可能 refinement 正逆対を +消去しながら商意味論を保存します。raw critical-pair joinability、完全な古典的任意 grid move、 +標準弱同値包装は未解決です。 + ## 内部ユニバレント解釈 `Ript/Univalent/` は通常の過程理論の下流で、深いインターフェース符号、内部構造同値と恒等の @@ -131,6 +139,8 @@ Ript は、実行可能な有限モデルが商、測度論、高次圏、内部 - `reference/BLUEPRINT.md`：依存関係と定理単位の状態 - `reference/CONJECTURES.md`：未証明命題 - `reference/AXIOMS.md`：実際のカーネル仮定 +- `GOVERNANCE.md`：意思決定権限と安定性方針 +- `SECURITY.md`：非公開報告と対応する信頼境界 不一致があれば Lean 宣言と機械監査を優先し、同じ PR で文書を整合させます。 diff --git a/docs/ja/CONTRIBUTING.md b/docs/ja/CONTRIBUTING.md index cb00bad..6155bba 100644 --- a/docs/ja/CONTRIBUTING.md +++ b/docs/ja/CONTRIBUTING.md @@ -3,34 +3,50 @@ [English](../en/CONTRIBUTING.md) · [简体中文](../zh-CN/CONTRIBUTING.md) · [日本語](CONTRIBUTING.md) · [Esperanto](../eo/CONTRIBUTING.md) -Ript は証明の信頼性、明示的依存関係、再現可能な計算をレビュー慣習ではなくマージ要件とします。 +証明、モデル、例、文書、ツールの貢献を受け付けます。信頼性、明示的依存、再現性、正確な公開主張は +マージ要件です。 -## 必須品質ゲート +## 開始前 -リポジトリルートで実行してください。 +[範囲](PROJECT_SCOPE.md)、[アーキテクチャ](ARCHITECTURE.md)、[研究状況](RESEARCH_STATUS.md)、 +issue と[予想台帳](reference/CONJECTURES.md)を確認します。範囲、公開定理、構成、信頼依存、 +ガバナンス、セキュリティ、ライセンスの変更は先に議論してください。脆弱性は +[セキュリティポリシー](SECURITY.md)に従います。 + +## ワークフロー ```bash +git switch -c +lake exe cache get +lake build ./scripts/quality-gate.sh ``` -ゲートは証明穴、独自公理、unsafe 宣言、コンパイラ信頼回避、広すぎる `Mathlib` import、暗黙の -Lean 識別子、古いルート import、宣言 lint エラー、実行動作の変化、ビルド警告、未文書化の仮定を -拒否し、完全なカーネルビルドを行います。 +ブランチと commit を集中させ、PR に成果、検証、公理依存、互換性、残る境界を書きます。 +マージには CI 成功とメンテナ承認が必要です。 + +## 証明・実装方針 + +- 証明穴、独自公理、信頼回避、unsafe 宣言は禁止 +- `autoImplicit false` と狭い Mathlib import を維持 +- 汎用基盤は `Ript/ForMathlib/` へ配置 +- 実行データを商・選択代表の上流に保つ +- 能力境界と分野に正確な定理名を維持 +- 未完了命題は `CONJECTURES.md` へ記録 +- 主要宣言を AxiomChecks と `AXIOMS.md` で監査 -CI の安定ジョブ名は `Lean quality gate` です。これが成功した変更だけをマージできます。 +## 文書と品質ゲート -## 証明と依存関係の方針 +保守ページを四言語で同じパスに置き、公開変更を同期します。公理表の変更後は +`./scripts/sync-doc-reference-tables.sh` を実行します。必須の +`./scripts/quality-gate.sh` は文書、根 import、全ビルド、lint、例、公理を検査します。 -- 未証明の研究命題は `CONJECTURES.md` に置き、定理や公理として宣言しない -- 実用上もっとも狭い Mathlib モジュールを import する -- 全実装モジュールで `set_option autoImplicit false` を維持する -- 主要定理を `Ript/Audit/AxiomChecks.lean` と `AXIOMS.md` の両方に追加する -- 実行動作を意図的に変更する場合、同じ変更で `scripts/check-examples.sh` の期待値を更新する +## PR チェック -## ドキュメント方針 +- [ ] 目的と残る境界が明確 +- [ ] 固定ツールチェーンで局所・全体ビルド成功 +- [ ] 主要仮定と実行変更を監査済み +- [ ] 構成、状況、参照、全対象言語が最新 +- [ ] 無関係・生成・秘密・私有ファイルなし -- 全論理ページを同じ相対パスで `docs/en`、`docs/zh-CN`、`docs/ja`、`docs/eo` に配置する -- 公開主張、コマンド、状態、信頼境界を変更したときは四言語すべてを更新する -- ルートの `AXIOMS.md`、`BLUEPRINT.md`、`CONJECTURES.md`、`MODEL_MATRIX.md` を - 機械的正本として維持する -- 公理一覧の変更後は `./scripts/sync-doc-reference-tables.sh` を実行してから品質ゲートを実行する +レビューは証明だけでなく定理文とモデル意図も確認します。[ガバナンス](GOVERNANCE.md)を参照してください。 diff --git a/docs/ja/GETTING_STARTED.md b/docs/ja/GETTING_STARTED.md index 8f2850e..4a52548 100644 --- a/docs/ja/GETTING_STARTED.md +++ b/docs/ja/GETTING_STARTED.md @@ -175,3 +175,5 @@ API が不安定な間は、パッケージ版だけでは再現に不十分で - [アーキテクチャ](ARCHITECTURE.md) - [研究状況](RESEARCH_STATUS.md) - [形式化ブループリント](reference/BLUEPRINT.md) +- [コントリビューション](CONTRIBUTING.md) +- [ガバナンス](GOVERNANCE.md)と[セキュリティ](SECURITY.md) diff --git a/docs/ja/GOVERNANCE.md b/docs/ja/GOVERNANCE.md new file mode 100644 index 0000000..daf466d --- /dev/null +++ b/docs/ja/GOVERNANCE.md @@ -0,0 +1,29 @@ +# ガバナンス + +[English](../en/GOVERNANCE.md) · [简体中文](../zh-CN/GOVERNANCE.md) · +[日本語](GOVERNANCE.md) · [Esperanto](../eo/GOVERNANCE.md) + +Ript はメンテナ主導の形式研究プロジェクトです。数学的正確性、カーネル検査可能な証拠、明示的境界、 +再現性を優先します。 + +## 役割 + +- メンテナは範囲、管理、リリース、セキュリティ、最終マージを担当する +- コントリビュータは焦点のある証明・モデル・文書・ツール変更を提案する +- レビュアーは定理、Lean 実装、依存、監査、実行証拠、公開主張を確認する + +## 権威と意思決定 + +競合時の順序は、固定ツールチェーンの Lean カーネル、定理型と公理出力、goal/blueprint/model/ +axiom/conjecture の正本、説明文書です。CI は必須ですが数学レビューを代替しません。 + +範囲・構成変更は先に議論し、PR を集中させ、完全品質ゲートを実行し、影響する全言語と監査を +更新し、未完了事項は予想台帳へ残します。 + +## 安定性とコミュニティ + +安定版や API 保証はないため commit SHA を固定します。正確・建設的・敬意ある交流を求め、 +ハラスメント、差別、個人情報暴露、資格情報漏洩、証明状態の故意の偽装を認めません。 + +オープンソースライセンスは未選択です。正本は[ルートガバナンス](../../GOVERNANCE.md)と +[セキュリティ](SECURITY.md)です。 diff --git a/docs/ja/PROJECT_SCOPE.md b/docs/ja/PROJECT_SCOPE.md index ece1be9..1a33f61 100644 --- a/docs/ja/PROJECT_SCOPE.md +++ b/docs/ja/PROJECT_SCOPE.md @@ -37,6 +37,11 @@ Ript は形式研究ライブラリであり、実時間推定器でも完成済 交換則、五角形・三角形整合性を持つ全双圏に束ねます。実装済み操作は [モデル能力行列](reference/MODEL_MATRIX.md)だけに記載します。 +最上位の局所化層は、各 local mapping category の完全な generated-hammock 表示、実際の局所化対象への +直接 categorical-nerve 同値、明示的単体ホモトピー逆、停止して意味論を保存する administrative +reduction を与えます。これは監査済みプロジェクト内 Dwyer--Kan core であり、古典的 reduced 任意 +grid hammock との比較や標準大域 Rezk 弱同値定理ではありません。 + ## 信頼モデル 次を禁止します。 @@ -74,3 +79,5 @@ Ript は形式研究ライブラリであり、実時間推定器でも完成済 - [公理一覧](reference/AXIOMS.md) - [予想台帳](reference/CONJECTURES.md) - [コントリビューションガイド](CONTRIBUTING.md) +- [ガバナンス](GOVERNANCE.md) +- [セキュリティ](SECURITY.md) diff --git a/docs/ja/README.md b/docs/ja/README.md index 20958c6..464c5df 100644 --- a/docs/ja/README.md +++ b/docs/ja/README.md @@ -1,58 +1,49 @@ -# Ript - -**資源添字付きプロセス理論のための、カーネル検証済み Lean 4 基盤。** +# Ript ドキュメント [English](../en/README.md) · [简体中文](../zh-CN/README.md) · [日本語](README.md) · [Esperanto](../eo/README.md) -[![Quality Gate](https://github.com/miuchan/ript/actions/workflows/ci.yml/badge.svg)](https://github.com/miuchan/ript/actions/workflows/ci.yml) -![Lean 4.33.0](https://img.shields.io/badge/Lean-4.33.0-0d6efd) -![mathlib 4.33.0](https://img.shields.io/badge/mathlib-4.33.0-a42e2b) -![研究状況](https://img.shields.io/badge/status-early--stage%20research-orange) +Ript は資源添字付き情報過程のための Lean 4 カーネル検証済み研究ライブラリです。実行可能な +有限構文を、確率・量子・因果・計算・意味情報・意思決定・熱力学モデルへ接続し、任意能力を +分離して扱います。 -Ript は、振る舞いと資源使用を合成できる型付きプロセスを形式化し、実行可能な有限モデルを -資源上界・健全性・完全性・構造保存意味論のカーネル検証済み結果へ接続します。 -最初の六モデル共通スライスでは、同じ Boolean 過程シグネチャを確率、量子、因果、計算、意味、 -熱モデルで解釈します。 +> [!IMPORTANT] +> 多くの実証済み基盤がありますが、初期研究段階です。最終大域定理と安定 API は未完成です。 -Ript の中心的な研究目標は、計算可能・機械検証可能・ユニヴァレントかつ高次圏論的な -資源制約付き情報プロセス理論を構築し、古典確率、量子プロセス、因果モデル、計算、 -意味情報、熱力学をその異なるモデルとして与え、それらを結ぶ表現定理と完全性定理を -証明することです。本リポジトリにはこの目標へ向かうコンパイル済みの層がありますが、 -目標全体がすでに証明済みであるという意味ではありません。 +## 現在のスナップショット -> [!IMPORTANT] -> Ript は初期段階の研究ソフトウェアです。コンパイル済み結果はカーネル検証されていますが、 -> 公開 API と研究の最前線は現在も変化しています。 +- 資源感応構文、予算、健全性、相対完全性、自由意味論がコンパイル済み +- 六モデル族すべてに具体インスタンスと検査済み非自明例がある +- モデルと資源変換射は検証済み双圏層を形成する +- 内部ユニヴァレンスと complete-Segal 基盤は実行可能コアの下流にある +- generated hammock mapping space は実際の局所化対象と同値で、明示的 nerve ホモトピー逆と + 停止する簡約を持つ -## クイックスタート +現在の最前線は critical-pair joinability、古典的 reduced-hammock 不変性、標準弱同値包装、 +大域 Rezk 定理です。 -[elan](https://github.com/leanprover/elan) をインストールし、固定された Lean と Mathlib の -プロジェクトをビルドします。 +## はじめに ```bash git clone https://github.com/miuchan/ript.git cd ript lake exe cache get -lake build +./scripts/quality-gate.sh ``` -要件、実行可能な例、依存利用、再現可能性、トラブルシューティングは -[導入ガイド](GETTING_STARTED.md)を参照してください。 - -## 目的別ガイド +続きは[導入ガイド](GETTING_STARTED.md)を参照してください。 -- **何が実装済みか？** [モデル機能行列](reference/MODEL_MATRIX.md) -- **何が証明済みで、何が未解決か？** [研究状況](RESEARCH_STATUS.md) -- **ライブラリはどう構成されているか？** [アーキテクチャ](ARCHITECTURE.md) -- **信頼境界と成熟度は？** [プロジェクトの範囲と信頼境界](PROJECT_SCOPE.md) -- **正確な研究記録は？** [形式化ブループリント](reference/BLUEPRINT.md)、 - [公理一覧](reference/AXIOMS.md)、[予想台帳](reference/CONJECTURES.md) +## 目的別に読む -## コントリビューション +- **プロジェクトを理解：** [範囲と信頼境界](PROJECT_SCOPE.md) · [アーキテクチャ](ARCHITECTURE.md) +- **証明済み内容を見る：** [研究状況](RESEARCH_STATUS.md) · [モデル機能行列](reference/MODEL_MATRIX.md) +- **厳密な証拠を監査：** [ブループリント](reference/BLUEPRINT.md) · + [公理](reference/AXIOMS.md) · [予想](reference/CONJECTURES.md) +- **参加する：** [コントリビューション](CONTRIBUTING.md) · [ガバナンス](GOVERNANCE.md) · + [セキュリティ](SECURITY.md) +- **言語を変更：** [多言語ドキュメントハブ](../README.md) -[コントリビューションガイド](CONTRIBUTING.md)を読み、PR の前に -`./scripts/quality-gate.sh` を実行してください。 +## 成熟度と再利用 -Ript は [Lean 4](https://lean-lang.org/) と -[Mathlib](https://github.com/leanprover-community/mathlib4) で構築されています。 +再現可能性には完全な commit SHA を固定してください。安定リリースや API 互換保証はありません。 +オープンソースライセンスは未選択で、公開表示だけでは複製・変更・再配布権を与えません。 diff --git a/docs/ja/RESEARCH_STATUS.md b/docs/ja/RESEARCH_STATUS.md index 2550e39..4dbcfcd 100644 --- a/docs/ja/RESEARCH_STATUS.md +++ b/docs/ja/RESEARCH_STATUS.md @@ -3,9 +3,23 @@ [English](../en/RESEARCH_STATUS.md) · [简体中文](../zh-CN/RESEARCH_STATUS.md) · [日本語](RESEARCH_STATUS.md) · [Esperanto](../eo/RESEARCH_STATUS.md) -これは簡潔な研究地図であり、定理台帳ではありません。正確な型、依存関係、ソース、仮定は +これは保守される叙述的な研究地図であり、定理台帳ではありません。正確な型、依存関係、ソース、仮定は [形式化ブループリント](reference/BLUEPRINT.md)と[公理一覧](reference/AXIOMS.md)にあります。 +## 現在のスナップショット + +**検証済み：** 実行可能な資源感応構文と予算、健全性・相対完全性・自由意味論、六モデル族の +具体スライス、固定/変資源モデル双圏、内部ユニヴァレンスと complete-Segal 基盤、実際の対象 nerve +へ直接同値な完全 generated-hammock mapping category、既約 reduct を持つ停止・意味保存 +administrative reduction。 + +**未解決：** raw critical-pair joinability と局所合流性、残る古典的任意 grid hammock move、 +reduced-hammock ホモトピー不変性、標準 derived 弱同値インターフェース、最終大域 +Dwyer--Kan/Rezk 定理。統一研究目標は継続中です。 + +機能は[モデル行列](reference/MODEL_MATRIX.md)、定理証拠は[ブループリント](reference/BLUEPRINT.md)、 +未証明方向は[予想台帳](reference/CONJECTURES.md)を参照してください。 + ## 状態語彙 - `DEFINED`：インターフェースまたは構成が存在する diff --git a/docs/ja/SECURITY.md b/docs/ja/SECURITY.md new file mode 100644 index 0000000..80269f0 --- /dev/null +++ b/docs/ja/SECURITY.md @@ -0,0 +1,27 @@ +# セキュリティポリシー + +[English](../en/SECURITY.md) · [简体中文](../zh-CN/SECURITY.md) · +[日本語](SECURITY.md) · [Esperanto](../eo/SECURITY.md) + +Ript は形式研究ライブラリであり、ホスト型サービスではありません。証明信頼境界、実行例、依存・ +CI の完全性、利用者へ影響する unsafe な動作をセキュリティ範囲とします。 + +## サポート対象 + +現在の `main` のみを対象とします。完全な commit SHA と固定 Lean ツールチェーンを記載してください。 + +## 非公開報告 + +GitHub の **Security** タブに private vulnerability reporting があれば使用してください。利用できない +場合、非公開連絡経路を求める最小限の issue だけを公開し、悪用手順・認証情報・私有データを +書かないでください。 + +対象モジュールと commit、影響、現実的脅威、最小再現、信頼境界、既知の緩和策を含めます。 + +## 対象と対応 + +信頼回避、隠れた公理、unsafe 宣言、品質ゲート回避、到達可能な依存/CI 侵害、実行境界違反、 +秘密漏洩が対象です。登録済み予想、モデル論争、不安定 API は通常の研究・バグ報告です。 + +対応はベストエフォートで SLA はありません。修正は通常のカーネル・監査・CI を通過し、修正または +緩和まで公開を調整してください。正本は[ルートポリシー](../../SECURITY.md)です。 diff --git a/docs/zh-CN/ARCHITECTURE.md b/docs/zh-CN/ARCHITECTURE.md index 5fa07dc..ef5a8de 100644 --- a/docs/zh-CN/ARCHITECTURE.md +++ b/docs/zh-CN/ARCHITECTURE.md @@ -108,6 +108,13 @@ Ript 的组织原则是：可执行有限模型不依赖商类型、测度论、 - 精确的双范畴泛性质谓词单独定义； - 尚未证明的协调或本质满性字段绝不会以公理代替。 +当前 mapping-space 栈具有三种显式呈示：二叉 marked-zigzag word/商 2-胞腔、独立右结合 linear +hammock 行，以及把可执行 refinement 与任意 aligned raw cell 组合起来的非群胚 generated hammock +path。三者均已与实际局部化目标的 local hom-category 建立范畴等价，nerve 比较具有显式单纯同伦逆， +generated 比较严格经过 linear 比较。一个终止 administrative reduction 会消去单位/嵌套、融合相邻 +move 并抵消可执行 refinement 正逆对，同时保持商语义。raw critical-pair joinability、完整经典任意 +网格 move 系统与标准弱等价封装仍是研究边界。 + ## 内部单值解释 `Ript/Univalent/` 位于普通过程理论下游，定义： @@ -138,6 +145,8 @@ Ript 将项目沟通与形式状态分开： - `reference/BLUEPRINT.md` 记录依赖与定理级状态； - `reference/CONJECTURES.md` 记录未证明陈述； - `reference/AXIOMS.md` 记录实际内核假设。 +- `GOVERNANCE.md` 记录决策权与稳定性策略； +- `SECURITY.md` 记录私密报告方式和支持的可信边界。 若这些文件不一致，以 Lean 声明和机器检查的审计输出为准；文档变更必须在同一个 PR 中恢复一致。 diff --git a/docs/zh-CN/CONTRIBUTING.md b/docs/zh-CN/CONTRIBUTING.md index 88a5c67..415734c 100644 --- a/docs/zh-CN/CONTRIBUTING.md +++ b/docs/zh-CN/CONTRIBUTING.md @@ -3,34 +3,53 @@ [English](../en/CONTRIBUTING.md) · [简体中文](CONTRIBUTING.md) · [日本語](../ja/CONTRIBUTING.md) · [Esperanto](../eo/CONTRIBUTING.md) -Ript 把证明可信度、显式依赖和可复现计算视为合并要求，而不仅是代码审查惯例。 +Ript 接受证明、模型、示例、文档和工具贡献。可信度、显式依赖、可复现性和准确公开声明都是合并要求。 -## 必须通过的质量门禁 +## 开始之前 -在仓库根目录运行： +阅读[项目范围](PROJECT_SCOPE.md)、[架构](ARCHITECTURE.md)与[研究状态](RESEARCH_STATUS.md)， +搜索 issue 和[猜想登记册](reference/CONJECTURES.md)。范围、公开定理陈述、架构、可信依赖、治理、 +安全或许可证变更应先讨论。安全问题按[安全策略](SECURITY.md)私密报告。 + +## 工作流 ```bash +git switch -c +lake exe cache get +lake build ./scripts/quality-gate.sh ``` -门禁会拒绝证明占位符、项目自定义公理、不安全声明、编译器信任逃逸、过宽的 `Mathlib` 导入、 -隐式 Lean 标识符、陈旧的根模块导入、声明 lint 失败、可执行行为变化、构建警告和未记录的定理 -假设，随后执行完整内核构建。 - -CI 以稳定的 `Lean quality gate` job 暴露同一组检查。只有该 job 通过，变更才可合并。 +分支和提交应保持聚焦。PR 必须说明结果、验证、公理足迹、兼容影响和剩余边界；合并要求 CI 全绿并 +获得维护者批准。 -## 证明与依赖策略 +## 证明与实现策略 -- 未证明研究陈述写入 `CONJECTURES.md`，不要声明为定理或公理； -- 导入尽可能窄的 Mathlib 模块； -- 每个实现模块保留 `set_option autoImplicit false`； -- 旗舰定理同时登记到 `Ript/Audit/AxiomChecks.lean` 和 `AXIOMS.md`； -- 若有意改变可执行行为，应在同一变更中更新 `scripts/check-examples.sh` 的示例断言。 +- 禁止证明占位符、项目公理、信任逃逸和 unsafe 声明； +- 保持 `autoImplicit false`，使用窄 Mathlib 导入； +- 通用缺失基础设施放在 `Ript/ForMathlib/`； +- 可执行数据保持在商和选择代表元的上游； +- 保持能力边界，使用领域准确的定理名称； +- 未完成陈述进入 `CONJECTURES.md`； +- 旗舰声明登记到 `Ript/Audit/AxiomChecks.lean` 与 `AXIOMS.md`； +- 只有有意且有证明支持时才更新可执行输出断言。 ## 文档策略 -- 每个逻辑页面必须以相同相对路径镜像到 `docs/en`、`docs/zh-CN`、`docs/ja` 和 `docs/eo`； -- 公开声明、命令、状态或可信边界改变时，同步更新四种语言； -- 根目录 `AXIOMS.md`、`BLUEPRINT.md`、`CONJECTURES.md` 和 `MODEL_MATRIX.md` - 保持为机器真源； -- 修改公理清单后，先运行 `./scripts/sync-doc-reference-tables.sh`，再运行质量门禁。 +所有维护页面按相同路径镜像到四种语言。命令、声明、状态或可信边界变化时同步相关语言。根目录蓝图、 +模型矩阵、公理与猜想记录是机器规范来源；公理表变化后运行 `./scripts/sync-doc-reference-tables.sh`。 + +## 必须通过的门禁 + +`./scripts/quality-gate.sh` 检查源代码/文档策略、根导入、完整内核构建、声明 lint、可执行示例和公理 +allowlist。不得为通过变更而削弱检查。 + +## PR 清单 + +- [ ] 目的单一，剩余边界明确； +- [ ] 锁定工具链下定向和完整构建通过； +- [ ] 旗舰假设与执行变化已经审计； +- [ ] 架构、状态、参考资料和相关语言均为最新； +- [ ] 不含无关、生成、秘密或私有文件。 + +审查同时评估定理陈述、建模意图与证明。决策规则见[治理](GOVERNANCE.md)。 diff --git a/docs/zh-CN/GETTING_STARTED.md b/docs/zh-CN/GETTING_STARTED.md index 4e6b2b5..639521f 100644 --- a/docs/zh-CN/GETTING_STARTED.md +++ b/docs/zh-CN/GETTING_STARTED.md @@ -174,3 +174,5 @@ import Ript.Models.FiniteStochastic - [架构](ARCHITECTURE.md)：模块与依赖边界； - [研究状态](RESEARCH_STATUS.md)：当前数学前沿； - [形式化蓝图](reference/BLUEPRINT.md)：定理级状态。 +- [贡献指南](CONTRIBUTING.md)：开发与审查流程； +- [治理](GOVERNANCE.md)和[安全](SECURITY.md)：项目策略。 diff --git a/docs/zh-CN/GOVERNANCE.md b/docs/zh-CN/GOVERNANCE.md new file mode 100644 index 0000000..06b10fc --- /dev/null +++ b/docs/zh-CN/GOVERNANCE.md @@ -0,0 +1,28 @@ +# 项目治理 + +[English](../en/GOVERNANCE.md) · [简体中文](GOVERNANCE.md) · +[日本語](../ja/GOVERNANCE.md) · [Esperanto](../eo/GOVERNANCE.md) + +Ript 是维护者主导的形式化研究项目。决策优先考虑数学准确性、内核可核验证据、明确边界和可复现性。 + +## 角色 + +- 维护者负责范围、仓库管理、发行、安全协调与最终合并； +- 贡献者提出聚焦且可审查的证明、模型、文档或工具变更； +- 审查者核对定理陈述、Lean 实现、依赖、审计、执行证据和公开声明。 + +## 权威顺序与决策 + +冲突按以下顺序解决：锁定工具链下的 Lean 内核结果；定理类型与公理输出；goal、蓝图、模型、 +公理和猜想规范记录；最后才是解释性文档。CI 必须通过，但不能代替数学审查。 + +范围或架构变更应先讨论；PR 应聚焦，运行完整门禁，同步所有受影响语言和审计，并把未完成工作 +保留在猜想登记册中。 + +## 稳定性与社区 + +项目没有稳定发行或 API 保证，请固定 commit SHA。交流应精确、建设性且尊重他人；不接受骚扰、 +歧视、开盒、凭据暴露或故意歪曲证明状态。 + +当前没有开源许可证；许可证选择必须由维护者通过专门变更明确决定。规范原文见根目录 +[治理文档](../../GOVERNANCE.md)和[安全策略](SECURITY.md)。 diff --git a/docs/zh-CN/PROJECT_SCOPE.md b/docs/zh-CN/PROJECT_SCOPE.md index 9f5dfad..c63942e 100644 --- a/docs/zh-CN/PROJECT_SCOPE.md +++ b/docs/zh-CN/PROJECT_SCOPE.md @@ -35,6 +35,11 @@ Ript 是形式研究库，不是运行时估算器，也不是已经完成的物 的单子 2-胞腔、异质水平复合、交换律以及五边形/三角形协调。 [模型能力矩阵](reference/MODEL_MATRIX.md)只记录已经实现并编译的操作。 +当前最高局部化层已经为每个 local mapping category 给出完整 generated-hammock 呈示、到实际局部化 +目标的直接范畴 nerve 等价、显式单纯同伦逆，以及终止且保持语义的 administrative reduction。 +这是经审计的项目内 Dwyer--Kan core；它还不是与经典 reduced 任意网格 hammock 的比较，也不是 +标准全局 Rezk 弱等价定理。 + ## 信任模型 Ript 禁止： @@ -68,8 +73,10 @@ Ript 是早期研究软件： ## 权威记录 -- [研究状态](RESEARCH_STATUS.md)：简明的已证明/开放边界； +- [研究状态](RESEARCH_STATUS.md)：当前叙述性已证明/开放边界； - [形式化蓝图](reference/BLUEPRINT.md)：定理类型与依赖台账； - [公理清单](reference/AXIOMS.md)：已审计内核假设； - [猜想登记册](reference/CONJECTURES.md)：开放研究陈述； - [贡献指南](CONTRIBUTING.md)：证明与合并策略。 +- [项目治理](GOVERNANCE.md)：决策权和稳定性； +- [安全策略](SECURITY.md)：报告方式和支持的可信边界。 diff --git a/docs/zh-CN/README.md b/docs/zh-CN/README.md index bfb590b..bb11e5b 100644 --- a/docs/zh-CN/README.md +++ b/docs/zh-CN/README.md @@ -1,53 +1,45 @@ -# Ript - -**面向资源索引过程理论、由内核核验的 Lean 4 基础库。** +# Ript 文档 [English](../en/README.md) · [简体中文](README.md) · [日本語](../ja/README.md) · [Esperanto](../eo/README.md) -[![Quality Gate](https://github.com/miuchan/ript/actions/workflows/ci.yml/badge.svg)](https://github.com/miuchan/ript/actions/workflows/ci.yml) -![Lean 4.33.0](https://img.shields.io/badge/Lean-4.33.0-0d6efd) -![mathlib 4.33.0](https://img.shields.io/badge/mathlib-4.33.0-a42e2b) -![研究状态](https://img.shields.io/badge/status-early--stage%20research-orange) +Ript 是面向资源索引信息过程的 Lean 4 内核核验研究库。它连接可执行有限语法与概率、量子、 +因果、计算、语义信息、决策和热力学模型，同时保持各种可选能力彼此分离。 -Ript 形式化行为与资源消耗均可组合的带类型过程，并把可执行有限模型连接到资源界、 -可靠性、完备性和保结构语义的内核核验结果。 -首个字面共享的六模型切片，已经把同一个布尔过程签名解释到概率、量子、因果、计算、语义和热模型。 +> [!IMPORTANT] +> 仓库已经包含大量真实证明，但仍是早期研究项目；最终全局定理与稳定 API 尚未完成。 -Ript 的核心研究目标是：构造一种可计算、机器可验证、单值化、高阶范畴化的资源受限 -信息过程理论，使经典概率、量子过程、因果模型、计算、语义信息和热力学成为它的不同 -模型，并证明连接这些模型的表示定理与完备性定理。本仓库包含通向该目标的已编译层； -整体目标目前还不是一个已经证明的定理。 +## 当前快照 -> [!IMPORTANT] -> Ript 是早期研究软件。已编译结果由 Lean 内核核验；公共 API 与研究前沿仍在演进。 +- 资源敏感语法、预算、可靠性、相对完备性与自由语义均已编译； +- 六类模型均有具体实例和经检查的非平凡示例； +- 模型及资源变换态射组成经验证的双范畴层； +- 内部单值与 complete-Segal 基础位于可执行核心下游； +- generated hammock mapping spaces 已与实际局部化目标等价，并具有显式 nerve 同伦逆和终止约化。 -## 快速开始 +当前前沿是 critical-pair joinability、经典 reduced-hammock 不变性、标准弱等价封装与全局 Rezk 定理。 -安装 [elan](https://github.com/leanprover/elan) 后构建锁定版本的 Lean 与 Mathlib 项目： +## 从这里开始 ```bash git clone https://github.com/miuchan/ript.git cd ript lake exe cache get -lake build +./scripts/quality-gate.sh ``` -环境要求、可执行示例、依赖接入、可复现使用和故障排查见[入门指南](GETTING_STARTED.md)。 - -## 按需阅读 +后续步骤见[入门指南](GETTING_STARTED.md)。 -- **已经实现了什么？** 查看[模型能力矩阵](reference/MODEL_MATRIX.md)； -- **哪些已经证明，哪些仍然开放？** 查看[研究状态](RESEARCH_STATUS.md)； -- **代码如何组织？** 阅读[架构指南](ARCHITECTURE.md)； -- **可信边界和成熟度如何？** 阅读[项目范围与可信边界](PROJECT_SCOPE.md)； -- **精确研究记录在哪里？** 查阅[形式化蓝图](reference/BLUEPRINT.md)、 - [公理清单](reference/AXIOMS.md)和[猜想登记册](reference/CONJECTURES.md)。 +## 按任务阅读 -## 参与贡献 +- **理解项目：** [范围与可信边界](PROJECT_SCOPE.md) · [架构](ARCHITECTURE.md) +- **查看已证明内容：** [研究状态](RESEARCH_STATUS.md) · [模型能力矩阵](reference/MODEL_MATRIX.md) +- **审计精确证据：** [蓝图](reference/BLUEPRINT.md) · [公理](reference/AXIOMS.md) · + [猜想](reference/CONJECTURES.md) +- **参与项目：** [贡献指南](CONTRIBUTING.md) · [治理](GOVERNANCE.md) · [安全](SECURITY.md) +- **切换语言：** [多语言文档中心](../README.md) -请先阅读[贡献指南](CONTRIBUTING.md)，并在提交 PR 前运行 -`./scripts/quality-gate.sh`。 +## 成熟度与复用 -Ript 基于 [Lean 4](https://lean-lang.org/) 与 -[Mathlib](https://github.com/leanprover-community/mathlib4) 构建。 +可复现研究应固定完整 commit SHA。项目没有稳定发行或 API 兼容承诺。当前尚未选择开源许可证， +公开可见不等于获得复制、修改或再分发权；详见[项目范围](PROJECT_SCOPE.md#许可)。 diff --git a/docs/zh-CN/RESEARCH_STATUS.md b/docs/zh-CN/RESEARCH_STATUS.md index f403778..3fd55e6 100644 --- a/docs/zh-CN/RESEARCH_STATUS.md +++ b/docs/zh-CN/RESEARCH_STATUS.md @@ -3,9 +3,21 @@ [English](../en/RESEARCH_STATUS.md) · [简体中文](RESEARCH_STATUS.md) · [日本語](../ja/RESEARCH_STATUS.md) · [Esperanto](../eo/RESEARCH_STATUS.md) -本页是简明研究地图，不是定理台账。精确定理类型、依赖、源文件与假设见 +本页是持续维护的叙述性研究地图，不是定理台账。精确定理类型、依赖、源文件与假设见 [形式化蓝图](reference/BLUEPRINT.md)和[公理清单](reference/AXIOMS.md)。 +## 当前快照 + +**已验证：** 可执行资源敏感语法与预算；可靠性、相对完备性和自由语义；六类具体模型切片；固定与 +变资源模型双范畴；内部单值与 complete-Segal 基础；到实际目标 nerve 直接等价的完整 generated- +hammock mapping category；以及具有不可约 reduct 的终止、语义保持 administrative reduction。 + +**仍开放：** raw critical-pair joinability 与局部合流、其余经典任意网格 hammock moves、reduced- +hammock 同伦不变性、标准 derived 弱等价接口和最终全局 Dwyer--Kan/Rezk 定理。总研究目标仍然有效。 + +能力问题查[模型矩阵](reference/MODEL_MATRIX.md)，定理证据查[蓝图](reference/BLUEPRINT.md)，未证方向查 +[猜想登记册](reference/CONJECTURES.md)。 + ## 状态词汇 蓝图只使用以下正式状态： diff --git a/docs/zh-CN/SECURITY.md b/docs/zh-CN/SECURITY.md new file mode 100644 index 0000000..bef7836 --- /dev/null +++ b/docs/zh-CN/SECURITY.md @@ -0,0 +1,28 @@ +# 安全策略 + +[English](../en/SECURITY.md) · [简体中文](SECURITY.md) · +[日本語](../ja/SECURITY.md) · [Esperanto](../eo/SECURITY.md) + +Ript 是形式化研究库，不是托管服务。安全范围包括证明可信边界、可执行示例、依赖与 CI 完整性， +以及可能影响使用者的不安全行为。 + +## 支持范围 + +仅支持当前 `main`。报告必须注明完整 commit SHA 与锁定的 Lean 工具链；目前没有版本回溯策略。 + +## 私密报告 + +优先使用 GitHub **Security** 页面的私密漏洞报告。如果该入口不可用，只公开提交“请求私密联系渠道” +的最小 issue，不要公开利用细节、凭据或私有数据。 + +请包含受影响模块与提交、影响、现实威胁场景、最小复现、受影响可信边界和已知缓解措施。 + +## 哪些属于安全问题 + +证明信任逃逸、隐藏公理、unsafe 声明、门禁绕过、可达的依赖/CI 入侵、可执行边界违反、秘密或 +私有数据泄露属于安全问题。已登记猜想、建模争议或不稳定 API 通常属于研究或缺陷问题。 + +## 响应与披露 + +维护者尽力处理，但早期研究软件没有 SLA。修复必须通过正常内核、审计和 CI 门禁；在修复或缓解 +方案可用前请协调公开披露。规范原文见根目录[安全策略](../../SECURITY.md)。 diff --git a/scripts/check-doc-locales.sh b/scripts/check-doc-locales.sh index 4b9ba75..3c15ff9 100755 --- a/scripts/check-doc-locales.sh +++ b/scripts/check-doc-locales.sh @@ -13,6 +13,8 @@ documents=( PROJECT_SCOPE.md RESEARCH_STATUS.md CONTRIBUTING.md + GOVERNANCE.md + SECURITY.md reference/MODEL_MATRIX.md reference/BLUEPRINT.md reference/AXIOMS.md @@ -25,6 +27,14 @@ canonical_tail="$(mktemp)" english_tail="$(mktemp)" trap 'rm -f "$canonical_tail" "$english_tail"' EXIT +for root_document in README.md CONTRIBUTING.md GOVERNANCE.md SECURITY.md \ + RESEARCH_GOAL.md BLUEPRINT.md MODEL_MATRIX.md AXIOMS.md CONJECTURES.md; do + if [[ ! -f "$root_document" ]]; then + printf 'Missing canonical project document: %s\n' "$root_document" >&2 + failed=1 + fi +done + for document in "${documents[@]}"; do for locale in "${locales[@]}"; do path="docs/$locale/$document" @@ -51,6 +61,8 @@ legacy_paths=( docs/ARCHITECTURE.md docs/PROJECT_SCOPE.md docs/RESEARCH_STATUS.md + docs/GOVERNANCE.md + docs/SECURITY.md ) for legacy_path in "${legacy_paths[@]}"; do