Ript

Kernel-checked foundations for resource-indexed information processes.

English · 简体中文 · 日本語 · Esperanto

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. Kernel-checked declarations are real proofs, but the public API and the global research theorem are not complete.

Verified today

• 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.

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.

Quick start

git clone https://github.com/miuchan/ript.git
cd ript
lake exe cache get
./scripts/quality-gate.sh

The repository pins Lean and Mathlib. Follow Getting started for prerequisites, focused commands, examples, dependency use, and troubleshooting.

Documentation

• Learn the system: Project scope · Architecture
• Inspect current evidence: Research status · Model matrix
• Audit exact claims: Blueprint · Axioms · Conjectures
• Work on Ript: Contributing · Governance · Security
• Choose another language: Documentation hub

Reuse and citation

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 for the exact boundary.