docs(spec): 重写 spec/ 与根 README 的语言与取舍

按新文风(简洁书面中文)重写 spec/ 全部 Lean doc 注释、spec/README,
并顺根 README。核心:讲清产品逻辑、去伪术语、去 ADR 黑话、DRY。

语言:砍钉死/留痕/实现侧/将就/脑补/刻意等伪术语;短句;不复述文件系统
能看到的东西;typst 考据移出 spec 指向 ADR。

内容取舍(动结构):
- System 层大改:删 can_mono 形式化定理、Capability 9 项枚举与
  requiredRole 映射、RunState 6 构造子;Audit.lean 删除并入 System 顶部。
  Hub 未建的部分一律 prose 占位,只留 Lock 的 owner=run 与 WellFormed。
- 澄清两个"检查":产品 checker(LLM 判不了合法性,checker 真跑工具补这块)
  vs 开发时 spec↔impl 一致性检查(无自动闸门)。Oracle 重新定位为
  "checker 得委托外部工具才能判的事实",不是"Lean 没写形式化"。
- spec/README 补取舍判据 checklist(自顶向下逐步细化、不在 Lean 里验证实现)。
- 根 README 去 DRY:删硬编码版本号、cache 路径细节;宪法第 3 条吸收
  "人/coding assistant 核对"修正;第 5 条与 spec/README 判据去重。

保留:Export/Render 执行语义、Info 的 raw→canonical 设计模式(产品语义,
只顺文风不砍结构);renderIgnoredSeverity(实现对齐依赖)。

lake build 通过(24 jobs)。

Co-Authored-By: Claude <noreply@anthropic.com>

Cargo.lock

@@ -294,6 +294,15 @@ dependencies = [
  "strsim",
 ]
 
+[[package]]
+name = "clap_complete"
+version = "4.6.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e0a7a9bfdb35811f9e59832f0f05975114d2251b415fb534108e6f34060fd772"
+dependencies = [
+ "clap",
+]
+
 [[package]]
 name = "clap_derive"
 version = "4.6.1"
@@ -386,7 +395,7 @@ dependencies = [
 
 [[package]]
 name = "cph-check"
-version = "0.0.1"
+version = "0.0.2"
 dependencies = [
  "cph-diag",
  "cph-model",
@@ -396,9 +405,10 @@ dependencies = [
 
 [[package]]
 name = "cph-cli"
-version = "0.0.1"
+version = "0.0.2"
 dependencies = [
  "clap",
+ "clap_complete",
  "cph-check",
  "cph-diag",
  "cph-typst",
@@ -406,14 +416,14 @@ dependencies = [
 
 [[package]]
 name = "cph-diag"
-version = "0.0.1"
+version = "0.0.2"
 dependencies = [
  "serde",
 ]
 
 [[package]]
 name = "cph-model"
-version = "0.0.1"
+version = "0.0.2"
 dependencies = [
  "cph-diag",
  "serde",
@@ -422,7 +432,7 @@ dependencies = [
 
 [[package]]
 name = "cph-schema"
-version = "0.0.1"
+version = "0.0.2"
 dependencies = [
  "cph-diag",
  "cph-model",
@@ -432,7 +442,7 @@ dependencies = [
 
 [[package]]
 name = "cph-typst"
-version = "0.0.1"
+version = "0.0.2"
 dependencies = [
  "cph-diag",
  "cph-model",

Cargo.toml

@@ -12,7 +12,7 @@ members = [
 # Shared metadata for all workspace crates. Individual crates inherit these via
 # `version.workspace = true` / `edition.workspace = true`.
 [workspace.package]
-version = "0.0.1"
+version = "0.0.2"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 

README.md

@@ -1,66 +1,74 @@
 # curriculum-project-hub
 
-教研生产的数字化解决方案。核心思路:课程像 DAW / 剪辑软件那样有一个**结构化的工程文件**;coding agent 协助编辑它;一个 rule-based checker(类编译器)校验其合法性并给出 helpful fix hint。目标是把教研从一次性的文档,沉淀成**可累积、可校验、可复用的资产**。
+教研生产的数字化解决方案。核心思路:课程像 DAW / 剪辑软件那样有一个结构化的工程文件;
+LLM assistant 协助编辑它;一个 rule-based checker 校验其合法性并给出有用的诊断。
 
-这是一个 **monorepo**。它的组织方式本身就表达了一条原则:**`spec/` 是上游的语义母本,其余部件是向它对齐的实现。**
+LLM 提效,但判不了一节课合不合法(它不能真去跑 typst、不能可靠地断言数据合不合
+schema);checker 真跑工具、给确定性诊断,补上这块。两者一起才是完整闭环。目标是把教研
+从一次性的文档,变成可累积、可校验、可复用的资产。
 
-## 安装 `cph` 命令行
+这是一个 monorepo。组织方式本身就表达了一条原则:`spec/` 是上游的语义母本,其余部件是
+向它对齐的实现。
 
-当前版本 **0.0.1**。从源码安装(本仓库根目录):
+## 安装 `cph`
+
+从源码安装(本仓库根目录):
 
 ```sh
 cargo install --path crates/cph-cli --locked
 ```
 
-`render` 包已嵌入二进制(build.rs 编译期拷入 + `include_dir!`),所以装好后**无需任何环境变量、不依赖源码树**即可用。渲染包按版本解压到 per-user cache(`~/.cache/cph/render-<version>/` 或 macOS `~/Library/Caches/cph/...`);开发时可设 `CPH_RENDER_DIR` 指向 live `render/` 目录覆盖。
+`render` 包已嵌入二进制,装好后无需任何环境变量、不依赖源码树即可用。开发时可设
+`CPH_RENDER_DIR` 指向 live `render/` 目录覆盖。
 
 ```sh
-cph --version          # cph 0.0.1
-cph check <工程目录>     # 校验合法性(6 类诊断)
+cph check <工程目录>                              # 校验合法性
 cph build <工程目录> --target student -o build/student.pdf   # 渲讲义 PDF
+cph completions zsh > ~/.zfunc/_cph               # shell 补全(可选)
 ```
 
+工程文件根放一个 `.cph-version` 文件,声明它面向的 cph 版本;`cph` 加载时比对自身版本,
+不相容则拒绝(版本契约,ADR-0016)。
+
 ## 仓库布局
 
-```
-README.md          ← 本文件:总览 + 宪法(下面 5 条)
-CLAUDE.md          ← 全局 agent 操作手册(管整个 repo)
-docs/adr/          ← 系统级架构决策记录(跨部件,被 spec 契约引用)
-spec/              ← Lean 语义母本(自包含的 Lean 工程)。见 spec/README.md
-Cargo.toml         ← 仓库级 cargo workspace(实现部件共用,便于跨部件复用 crate)
-crates/            ← 实现:rule-based checker(向 spec 对齐)。见 crates/README.md
-  cph-diag / cph-model / cph-schema / cph-typst   ← 可复用基础(模型/校验/typst 引擎)
-  cph-check / cph-cli                             ← checker 本体 + `cph` 命令行
-render/            ← typst 渲染包 cph-render(母本的渲染后端之一,ADR-0005)
-examples/          ← 样例工程文件(如 TH-141),流水线的真实输入
-(hub/ exporter/ …) ← 将来的其他部件,平级于 spec/。尚未创建
-```
+`spec/` 是 Lean 语义母本(自包含 Lean 工程,见 `spec/README.md`);`crates/` 是实现
+(rule-based checker,向 spec 对齐,见 `crates/README.md`);`render/` 是 typst 渲染包;
+`examples/` 是样例工程文件;`docs/adr/` 是架构决策记录,被 spec 引用。
 
-`spec/` 与实现部件**物理分离、平级共存**:谁是上游、谁向谁对齐,一眼可见。
-实现部件共用一个仓库根的 cargo workspace,使基础 crate(模型、typst 引擎)能被
-未来部件(如 exporter)复用,而非各自重造。
+`spec/` 与实现部件物理分离、平级共存:谁是上游、谁向谁对齐,一眼可见。实现部件共用一个
+仓库根的 cargo workspace,使基础 crate 能被未来部件复用。
 
 ## 宪法
 
 这 5 条是 `spec/` 这份语义母本的定位与约束,是本仓库一切工作的前提。
 
 1. **角色——Lean 是研发侧的上游参照。**
-   `spec/` 用 Lean 编写,是开发者(领域专家)与 coding agent **共用**的 spec 工具,用来沉淀产品各部件的**语义**。它**不进入产品运行时**——产品里"站在 Lean 这个位置"的那个 checker 用什么技术实现,尚未决定;但那个东西的语义,先在 `spec/` 里固定下来。
+   `spec/` 用 Lean 写,是开发者和 coding assistant 共用的 spec 工具,用来沉淀产品各部件
+   的语义。它不进产品运行时——运行时那个 checker 用什么技术实现还没定,但它的语义先在
+   `spec/` 里固定下来。
 
 2. **对齐机制——Lean 只做上游参照。**
-   不做 extract / codegen,不派生 conformance test,CI 里**没有** spec→实现的 gate。实现对齐 spec,由"开发者 review + agent 巡逻 diff"这个人肉环节承载。
-   (CI 里的 `spec check` 只验 spec **自身**能否 type-check,即契约内部良构,不是 spec↔实现的对齐检查。)
+   不做 extract / codegen,不派生 conformance test,CI 里没有 spec→实现的 gate。实现对齐
+   spec,靠开发者 review 和 agent 巡逻 diff 这个人肉环节承载。(CI 里的 spec check 只验
+   spec 自身能否 type-check,即契约内部良构,不是 spec↔实现对齐检查。)
 
-3. **资产性 —— 由 review 纪律承载,无机器兜底。**
-   这份仓库给你的是"精确、自洽、机器验内部良构的语义共识",**不是**"实现正确性保证"。spec 与实现之间那道缝,是我们自愿用人来守的——清醒地守,它就是资产;放任实现漂移而不回头同步,它就退化成最贵的过期文档。
+3. **资产性——由核对纪律承载,无机器兜底。**
+   这份仓库给的是精确、自洽、机器验过内部良构的语义共识,不是实现正确性的保证。spec 与
+   实现是否一致,没有自动闸门,要靠人工或 coding assistant 不定期(或每次改动后)核对;
+   坚持核对,它就是有用的参照,否则只会变成过期的文档。
 
 4. **形态——它是人机共识的契约。**
-   契约必须**自包含**:凡契约未明文规定的,开发者与 agent 双方都不该假设。这比"文档"严格——type checker 会逼这份契约在结构上无洞。
+   契约必须自包含:凡契约未明文规定的,开发者与 agent 双方都不该假设。这比"文档"严格——
+   type checker 会逼这份契约在结构上无洞。
 
 5. **深度判据——只收录分歧点。**
-   一条语义该不该写进 Lean,取决于一句话:**"不写明,开发者与 agent 会不会各自做出不同假设?"** 会 → 进契约;显然的东西 / 纯 plumbing / 普通 CRUD 字段 → 不进(写进去只稀释信噪比、增加维护面)。
-   深度上限不是 Lean 的表达力,而是**你愿意在每次实现变更时手动回头同步的量**——写得比你能维护的更深,多出来的部分会率先过期、反过来误导实现。
+   一条语义该不该写进 Lean,取决于一句话:不写明,开发者与 agent 会不会各自做出不同
+   假设?会,就进契约;显然的东西、纯基础设施、普通 CRUD 字段,不进(写进去只稀释信噪比、
+   增加维护面)。深度上限不是 Lean 的表达力,而是你愿意在每次实现变更时手动回头同步的量。
+   进了之后钉到多细,见 `spec/README.md` 的取舍判据。
 
 ## CI
 
-`.gitea/workflows/spec-check.yml` 在每次 push / PR 时于 `spec/` 下跑 `lake build`,确保契约始终 type-check 通过(从第一天起就是"绿"的)。这是良构 gate,见宪法第 2 条。
+每次 push / PR 在 `spec/` 下跑 `lake build`,确保契约始终 type-check 通过。这是良构 gate,
+见宪法第 2 条。

crates/cph-cli/Cargo.toml

@@ -13,3 +13,4 @@ cph-check = { path = "../cph-check" }
 cph-diag = { workspace = true }
 cph-typst = { path = "../cph-typst" }
 clap = { version = "4", features = ["derive"] }
+clap_complete = "4"

crates/cph-cli/src/main.rs

@@ -46,6 +46,22 @@ enum Command {
         #[arg(short = 'o', long, value_name = "OUT")]
         out: Option<PathBuf>,
     },
+    /// Print a shell-completion script to stdout (clap_complete; ADR-0013 opt-in
+    /// sibling: a local convenience, no lesson involved). Pipe to your shell's
+    /// completion file, e.g. `cph completions zsh > ~/.zfunc/_cph`.
+    Completions {
+        /// Which shell to generate completions for.
+        shell: Shell,
+    },
+}
+
+#[derive(Debug, Clone, Copy, clap::ValueEnum)]
+enum Shell {
+    Bash,
+    Zsh,
+    Fish,
+    PowerShell,
+    Elvish,
 }
 
 fn main() -> ExitCode {
@@ -59,9 +75,29 @@ fn main() -> ExitCode {
     match cli.command {
         Command::Check { path } => run_check(&path, &engine),
         Command::Build { path, target, out } => run_build(&path, &engine, &target, out),
+        Command::Completions { shell } => run_completions(shell),
     }
 }
 
+/// Emit a shell-completion script for `shell` to stdout. The script is built
+/// from the same `Cli` clap definition above, so it tracks subcommands/flags as
+/// they evolve.
+fn run_completions(shell: Shell) -> ExitCode {
+    use clap::CommandFactory;
+    use clap_complete::Shell as CompShell;
+
+    let sh = match shell {
+        Shell::Bash => CompShell::Bash,
+        Shell::Zsh => CompShell::Zsh,
+        Shell::Fish => CompShell::Fish,
+        Shell::PowerShell => CompShell::PowerShell,
+        Shell::Elvish => CompShell::Elvish,
+    };
+    let mut cmd = Cli::command();
+    clap_complete::generate(sh, &mut cmd, "cph", &mut std::io::stdout());
+    ExitCode::SUCCESS
+}
+
 /// Print every diagnostic in `report` to stderr, followed by a summary line.
 fn print_diagnostics(report: &CheckReport) {
     for d in &report.diagnostics {

crates/cph-diag/src/lib.rs

@@ -88,6 +88,9 @@ pub enum DiagCode {
     TypstCompile,
     /// An element is ignored under a render target (ADR-0005: warning).
     RenderIgnored,
+    /// The engineering file's `.cph-version` is not compatible with the running
+    /// CLI's version (ADR-0016). Decided at load time; `error` severity.
+    CphVersionMismatch,
 }
 
 impl DiagCode {
@@ -103,6 +106,7 @@ impl DiagCode {
             DiagCode::SchemaViolation => "E-SCHEMA",
             DiagCode::TypstCompile => "E-TYPST-COMPILE",
             DiagCode::RenderIgnored => "W-RENDER-IGNORED",
+            DiagCode::CphVersionMismatch => "E-CPH-VERSION",
         }
     }
 }

crates/cph-model/src/lib.rs

@@ -391,6 +391,14 @@ pub fn load(root: &Path) -> (Option<Lesson>, Vec<Diagnostic>) {
         }
     };
 
+    // `.cph-version` compatibility (ADR-0016). Decided at load time, before
+    // any structural/schema/compile work. An incompatible version is an
+    // error diagnostic (`CphVersionMismatch`); it does not halt loading, so
+    // any other defects surface alongside it — but an error diagnostic alone
+    // already makes the lesson illegal (ADR-0010), so `check`/`build` refuse.
+    // A missing `.cph-version` is skipped for now (ADR-0016 OPEN).
+    check_cph_version(root, &mut diags);
+
     // [project] and [info] are required to build a Lesson at all.
     let project = match raw.project {
         Some(p) => Project {
@@ -506,6 +514,58 @@ pub fn load(root: &Path) -> (Option<Lesson>, Vec<Diagnostic>) {
     (Some(lesson), diags)
 }
 
+/// The cph version the running CLI was built with (ADR-0016). Pulled from the
+/// crate's `CARGO_PKG_VERSION` at compile time.
+pub const CPH_VERSION: &str = env!("CARGO_PKG_VERSION");
+
+/// Read the engineering file's `.cph-version` and, if present, push a
+/// `CphVersionMismatch` error when it is not compatible with [`CPH_VERSION`]
+/// (ADR-0016). A missing file is skipped for now (migration period; OPEN in
+/// ADR-0016).
+fn check_cph_version(root: &Path, diags: &mut Vec<Diagnostic>) {
+    let path = root.join(".cph-version");
+    let Ok(src) = std::fs::read_to_string(&path) else {
+        return; // missing `.cph-version` — skipped (ADR-0016 OPEN).
+    };
+    let file_version = src.trim();
+    if file_version.is_empty() {
+        diags.push(
+            Diagnostic::error(
+                DiagCode::CphVersionMismatch,
+                format!(".cph-version is empty; expected cph version {CPH_VERSION}"),
+            )
+            .with_hint(format!(
+                "write the cph version this file targets into {} (currently {CPH_VERSION})",
+                path.display()
+            )),
+        );
+        return;
+    }
+    if !versions_compatible(file_version, CPH_VERSION) {
+        diags.push(
+            Diagnostic::error(
+                DiagCode::CphVersionMismatch,
+                format!(
+                    ".cph-version declares {file_version}, but this cph is {CPH_VERSION} (incompatible)"
+                ),
+            )
+            .with_hint(format!(
+                "align them: set .cph-version to {CPH_VERSION}, or install cph {file_version}"
+            )),
+        );
+    }
+}
+
+/// Whether an engineering file's declared cph version is compatible with the
+/// running CLI's version (ADR-0016). **The rule is exact equality** — the
+/// strictest choice, deliberately, while the format is young (0.0.x). This is
+/// the single seam for future relaxation to a semver range: relaxing the
+/// format does not change the diagnostic class, the spec, or the CLI — only
+/// this predicate.
+fn versions_compatible(file_version: &str, cli_version: &str) -> bool {
+    file_version == cli_version
+}
+
 /// Load one element's `element.toml` into an [`ElementDescriptor`], collecting
 /// diagnostics. On a missing/malformed `element.toml` the descriptor falls back
 /// to the part's declared kind with empty scalars so the lesson stays buildable.

crates/cph-model/tests/fixtures/valid/.cph-version

@@ -0,0 +1 @@
+0.0.2

crates/cph-model/tests/load.rs

@@ -272,3 +272,90 @@ fn malformed_target_config_is_non_fatal_with_schema_violations() {
         "a diagnostic should name the bad step type, got: {diags:?}"
     );
 }
+
+// --- `.cph-version` compatibility gate (ADR-0016) ------------------------------
+
+/// The cph version the running CLI was built with — what `.cph-version` must
+/// match exactly (ADR-0016's MVP rule).
+const CPH_VERSION: &str = env!("CARGO_PKG_VERSION");
+
+/// Write a one-part lesson into a temp dir, optionally with a `.cph-version`
+/// file. Returns the temp dir so the caller runs `load`.
+fn tmp_lesson_with_version(version: Option<&str>) -> PathBuf {
+    let mut p = std::env::temp_dir();
+    let nanos = std::time::SystemTime::now()
+        .duration_since(std::time::UNIX_EPOCH)
+        .unwrap()
+        .as_nanos();
+    p.push(format!("cph-version-test-{nanos}"));
+    std::fs::create_dir_all(&p).unwrap();
+    std::fs::write(
+        p.join("manifest.toml"),
+        "[project]\nid = \"v\"\nname = \"v\"\n[info]\ntitle = \"v\"\n[[parts]]\nkind = \"segment\"\npath = \"segments/a\"\n",
+    )
+    .unwrap();
+    let seg = p.join("segments").join("a");
+    std::fs::create_dir_all(&seg).unwrap();
+    std::fs::write(seg.join("element.toml"), "kind = \"segment\"\n").unwrap();
+    std::fs::write(seg.join("textbook.typ"), "t.\n").unwrap();
+    if let Some(v) = version {
+        std::fs::write(p.join(".cph-version"), v).unwrap();
+    }
+    p
+}
+
+#[test]
+fn cph_version_matching_is_not_a_diagnostic() {
+    let tmp = tmp_lesson_with_version(Some(CPH_VERSION));
+    let (_lesson, diags) = load(&tmp);
+    let _ = std::fs::remove_dir_all(&tmp);
+    assert!(
+        diags.iter().all(|d| d.code != DiagCode::CphVersionMismatch),
+        "a matching .cph-version must not warn, got {diags:?}"
+    );
+}
+
+#[test]
+fn cph_version_mismatch_is_an_error_diagnostic() {
+    let tmp = tmp_lesson_with_version(Some("99.99.99"));
+    let (lesson, diags) = load(&tmp);
+    let _ = std::fs::remove_dir_all(&tmp);
+    // The lesson still loads (so other defects could surface), but the
+    // mismatch is an error diagnostic — which alone makes it illegal.
+    assert!(lesson.is_some(), "a mismatch should not halt loading");
+    let mm: Vec<_> = diags
+        .iter()
+        .filter(|d| d.code == DiagCode::CphVersionMismatch)
+        .collect();
+    assert_eq!(mm.len(), 1, "expected one CphVersionMismatch, got {diags:?}");
+    assert!(
+        mm[0].message.contains("99.99.99") && mm[0].message.contains(CPH_VERSION),
+        "diagnostic should name both versions, got: {}",
+        mm[0].message
+    );
+}
+
+#[test]
+fn cph_version_missing_is_skipped() {
+    // No `.cph-version` file at all → skipped (ADR-0016 migration period; OPEN).
+    let tmp = tmp_lesson_with_version(None);
+    let (_lesson, diags) = load(&tmp);
+    let _ = std::fs::remove_dir_all(&tmp);
+    assert!(
+        diags.iter().all(|d| d.code != DiagCode::CphVersionMismatch),
+        "a missing .cph-version must be skipped, got {diags:?}"
+    );
+}
+
+#[test]
+fn cph_version_empty_is_an_error() {
+    let tmp = tmp_lesson_with_version(Some("   \n"));
+    let (_lesson, diags) = load(&tmp);
+    let _ = std::fs::remove_dir_all(&tmp);
+    assert!(
+        diags
+            .iter()
+            .any(|d| d.code == DiagCode::CphVersionMismatch && d.message.contains("empty")),
+        "an empty .cph-version should be an error, got {diags:?}"
+    );
+}

crates/cph-typst/tests/fixtures/mini/.cph-version

@@ -0,0 +1 @@
+0.0.2

docs/adr/0016-cph-version-contract-file.md

@@ -0,0 +1,105 @@
+# ADR 0016: The `.cph-version` Contract File
+
+## Status
+
+Accepted — and implemented. The cph CLI refuses to process an engineering
+file whose `.cph-version` is not compatible with the running CLI, surfacing
+this as a 7th diagnostic class `cphVersionMismatch`.
+
+Builds on **ADR-0005** (the engineering file is the asset; its structure is
+declared), **ADR-0008** (the engineering file is a directory tree rooted at
+`manifest.toml`), and **ADR-0010/0012** (the diagnostic taxonomy and the
+"legal lesson = no error diagnostics" rule).
+
+## Context
+
+As the cph tool and the authored curriculum engineering files evolve
+independently, a file authored against one version of the format may not be
+processable by a CLI built against another. Without a version contract, a
+mismatch surfaces as confusing downstream failures (a malformed-manifest
+diagnostic, a compile error, or a silently-wrong build) rather than as the
+real cause: "this file expects a different cph than the one you're running."
+
+The user's framing: the curriculum engineering-file workspace should carry a
+`.cph-version` file naming the cph version it targets; the CLI should
+**fail early** when that version is not compatible with itself. The
+compatibility rule can be refined over time, but for now it is the strictest
+possible: **exact version equality**.
+
+## Decision
+
+### A `.cph-version` file at the engineering-file root
+
+An engineering file's root (alongside `manifest.toml`) carries a
+`.cph-version` file whose entire content is the version string the file
+targets (e.g. `0.0.2`, no trailing newline required, whitespace trimmed).
+The CLI reads its own version from `CARGO_PKG_VERSION`.
+
+### Compatibility is decided at `load` time and is a diagnostic
+
+The version check runs in the `load` phase (`cph-model::load`), before any
+structural/schema/compile work. An incompatible version produces a
+`cphVersionMismatch` **error** diagnostic — not a CLI-level early exit
+without a diagnostic. This keeps the failure inside the checker's normal
+diagnostic vocabulary: `cph check` reports it and exits 1 (which *is* an
+early refusal — load-phase errors halt the pipeline), and `cph build`
+refuses to run. Because it is an error diagnostic, an incompatible-version
+file is, by the contract, **not a legal lesson** (ADR-0010's "legal = no
+error diagnostics").
+
+The diagnostic carries a hint pointing the user at both versions and at the
+file (`expected <cli-version>, found <file-version> in .cph-version`).
+
+### The 7th diagnostic class `cphVersionMismatch`
+
+The taxonomy grows from six to seven classes. `cphVersionMismatch` is
+**structural** (the loader decides it from a file read — no oracle needed),
+like `partPathMissing`/`unknownKind`; its severity is `error`. This is a
+real divergence point (the taxonomy is spec-pinned), so it lands in Lean
+(`Spec.Courseware.Check.Diagnostic.DiagKind`) and in `DiagCode`.
+
+### The compatibility rule is exact equality, for now — and is replaceable
+
+The current rule is: **the file's `.cph-version` must exactly equal the
+CLI's version.** This is deliberately the strictest choice — it fails
+loudly on any drift, which is the right default while the format is young
+(0.0.x). The rule is isolated in one function
+(`cph_model::versions_compatible`), so it can be relaxed later to a semver
+range (e.g. "same major" or "compatible minor") **without touching the
+diagnostic class, the spec, or the CLI** — only that one predicate changes.
+The taxonomy and the "it's a `cphVersionMismatch` error" contract are
+stable across that evolution.
+
+### A missing `.cph-version` is not (yet) an error
+
+If the file has no `.cph-version`, the check is skipped (no diagnostic) for
+now — existing files and the `mini`/`TH-141` fixtures predate the contract.
+Whether a missing file should itself be a `cphVersionMismatch` (or a softer
+warning) once the ecosystem migrates is left open. The KenKen lesson and
+this repo's examples carry the file as the migration's starting point.
+
+## Consequences
+
+- A curriculum file now declares the cph version it was authored against;
+  the CLI refuses incompatible versions with a clear diagnostic rather than
+  a downstream mystery.
+- The diagnostic taxonomy is seven classes (was six). The Lean master, the
+  `DiagCode` enum, and the severity mapping all gain `cphVersionMismatch`.
+- The compatibility predicate is the single place future semver relaxation
+  lands — a deliberate seam.
+- `cph check`/`build` against the repo's own examples requires those
+  examples' `.cph-version` to match the workspace version; the release
+  commit updates them together.
+
+## Open Questions / Deferred
+
+- **Missing-file policy.** Whether an absent `.cph-version` should become an
+  error (forcing migration) or a warning — deferred until the contract is
+  broadly adopted.
+- **Semver relaxation.** The exact equality rule is a placeholder; the real
+  compatibility intervals (per ADR-0014-style "what's a breaking change")
+  are settled when there is a real breaking change to justify loosening.
+- **Manifest vs file.** The version lives in a sibling file, not a
+  `[project] cph-version = …` manifest key. This mirrors how a toolchain
+  version is often a separate file (`.tool-versions`, `rust-toolchain`);
+  whether it should migrate into the manifest is open.

examples/TH-141/.cph-version

@@ -0,0 +1 @@
+0.0.2

spec/README.md

@@ -1,55 +1,74 @@
-# spec —— Lean 语义母本
+# spec —— 语义契约
 
-这是本 monorepo 的**契约**:产品各部件语义的上游参照,用 Lean 编写。它的定位与约束见仓库根 `README.md` 的"宪法"5 条——本文件只讲**怎么往这份契约里写东西**。
+## 这个项目在解决什么
 
-## 现状
+教研产出现在是一摞一次性的文档:写完就躺着,改一次要同步很多地方,没法校验、
+没法复用、没法追溯。这个项目想把教研产出变成可校验、可复用、能派生多种成品
+(讲义、教案、课件、归档)的工程化文件。
 
-刚初始化的 Lean 工程(`lake init`),目前只有占位内容(`Spec/Basic.lean`)。实质领域内容(System 平台层、Courseware 产品层)将逐个概念加入,每个都遵循下面的规范。
+但光有工程文件还不够。它要变成一个能卖钱的产品,还得:
 
-## 构建
+- 工程文件这种形式,正好适合现在大热的 LLM assistant 来改,从而提效;
+- 但 LLM 判不了一节课合不合法(它不能真去跑 typst 编译器、不能可靠地断言数据合不合
+  schema),所以产品里还有一个 rule-based checker:它真跑工具、给确定性的诊断,补上
+  LLM 判不了的这块。LLM 提效 + checker 兜底,两者一起才是完整的产品闭环。
+- 加上一些提升体验的小功能:飞书/企业微信集成、自动化提醒之类;
+- 如果要做 SaaS,还要有基本的管理概念:权限、LLM API 的配置和用量、费用等。
 
-```sh
-cd spec
-lake build
-```
+工程文件是起点,不是终点。
 
-工具链锁定在 `lean-toolchain`(`leanprover/lean4:v4.31.0`)。无外部依赖——Mathlib / Batteries 等留待第一个真正需要它的定理出现时再引入(依赖碰到再加)。
+## spec 是什么
 
-## 写作规范
+spec/ 是产品语义的契约,用 Lean 写。它定义产品各部件"是什么意思"。
 
-### 双半契约:prose + type
+- 它是开发者和 coding assistant 共同的语义依据:两边对某个东西的理解,以这里为准。
+- 它不进产品运行时。运行时真正做校验的那个东西用什么技术实现,还没定;但它的语义,
+  先在这里固定下来。
+- 它精确、自洽,机器能校验它内部结构没有漏洞。它不保证实现一定符合它——
+  实现和它是否一致,没有自动检查,要靠人工或 coding assistant 不定期(或每次改动后)核对。
 
-每个 top-level 声明**必须**带 `/-- … -/` doc 注释,用自然语言陈述其语义意图。两半缺一不可:
+## 人机怎么一起干活
 
-- **prose 半**给人读——说清"这在领域里是什么、为什么"。
-- **type 半**给机器读、给 type checker 把关——保证结构无洞。
+- 凭语义,不凭经验。这个领域新,coding assistant 在这里没有可靠的既有经验,
+  所以语义以 spec 的注释为准,不要凭训练先验臆测。
+- 契约没写的,就是不存在的。遇到没定的点,提出来让开发者定,不要替它选答案。
+- 改了实现或 spec 之后,两边是否还对得上,要核对一下;这一致性没有自动闸门。
 
-agent 不得用预训练先验脑补本领域(领域很新,无先验);prose 是 agent 理解语义的唯一权威来源。
+## 怎么往 spec 里写
 
-### 标签分类法
+### 一条东西要不要进 spec
 
-在 doc 注释里用以下标签标注每条语义的状态:
+不写它,开发者和 coding assistant 会不会各自做出不同假设?会,就进;不会
+(显然的事、纯基础设施、普通 CRUD 字段),就不进。
 
-- **`PINNED`** —— 已解决的分歧点,契约在此处权威,双方据此对齐。
-- **`OPEN`** —— 故意未规定。双方均**不得假设**其解;实现遇到时必须 surface 出来讨论,而不是擅自决定。
-- **`ADR-NNNN`** —— 链接到根 `docs/adr/` 下的对应决策记录(如 `ADR-0002`),交代该语义的决策出处。
+### 进了之后,钉到多细
 
-### 分歧点测试(写之前先过一遍)
+- 现在想清楚的,用 Lean 固定(声明、类型、关系)。
+- 没想清楚的,两三句话 prose 占位,标 `OPEN`。等讨论或业务反馈后再细化,
+  细化结果可以再用 Lean 固定。
+- 不在 Lean 里验证实现真的做了这些事。spec 只讲"要做什么、判什么";实现有没有真做,
+  不形式化证明。
+- 形式化定理:不用写;写了不是坏事,但现在很少有能写的定理。定理本身得是产品语义,
+  不是"实现该满足的性质"。
 
-新增任何概念前,先问:**"不写明,开发者与 agent 会不会各自做出不同假设?"**
+### 写的时候
 
-- 会 → 它是分歧点,入契约。
-- 不会(显然的东西 / 纯 plumbing / 普通 CRUD 字段)→ 不入。
-
-详见根 README 宪法第 5 条。
-
-### 不用 `sorry`
-
-无法陈述清楚的东西,用 `OPEN` 在 prose 里标注,而**不是**用 `sorry` 留一个假装成立的定理。`sorry` 会让 `lake build` 仍然变绿,却在契约里埋一个谎——这与"契约自包含、无洞"直接冲突。
+- 每个顶层声明要带 doc 注释,用 `/-- ... -/` 写自然语言,说清这在领域里是什么、为什么。
+  注释是语义的依据,Lean 类型保证结构,两者缺一不可。
+- 在注释里标这条语义的状态:
+  - `PINNED`:已定,契约在此处权威。
+  - `OPEN`:故意没定。不要假设它的解,遇到要提出来讨论。
+  - `ADR-NNNN`:指向 `docs/adr/` 下的决策记录。
+- 不用 `sorry`。没想清楚的,用 `OPEN` 标在注释里,不要用 `sorry` 假装成立——
+  那会让构建通过,却在契约里埋一个谎。
+- 不复述文件系统上能直接看到的东西(目录结构、文件名)。文件系统应当自描述,文档讲 context。
+- 不写变更史(进 git/ADR)。不搬 ADR 内部黑话,要表达就直说。
+  不为设计选择辩护("刻意用 X 而非 Y"),只说是什么。
+- "为什么"的背景考据(如某工具的内部机制)不进 spec,指向 ADR;但产品行为和设计模式要钉。
 
 ### 命名
 
-- **模块 / 命名空间**:PascalCase,对应分层,如 `Spec.System.Run`、`Spec.Courseware.Validity`。
-- **类型**:PascalCase。
-- **谓词 / `Prop`**:用意图清晰的命名,如 `Legal…`、`ValidTransition`、`Can…`。
-- **文件粒度**:原则上"一个带独立不变式的概念一个文件"。
+- 模块/命名空间:PascalCase,按分层,如 `Spec.System.Run`。
+- 类型:PascalCase。
+- 谓词(`Prop`):用意图清楚的词,如 `Legal…`、`ValidTransition`、`Can…`。
+- 文件粒度:一个带独立不变式的概念一个文件。

spec/Spec/Courseware.lean

@@ -6,16 +6,5 @@ import Spec.Courseware.Open
 /-!
 # Courseware —— 产品层契约(课程工程文件)
 
-护城河:课程"工程文件"的语义母本与合法性规则。决策出处 ADR-0005..0015。按四组组织:
-
-- **`Model`** —— 工程文件的内容模型:基元 `Primitives`、富内容 `RichContent`、原子
-  单位 `Element`、单节课 `Lesson`(element 的有序序列)。
-- **`Export`** —— export target = artifact + 有序 typed steps:产物 ADT `Artifact`
-  (`singleFile` / `fileTree`),build 规格 `TargetSpec`(artifact + steps + 覆盖声明
-  `covers`)与 `RenderConfig`。
-- **`Check`** —— checker 语义:`Severity` + 6 类诊断 + **合法 lesson = 无 error 级
-  诊断**(模型外设施诊断以抽象谓词 + `Oracle` 表示);检查管线的 5 阶段、序、compile
-  门控。
-- **`Open`** —— 留白骨架(核心关系 OPEN,已 surface 不臆造):题库 `QuestionBank`、
-  课程编排 `Course`。
+课程"工程文件"的语义母本与合法性规则。决策出处 ADR-0005..0016。
 -/

spec/Spec/Courseware/Check.lean

@@ -2,7 +2,7 @@ import Spec.Courseware.Check.Diagnostic
 import Spec.Courseware.Check.Pipeline
 
 /-!
-# Courseware.Check —— checker 语义
+# Courseware.Check —— 产品 checker 语义
 
 诊断分类与合法 lesson(`Diagnostic`)、检查管线的阶段与序(`Pipeline`)。决策出处
 ADR-0010。

spec/Spec/Courseware/Check/Diagnostic.lean

@@ -2,30 +2,39 @@ import Spec.Courseware.Model.Lesson
 import Spec.Courseware.Export.Render
 
 /-!
-# Diagnostic —— checker 诊断:分类、严重级别、合法 lesson
+# Diagnostic —— 产品 checker 的诊断
 
-产品里"站在 Lean 位置"的 rule-based checker,语义在此沉淀(ADR-0010,经 ADR-0012
-修订)。它对 lesson 提诊断,每条有**分类**(`DiagKind`)与**严重级别**(`Severity`)。
-本模块:钉级别类型(二分);钉 6 类诊断各自的含义与级别,并把"**合法 lesson = 无
-error 级诊断**"建成判定(ADR-0005 deferred 的"完整合法判定"的回填);对**模型外设施**
-型诊断(typst 编过否、数据合 schema 否)用**抽象谓词 + `Oracle` 实现边界**表示——契约
-说"存在这条诊断、什么意思、什么级别",真值由实现提供,不在 Lean 内计算(不内嵌 typst
-编译器)。引用解析(`@ref`、相对 import)不另设诊断:它们都是 typst 编译期失败,归
-`typstCompile`(ADR-0012)。
+这个 codebase 是要拿去卖的产品。LLM 辅助操作提效是它的核心卖点之一——但 LLM 判不了
+一节课合不合法:它不能真的去跑 typst 编译器、不能可靠地断言一段数据合不合 schema、
+也不能可靠地检查文件齐不齐。所以产品里有一个 rule-based checker 来做这件事:它真跑
+工具、给确定性的诊断,补上 LLM 判不了的这块。这个 checker 的语义在这里(ADR-0010,
+经 ADR-0012、ADR-0016 修订)。它对 lesson 提诊断,每条有一个分类(`DiagKind`)和一
+个严重级别(`Severity`)。
+
+注意区分两个"检查":这里的 checker 是**产品功能**——用户把教研工程文件喂给 `cph`,
+检查这个工程文件合不合法。它和"开发时 spec 与实现是否一致"是两回事,后者没有自动
+闸门,靠核对。
+
+本模块钉三件事:严重级别二分;7 类诊断各自的含义和级别;"合法 lesson = 无 error 级
+诊断"这条判定。其中有些诊断是 LLM 判不了、得 checker 真跑工具才能判的(typst 编不编
+得过、数据合不合 schema、content 文件齐不齐)——这些用抽象谓词加 `Oracle` 表示:契约
+说"存在这条诊断、什么意思、什么级别",真值由 checker 给(契约不在 Lean 里内嵌 typst
+编译器去算)。引用解析(`@ref`、相对 import)不单列:它们都是 typst 编译期失败,归
+`typstCompile`(ADR-0012)。版本契约 `cphVersionMismatch`(ADR-0016)是第 7 类。
 -/
 
 namespace Spec.Courseware
 
-/-- 诊断严重级别(`PINNED` 二分, ADR-0005)。`error` 阻断(产物不合法),`warning` 不
-阻断(产物仍可导出,只是有损)。更细级别(info/hint)未决策,故只二分。 -/
+/-- 诊断严重级别(ADR-0005)。`error` 阻断(产物不合法),`warning` 不阻断(产物仍可导出,
+    只是有损)。更细级别(info/hint)未决策,故只二分。 -/
 inductive Severity where
   | warning
   | error
 
-/-- 诊断**分类**(`PINNED` 6 类, ADR-0010,经 ADR-0012 修订为 6 类)。按"谁来判定"分
-三层:**结构型**(模型自身可判):`partPathMissing`/`unknownKind`;**schema/外部设施型**
-(靠实现 oracle):`missingContentFile`/`schemaViolation`/`typstCompile`;**语义型**:
-`renderIgnored`。 -/
+/-- 诊断分类(ADR-0010,经 ADR-0012 折并为 6 类、ADR-0016 增至 7 类)。按 checker 怎么判分三层:
+    结构型(checker 自己按结构判):`partPathMissing`/`unknownKind`/`cphVersionMismatch`;
+    schema/外部工具型(得真跑工具):`missingContentFile`/`schemaViolation`/`typstCompile`;
+    语义型:`renderIgnored`。 -/
 inductive DiagKind where
   /-- manifest 的 part 指向不存在的文件夹(或经 `..` 逃出根)。结构型。 -/
   | partPathMissing
@@ -36,15 +45,19 @@ inductive DiagKind where
   /-- 实例数据不合其 kind 的 JSON Schema;亦作 manifest/element.toml 畸形的兜底。 -/
   | schemaViolation
   /-- 拼装出的 typst 源编译失败:语法错、未解析的交叉引用 `@ref`、越界或缺失的相对
-      `import`/`include`(后两者即旧 `danglingReference` 的两种情形——typst 在编译期
-      检出,故归此类,ADR-0012)。外部设施型。 -/
+      `import`/`include`。后两者 typst 在编译期检出,故归此类(ADR-0012)。外部工具型。 -/
   | typstCompile
   /-- 某被用到的 kind 在某声明的 target 下无渲染规则,该 element 被忽略。语义型。 -/
   | renderIgnored
+  /-- 工程文件的 `.cph-version` 与 CLI(cph)版本不相容(ADR-0016)。结构型(加载期判)。
+      工程文件根的 `.cph-version` 声明它所面向的 cph 版本;CLI 加载时比对自身版本,不相容
+      即产此类。当前判定为版本完全相等才相容(MVP;后续可放宽为 semver 区间,判定逻辑可
+      逐步改而不动本分类)。`error` 级——版本不相容的工程文件不应被该 CLI 处理。 -/
+  | cphVersionMismatch
 
-/-- 每类诊断的**严重级别**(`PINNED`, ADR-0010)。五类 `error`(阻断);**唯
-`renderIgnored` 为 `warning`**——ADR-0005 种子规则"缺渲染 ⇒ warning,不阻断导出"。
-钉成全函数使"哪类阻断"成为可引用、可对齐的事实(实现侧 `DiagCode` 级别据此对齐)。 -/
+/-- 每类诊断的严重级别(ADR-0010)。六类 `error`(阻断);唯 `renderIgnored` 为 `warning`
+    ——ADR-0005 种子规则"缺渲染 ⇒ warning,不阻断导出"。钉成全函数使"哪类阻断"成为可
+    引用、可对齐的事实。 -/
 def DiagKind.severity : DiagKind → Severity
   | .partPathMissing    => .error
   | .unknownKind        => .error
@@ -52,47 +65,53 @@ def DiagKind.severity : DiagKind → Severity
   | .schemaViolation    => .error
   | .typstCompile       => .error
   | .renderIgnored      => .warning
+  | .cphVersionMismatch => .error
 
-/-- 缺渲染诊断的级别 = **warning**(`PINNED`, ADR-0005/0010,**非 error**)。具名常量,
-使"它是 warning"可被实现侧 grep 对齐(实现里同名常量 `RENDER_IGNORED_SEVERITY` 引用
-本定义)。等价于 `DiagKind.renderIgnored.severity`。 -/
+/-- 缺渲染诊断的级别 = warning(ADR-0005/0010,非 error)。具名常量,使"它是 warning"
+    可被实现 grep 对齐(实现里同名常量 `RENDER_IGNORED_SEVERITY` 引用本定义)。
+    等价于 `DiagKind.renderIgnored.severity`。 -/
 def renderIgnoredSeverity : Severity := DiagKind.renderIgnored.severity
 
 variable (P : Primitives)
 
-/-- **缺渲染诊断**:lesson 在 target `t` 下存在无法渲染的 element(`PINNED`,
-ADR-0005/0009)。成立 ⟺ 存在某 element,其 kind 在 `t` 下 `covers` 为假。语义型诊断,
-级别 warning。 -/
+/-- 缺渲染诊断:lesson 在 target `t` 下存在无法渲染的 element(ADR-0005/0009)。成立 ⟺
+    存在某 element,其 kind 在 `t` 下 `covers` 为假。语义型诊断,级别 warning。 -/
 def renderIgnored (l : Lesson P) (c : RenderConfig P) (t : P.TargetId) : Prop :=
   ∃ e ∈ l, ¬ c.covers e.kind t
 
 /-!
-## 模型外设施型诊断:抽象谓词 + 实现边界(ADR-0010)
+## 要真跑工具才能判的诊断:抽象谓词 + Oracle
 
-`typstCompile`/`schemaViolation`(的 schema-合规面)断言的是模型自身无法判定的事实——
-要跑 typst 编译器、schema 校验器。契约把它们建成**抽象谓词**,真值由实现提供的 oracle
-给出。下面用 `Oracle` 收口这些判定:它不是要在 Lean 里实现 checker,而是把"这些事实
-来自模型外"显式化、类型化。
+诊断分两类(按 checker 怎么判):有些 checker 自己按工程文件结构就能判(part 路径
+在不在、kind 知不知道、某 kind 在某 target 下有没有被覆盖);有些 checker 自己也判
+不了,得真跑外部工具——typst 编不编得过(要跑 typst 编译器)、数据合不合 schema(要
+跑 schema 校验器)、content 文件齐不齐(要看磁盘)。后者就是 `Oracle` 收口的。
+
+`Oracle` 把这些"得 checker 委托外部工具才能判"的事实建成抽象谓词,真值由 checker 给。
+它不是要在 Lean 里实现 checker,而是把"这几件事 checker 自己算不了、得委托出去"显式
+表达、类型化。它只收 Legal 需要的、得委托外部工具的事实;checker 自己能判的(如
+`renderIgnored`)不进 Oracle。
+
+(这两类 checker 都判得了;但 LLM 两类都判不了——这正是产品里要有个 rule-based
+checker 的理由,见本模块顶部。)
 -/
 
-/-- **实现侧判定 oracle**(`PINNED` 实现边界, ADR-0010)。每个字段是一个谓词,真值由
-实现(checker)提供。结构型诊断(part 路径、未知 kind)不入此 oracle——那些模型自身可判。 -/
+/-- checker 委托外部工具才能判的那些事实(ADR-0010)。每个字段是一个谓词,真值由
+    checker 提供。checker 自己按结构就能判的诊断(part 路径、未知 kind)不入此 oracle。 -/
 structure Oracle (l : Lesson P) (c : RenderConfig P) where
-  /-- target `t` 下拼装源可编译(否 ⇒ `typstCompile`)。**含引用解析**:源能编译即蕴含
-      其 `@ref`、相对 import 全部解析(ADR-0012 已把引用诊断并入 `typstCompile`)。 -/
+  /-- target `t` 下拼装源可编译(否 ⇒ `typstCompile`)。含引用解析:源能编译即蕴含其
+      `@ref`、相对 import 全部解析(ADR-0012)。 -/
   compiles : P.TargetId → Prop
   /-- 每个 element 数据合 schema(否 ⇒ `schemaViolation`)。 -/
   dataConforms : Prop
   /-- schema 要求的 content 文件齐备(否 ⇒ `missingContentFile`)。 -/
   contentFilesPresent : Prop
 
-/-- **合法 lesson**(`PINNED`, ADR-0010;回填 ADR-0005 deferred 的"完整合法判定")。
-
-合法 ⟺ 检查管线产出**零条 error 级诊断**。展开为:模型外设施判定(经 `Oracle`)全为真,
-**且**每个声明的 target 都编译通过。结构型诊断由 `cph-model` 在加载期判定;能走到这步
-谈合法性意味着已加载成功,故此处聚焦 schema/外部设施层。引用解析不单列——已被
-`compiles` 蕴含(ADR-0012)。`renderIgnored` 是 warning,**不**进合取——ADR-0005 种子
-规则的体现。`targets` 用全称式表达以不绑定 `TargetId` 的可枚举性。 -/
+/-- 合法 lesson(ADR-0010)。合法 ⟺ 检查管线产出零条 error 级诊断。展开为:得委托外部
+    工具的判定(经 `Oracle`)全为真,且每个声明的 target 都编译通过。checker 自己按结构
+    能判的诊断(part 路径、未知 kind)在加载期已判;能走到这步谈合法性意味着那些已过,
+    故此处聚焦 schema/外部工具层。`renderIgnored` 是 warning,不进合取(ADR-0005 种子
+    规则)。`targets` 用全称式表达以不绑定 `TargetId` 的可枚举性。 -/
 def Legal (l : Lesson P) (c : RenderConfig P) (o : Oracle P l c) : Prop :=
   o.dataConforms ∧ o.contentFilesPresent ∧
     (∀ t : P.TargetId, (c.spec t).isSome → o.compiles t)

spec/Spec/Courseware/Check/Pipeline.lean

@@ -1,24 +1,24 @@
 import Spec.Courseware.Check.Diagnostic
 
 /-!
-# Pipeline —— checker 检查管线的阶段与序(ADR-0010)
+# Pipeline —— 检查管线的阶段与序
 
-checker 的 `check` 按**固定顺序**跑五个阶段,逐阶段收集诊断;`compile` 阶段有**门控**。
-顺序与门控是契约——它决定用户看到哪些诊断(藏在缺文件背后的语法错,在文件补齐前不
-显示,这是有意的)。每阶段的**算法**不进 Lean(宪法第 5 条深度上限):只钉**阶段、序、
-门控**。阶段对应上游模块:`load`←`cph-model`;`structural`←part 路径/未知 kind;
-`schema`←`cph-schema`;`compile`←`cph-typst`(模型外设施);`coverage`←`renderIgnored`。
+checker 的 `check` 按固定顺序跑五个阶段,逐阶段收集诊断;`compile` 阶段有门控。顺序和
+门控是契约——它决定用户看到哪些诊断(藏在缺文件背后的语法错,在文件补齐前不显示,这是
+有意的)。每阶段的算法不进 Lean(宪法第 5 条深度上限):只钉阶段、序、门控。
 -/
 
 namespace Spec.Courseware
 
-/-- 检查管线的**阶段**(`PINNED` 5 阶段, ADR-0010)。
+/-- 检查管线的阶段(ADR-0010)。
 
-- `load` —— 解析 manifest + 各 element.toml。硬失败则**停**整条管线。
+- `load` —— 解析 manifest + 各 element.toml。含 `.cph-version` 兼容性判定(ADR-0016:
+  工程根 `.cph-version` 与 CLI 版本不相容 ⇒ `cphVersionMismatch` error)。硬失败(无法
+  解析 lesson)则停整条管线。
 - `structural` —— part 路径存在、无 `..`、kind 已知且一致。此处判缺的 part 后续跳过。
 - `schema` —— 每个"存在且 kind 已知"的 part 按其 kind schema 校验。
-- `compile` —— 模型外设施阶段(typst 编译)。**门控:仅当前序零 error 才跑**。
-- `coverage` —— 语义型 warning(`renderIgnored`);**不**受门控,总跑。 -/
+- `compile` —— 跑外部工具的阶段(typst 编译)。门控:仅当前序零 error 才跑。
+- `coverage` —— 语义型 warning(`renderIgnored`);不受门控,总跑。 -/
 inductive Phase where
   | load
   | structural
@@ -27,8 +27,8 @@ inductive Phase where
   | coverage
 deriving DecidableEq
 
-/-- 管线阶段的**执行序**(`PINNED`, ADR-0010)。`order p` 越小越先跑。序是契约:
-`compile`(3)排在 `structural`(1)/`schema`(2)之后,正因前者门控于后者无 error。 -/
+/-- 管线阶段的执行序(ADR-0010)。`order p` 越小越先跑。序是契约:`compile`(3)排在
+    `structural`(1)/`schema`(2)之后,正因前者门控于后者无 error。 -/
 def Phase.order : Phase → Nat
   | .load       => 0
   | .structural => 1
@@ -36,15 +36,14 @@ def Phase.order : Phase → Nat
   | .compile    => 3
   | .coverage   => 4
 
-/-- 某阶段是否**受"前序零 error"门控**(`PINNED`, ADR-0010)。唯 `compile` 受门控:藏在
-结构/schema 错背后的编译错,在前者修好前不显示——有意降噪。 -/
+/-- 某阶段是否受"前序零 error"门控(ADR-0010)。唯 `compile` 受门控:藏在结构/schema 错
+    背后的编译错,在前者修好前不显示——有意降噪。 -/
 def Phase.gated : Phase → Bool
   | .compile => true
   | _        => false
 
-/-- 管线在 `load` 硬失败时**停**(`PINNED`, ADR-0010)。`load` 拿不到可解析 lesson 时,
-无 lesson 可喂下游,整条管线终止——唯一会截断后续所有阶段的情形(区别于 `compile`
-门控只跳过自己)。 -/
+/-- 管线在 `load` 硬失败时停(ADR-0010)。`load` 拿不到可解析 lesson 时,无 lesson 可喂
+    下游,整条管线终止——唯一会截断后续所有阶段的情形(区别于 `compile` 门控只跳过自己)。 -/
 def Phase.haltsPipelineOnFailure : Phase → Bool
   | .load => true
   | _     => false

spec/Spec/Courseware/Export.lean

@@ -4,5 +4,5 @@ import Spec.Courseware.Export.Render
 /-!
 # Courseware.Export —— export target = artifact + 有序 typed steps
 
-产物 ADT(`Artifact`)、build 规格与渲染覆盖(`Render`)。决策出处 ADR-0009 / 0011。
+产物 ADT、build 规格与渲染覆盖。决策出处 ADR-0009 / 0011。
 -/

spec/Spec/Courseware/Export/Artifact.lean

@@ -1,23 +1,22 @@
 /-!
-# Artifact —— export target 的产物(ADR-0009 / 0011)
+# Artifact —— export target 的产物
 
-ADR-0009:一个 export target 是**一次 build**,产出一个**有类型的产物**。ADR-0011
-钉死:产物是**带字段的 ADT**——"产物到底指什么"(单文件落在哪 / 一棵树产出哪些文件)
-是不好猜的领域语义,必须写进字段 + doc,而非抹成两个空构造子。路径/glob 用 `String`
-承载并由 doc 赋义(它们就是文本),不复刻文件系统类型。
+一个 export target 是一次 build,产出一个有类型的产物(ADR-0009、ADR-0011)。产物是
+带字段的 ADT:"产物到底指什么"(单文件落在哪 / 一棵树产出哪些文件)是不好猜的领域
+语义,要写进字段 + doc,而不是抹成两个空构造子。路径、glob 用 `String` 承载并由 doc
+赋义(它们就是文本),不复刻文件系统类型。
 -/
 
 namespace Spec.Courseware
 
-/-- export 产物(`PINNED` 带字段 ADT, ADR-0011)。产物形状决定 `cph build` 吐文件还是
-目录、reduce 怎么折叠(`singleFile` 把有序片段拼成一份再编译——交叉引用 `@ref`、例题
-计数器能工作的前提;`fileTree` 每 part 落一文件)。后端/格式仍 OPEN(ADR-0009)。 -/
+/-- export 产物(ADR-0011)。产物形状决定 `cph build` 吐文件还是目录、reduce 怎么折叠
+    (`singleFile` 把有序片段拼成一份再编译——交叉引用 `@ref`、例题计数器能工作的
+    前提;`fileTree` 每 part 落一文件)。后端、格式仍 OPEN(ADR-0009)。 -/
 inductive Artifact where
   /-- 单文件产物,落在 `filepath`(相对工程根)。讲义/教案 PDF 即此。 -/
   | singleFile (filepath : String)
-  /-- 多文件产物:`root` 目录下匹配 `outputs` **glob** 的文件集(第三方平台 archive
-      即此)。用 glob 而非显式清单:轻,又让消费方/checker 知道该产出哪些文件、可校验
-      完整性。 -/
+  /-- 多文件产物:`root` 目录下匹配 `outputs` glob 的文件集(第三方平台归档即此)。
+      用 glob 而非显式清单:轻,又让消费方/checker 知道该产出哪些文件、可校验完整性。 -/
   | fileTree (root : String) (outputs : String)
 
 end Spec.Courseware

spec/Spec/Courseware/Export/Render.lean

@@ -2,88 +2,89 @@ import Spec.Courseware.Model.Primitives
 import Spec.Courseware.Export.Artifact
 
 /-!
-# Render —— export target = artifact + 有序 typed steps(ADR-0009 / 0011)
+# Render —— export target = artifact + 有序 typed steps
 
-ADR-0009:export target 是一次 build,产出一个有类型的 `Artifact`。ADR-0011 钉死 build
-的**形状**:一个 target 是 `artifact` + 一串**有序 typed step**。
+一个 export target 是一次 build,产出一个有类型的 `Artifact`(ADR-0009)。build 的形状
+是:一个 target = `artifact` + 一串有序的 typed step(ADR-0011)。
 
-- `typstCompile template` —— 把**模板文件**(如 `exports/student.typ`)编译成产物。它是
-  *typed* 而非裸 shell,正因框架要把 **manifest 注入**模板(经 `--input manifest=…`),
-  裸字符串表达不了这个 wiring。presentation(编号、样式)住模板里,不在 manifest。
-- `shell run` —— 逃生口,给难以声明的步骤(ADR-0005 的 (b) 类 medium-only)。
-- `assembleMarkdown field` —— 按 parts 顺序把每个 element 的 `field`(markdown content 叶子,
-  ADR-0015)拼成**单文件 markdown** 产物。typed 而非 `cat`,因为按 manifest `[[parts]]` 顺序读取 +
-  跳过缺失项 + 写到单文件产物路径这件事,框架 own 比裸 shell 稳。
+- `typstCompile template` —— 把模板文件(如 `exports/student.typ`)编译成产物。它是
+  typed 而非裸 shell,因为框架要把 manifest 注入模板(经 `--input manifest=…`),裸
+  字符串表达不了这个 wiring。presentation(编号、样式)住模板里,不在 manifest。
+- `shell run` —— 逃生口,给难以声明的步骤。
+- `assembleMarkdown field` —— 按 parts 顺序把每个 element 的 `field`(markdown content
+  叶子,ADR-0015)拼成单文件 markdown 产物。typed 而非裸 `cat`:按 manifest `[[parts]]`
+  顺序读取 + 跳过缺失项 + 写到单文件产物路径,框架自己来比裸 shell 稳。
 
-**渲染覆盖**:ADR-0011 废止了 per-target `RenderRule` 载荷——渲染的"how"已移进模板。
-契约只保留覆盖声明 `covers`(该 target 渲染哪些 kind),供种子诊断用。
+渲染覆盖:契约只保留覆盖声明 `covers`(该 target 渲染哪些 kind),供种子诊断用;渲染的
+"how"住模板里(ADR-0011)。
 
-**shell step 的执行语义(ADR-0013)。** `shell` 不再只是占位:它**会被执行**,语义是把
-`run` 交给平台 shell、以**工程根为工作目录**运行,产物由被调外部工具自己写出(框架不装配
-内容)。三条边界是真分歧点,故钉契约:
-1. **opt-in by construction** —— 任意命令执行只在用户**显式** build 一个 shell target 时发生,
-   绝不在 `check` 里跑。`check` 只校验结构(lesson 是否合法),不执行外部工具、不验其产物。
-2. **失败归属** —— shell step 退出非零是一次 **build-过程失败**,不是 lesson 的合法性缺陷;
-   因此它**不**进 `Diagnostic` 的 6 类(那 6 类是 lesson 自身的诊断,见 `Check/Diagnostic.lean`),
-   而由 build 执行层报告。诊断分类保持 6 类不变(ADR-0013 显式拒绝新增 `ShellStep` 诊断码)。
-3. **非-typst target 不过 typst 编译** —— 一个只含 `shell` step 的 target(教具包即此)由
+shell step 的执行语义(ADR-0013):`shell` 会被执行,语义是把 `run` 交给平台 shell、以
+工程根为工作目录运行,产物由被调外部工具自己写出(框架不装配内容)。三条边界:
+
+1. opt-in:命令执行只在用户显式 build 一个 shell target 时发生,绝不在 `check` 里跑。
+   `check` 只校验结构,不执行外部工具、不验其产物。
+2. 失败归属:shell step 退出非零是一次 build 过程失败,不是 lesson 的合法性缺陷;因此
+   它不进 `Diagnostic` 的 7 类(那 7 类是 lesson 自身的诊断,见 `Check/Diagnostic.lean`),
+   而由 build 执行层报告。诊断分类保持 7 类不变。
+3. 非-typst target 不过 typst 编译:一个只含 `shell` step 的 target(教具包即此)由
    执行器跑命令,而非走 typst 引擎;`check` 的 compile 阶段跳过它。
 
-**assembleMarkdown step 的执行语义(ADR-0015)。** 与 `shell` 同属"非-typst target":框架 own
-读取每个 element 的 `<field>.md`、按 `[[parts]]` 顺序拼接、写到单文件产物路径(产物是 markdown,
-不经 typst 引擎)。同 shell 的三条边界:① 只在显式 `build --target` 跑,`check` 不跑;② 装配失败
-(如写盘失败、引用图缺失)是 build-过程错误,不入 6 类诊断;③ 非-typst target,`check` 的 compile
-阶段跳过它。**单文件产物**(现):装配器注入课程级标题为文档 h1(课程元数据,非 element 内容),
-每份 `slides.md`/`transcript.md` 贡献其 `##` part 与 `###` 小节(presentation 在内容里, ADR-0011),
-按 `[[parts]]` 顺序拼接(分隔符空行)。**自包含**:装配器扫描产物里的 `![](rel)` 图引用,把引用到的
-本地图从工程根按原相对路径复制进产物所在 build 根,使该 build 目录可独立交付;引用图在工程根缺失属
-build-过程错误(不入 6 类)。外部 URL(`http(s)://`/`data:`)不复制。结构化 FileTree 产物延后
-(待 parts 树形重组, ADR-0015 OPEN)。
+assembleMarkdown step 的执行语义(ADR-0015):与 `shell` 同属"非-typst target"。框架
+自己读每个 element 的 `<field>.md`、按 `[[parts]]` 顺序拼接、写到单文件产物路径(产物
+是 markdown,不经 typst 引擎)。同 shell 的三条边界:① 只在显式 `build --target` 跑,
+`check` 不跑;② 装配失败(如写盘失败、引用图缺失)是 build 过程错误,不入 7 类诊断;
+③ 非-typst target,`check` 的 compile 阶段跳过它。
+
+单文件产物(现):装配器注入课程级标题为文档 h1(课程元数据,非 element 内容),每份
+`slides.md`/`transcript.md` 贡献其 `##` part 与 `###` 小节(presentation 在内容里,
+ADR-0011),按 `[[parts]]` 顺序拼接(分隔符空行)。自包含:装配器扫描产物里的 `![](rel)`
+图引用,把引用到的本地图从工程根按原相对路径复制进产物所在 build 根,使该 build 目录
+可独立交付;引用图在工程根缺失属 build 过程错误(不入 7 类)。外部 URL(`http(s)://`、
+`data:`)不复制。结构化 FileTree 产物延后(待 parts 树形重组,ADR-0015 OPEN)。
 -/
 
 namespace Spec.Courseware
 
 variable (P : Primitives)
 
-/-- 一个 build **step**(`PINNED` typed, ADR-0011;可扩展)。MVP 仅一个 `typstCompile`;
-`steps` 是 list 因为 FileTree / 第三方 build 会需多步。刻意不把模板内部、shell 命令的
-解析结构写进来(实现细节, ADR-0011 OPEN)。 -/
+/-- 一个 build step(ADR-0011;可扩展)。MVP 仅一个 `typstCompile`;`steps` 是 list 因为
+    FileTree、第三方 build 会需多步。不把模板内部、shell 命令的解析结构写进来(实现细节,
+    ADR-0011 OPEN)。 -/
 inductive Step where
   /-- 编译模板文件 `template`(相对工程根)成产物;框架注入 manifest。typed 的理由:
       注入这件事裸 shell 写不出。 -/
   | typstCompile (template : String)
-  /-- shell 逃生口:执行命令 `run`(ADR-0005 (b) 类落这)。**已实现**(ADR-0013):以工程根
-      为 cwd 执行,opt-in(只在显式 build 该 target 时跑,`check` 不跑),失败属 build-过程错误
-      而非 lesson 诊断。教具包(如 KenKen 交互 HTML 由外部 `kendoku` 生成)即走此 step。 -/
+  /-- shell 逃生口:执行命令 `run`(ADR-0013)。以工程根为 cwd 执行,opt-in(只在显式
+      build 该 target 时跑,`check` 不跑),失败属 build 过程错误而非 lesson 诊断。
+      教具包(如 KenKen 交互 HTML 由外部 `kendoku` 生成)即走此 step。 -/
   | shell (run : String)
   /-- 装配 markdown:按 `[[parts]]` 顺序读取每个 element 的 `field`(markdown content 叶子,
-      ADR-0015),注入课程 h1 后拼接成**单文件 markdown** 产物,并收集 `![](rel)` 引用的本地图进
-      build 根使产物自包含。typed 而非 `cat`:按序读取+跳过缺失+注入标题+写盘+收集图由框架 own。
-      **已实现**(ADR-0015):非-typst target(`check` 不跑,失败属 build-过程错误不入 6 类诊断)。
-      slides 大纲面 / 逐字稿口播面即走此 step(直接 markdown+KaTeX 撰写,绕开 typst→md 公式转换,
-      ADR-0014 R2)。 -/
+      ADR-0015),注入课程 h1 后拼接成单文件 markdown 产物,并收集 `![](rel)` 引用的本地图
+      进 build 根使产物自包含。typed 而非 `cat`:按序读取+跳过缺失+注入标题+写盘+收集图由
+      框架自己来。非-typst target(`check` 不跑,失败属 build 过程错误不入 7 类诊断)。
+      slides 大纲、逐字稿口播即走此 step(直接 markdown+KaTeX 撰写,绕开 typst→md 公式转换,
+      ADR-0014)。 -/
   | assembleMarkdown (field : String)
 
-/-- 一个 export target 的 build 规格(`PINNED` artifact + 有序 steps, ADR-0011)。 -/
+/-- 一个 export target 的 build 规格(ADR-0011:artifact + 有序 steps)。 -/
 structure TargetSpec where
   /-- 产物(带字段,ADR-0011)。决定 build 折叠成单文件还是文件树。 -/
   artifact : Artifact
-  /-- **有序** build steps。按序执行;MVP 仅一个 `typstCompile`。 -/
+  /-- 有序 build steps。按序执行;MVP 仅一个 `typstCompile`。 -/
   steps : List Step
-  /-- **覆盖声明**:`covers k` 表示此 target 渲染 kind `k`。ADR-0011 把旧
-      `renders : KindId → Option RenderRule` 降级后的产物——契约只声明"渲染哪些 kind"
-      (种子诊断 `renderIgnored` 用),"how"由 `steps` 的模板实现。 -/
+  /-- 覆盖声明:`covers k` 表示此 target 渲染 kind `k`。契约只声明"渲染哪些 kind"
+      (种子诊断 `renderIgnored` 用),"how"由 `steps` 的模板实现(ADR-0011)。 -/
   covers : P.KindId → Prop
 
-/-- 渲染配置(`PINNED` target-中心, ADR-0009/0011)。`spec t = none` 表示 target `t`
-未声明(不导出);`some s` 给出其 build 规格。 -/
+/-- 渲染配置(ADR-0009/0011)。`spec t = none` 表示 target `t` 未声明(不导出);
+    `some s` 给出其 build 规格。 -/
 structure RenderConfig where
   /-- target ↦ 该 target 的 build 规格(未声明则 `none`)。 -/
   spec : P.TargetId → Option (TargetSpec P)
 
-/-- kind `k` 在 target `t` 下**被渲染**(`PINNED`, ADR-0009/0011;承接 ADR-0005)。成立
-⟺ `t` 已声明(`spec t = some s`)**且** `s.covers k`。为假即"此 kind 在此 target 下不
-被渲染"——checker 据此报 warning(见 `Diagnostic.renderIgnored`)。`P` 隐式以便点记法。 -/
+/-- kind `k` 在 target `t` 下被渲染(ADR-0009/0011)。成立 ⟺ `t` 已声明
+    (`spec t = some s`)且 `s.covers k`。为假即"此 kind 在此 target 下不被渲染"——
+    checker 据此报 warning(见 `Diagnostic.renderIgnored`)。 -/
 def RenderConfig.covers {P : Primitives} (c : RenderConfig P)
     (k : P.KindId) (t : P.TargetId) : Prop :=
   match c.spec t with

spec/Spec/Courseware/Model.lean

@@ -7,7 +7,5 @@ import Spec.Courseware.Model.Info
 /-!
 # Courseware.Model —— 工程文件的内容模型
 
-留白基元(`Primitives`)、富内容锚点(`RichContent`)、原子单位(`Element`)、单节课
-(`Lesson`)、课时元信息(`Info`:canonical author 为列表 vs `RawInfo` 撰写态)。
-决策出处 ADR-0005 / 0006 / 0008。
+基元、富内容、element、lesson、课时元信息。决策出处 ADR-0005 / 0006 / 0008。
 -/

spec/Spec/Courseware/Model/Element.lean

@@ -1,24 +1,23 @@
 import Spec.Courseware.Model.Primitives
 
 /-!
-# Element —— 课程内容的原子单位
+# Element —— 课程内容的最小单位
 
-ADR-0005:element 实例 = 一个 kind 标签 + 符合该 kind schema 的数据。本模块把它编码成
-依赖结构,使"数据必须匹配其 kind"成为类型层面的事实而非运行时校验。
+一个 element = 一个 kind 标签 + 符合该 kind schema 的数据(ADR-0005)。
+用依赖结构编码,使"数据必须匹配 kind"成为类型层面的事实,不是运行时校验。
 -/
 
 namespace Spec.Courseware
 
 variable (P : Primitives)
 
-/-- element 实例(`PINNED`, ADR-0005)。`data : P.ElementData kind` 由 `kind` 决定——
-无法构造数据与 kind 不符的 element,schema 合规由类型系统保证。ADR-0005 的 (a) 类
-字段(逐字稿、重点圈划)落在具体 kind 的 `ElementData` 内,不出现在此通用结构上;
-交互教具等"重型 kind"在此与例题、定理同构,仅 `kind` 不同,重实现在模型之外。 -/
+/-- 一个 element 实例(ADR-0005)。data 的类型由 kind 决定,所以没法造出数据和 kind
+    不符的 element——schema 合规由类型保证。逐字稿、重点圈划这类跟具体 kind 强相关
+    的字段,落在该 kind 的 ElementData 里,不放在这个通用结构上。 -/
 structure Element where
-  /-- 该 element 的 kind。 -/
+  /-- 这个 element 的 kind。 -/
   kind : P.KindId
-  /-- 符合 `kind` schema 的数据(类型随 `kind` 而变)。 -/
+  /-- 符合 kind schema 的数据,类型随 kind 变。 -/
   data : P.ElementData kind
 
 end Spec.Courseware

spec/Spec/Courseware/Model/Info.lean

@@ -1,56 +1,54 @@
 /-!
-# Info —— 课时元信息:canonical 模型 vs 撰写态(authoring surface)
+# Info —— 课时元信息:canonical 模型 vs 撰写态
 
-`[info]`(标题、作者)大多是 passthrough 元数据(ADR-0008),本不入契约。但**作者的
-基数**是一个真分歧点:一节课可由多人(教研组)署名,故 canonical 模型里 author 是一个
-**有序列表**,不是单值或可选单值。
+`[info]`(标题、作者)大多是 passthrough 元数据(ADR-0008),本不入契约。但作者的
+基数是一个真分歧点:一节课可由多人(教研组)署名,故 canonical 模型里 author 是一个
+有序列表,不是单值或可选单值。
 
-另有一条值得钉的模式:on-disk 的**撰写态**(用户实际填写的形态)是**语法糖**——单作者可写
-`author = "…"`,多作者写 `author = ["…", "…"]`——但这个"字符串或数组"的二态**只活在加载
-边界**:`RawInfo` 经归一化折叠成 canonical `Info`,其后不再出现。canonical 接收端始终是
-`List String`,raw 形式不泄漏进模型其余部分。这正是 `Info`(canonical)与 `RawInfo`
-(撰写态)两个结构存在的理由。
+另有一条值得钉的模式:on-disk 的撰写态(用户实际填写的形态)是语法糖——单作者可写
+`author = "…"`,多作者写 `author = ["…", "…"]`——但这个"字符串或数组"的二态只活在
+加载边界:`RawInfo` 经归一化折叠成 canonical `Info`,其后不再出现。canonical 接收端
+始终是 `List String`,raw 形式不泄漏进模型其余部分。这正是 `Info`(canonical)与
+`RawInfo`(撰写态)两个结构存在的理由。
 -/
 
 namespace Spec.Courseware
 
-/-- 作者的**撰写态形式**(`PINNED` 仅填写便利, ADR-0008)。on-disk 单作者可写裸
-字符串、多作者写数组——填写便利,非语义分歧。此 union **只活在加载边界**,经
-`RawAuthor.normalize` 折叠后不再出现。 -/
+/-- 作者的撰写态形式(ADR-0008)。on-disk 单作者可写裸字符串、多作者写数组——填写便利,
+    非语义分歧。此 union 只活在加载边界,经 `RawAuthor.normalize` 折叠后不再出现。 -/
 inductive RawAuthor where
   /-- 单作者裸字符串 `author = "…"`。 -/
   | one (name : String)
   /-- 多作者数组 `author = ["…", "…"]`。 -/
   | many (names : List String)
 
-/-- raw 作者归一化为**有序作者列表**(`PINNED`, ADR-0008)。单作者 ⇒ 单元素列表;数组
-⇒ 原样。这条钉死"canonical 接收端始终是 `List String`"。 -/
+/-- raw 作者归一化为有序作者列表(ADR-0008)。单作者 ⇒ 单元素列表;数组 ⇒ 原样。
+    这条钉"canonical 接收端始终是 `List String`"。 -/
 def RawAuthor.normalize : RawAuthor → List String
   | .one n => [n]
   | .many ns => ns
 
-/-- 课时元信息的 **canonical 模型**(`PINNED` author 为列表, ADR-0008)。`authors` 是
-**有序列表**:多人署名第一类,空列表 = 未署名。`title` 等其余字段是 passthrough 元数据,
-不在此承诺更多。这是系统其余部分唯一所见的形态——author 在此**已**是列表,不再是
-"字符串或数组"。 -/
+/-- 课时元信息的 canonical 模型(ADR-0008)。`authors` 是有序列表:多人署名第一类,
+    空列表 = 未署名。`title` 等其余字段是 passthrough 元数据,不在此承诺更多。这是系统
+    其余部分唯一所见的形态——author 在此已是列表,不再是"字符串或数组"。 -/
 structure Info where
   /-- 标题(passthrough 元数据)。 -/
   title : String
-  /-- 作者**有序列表**(空 = 未署名)。canonical 始终是列表。 -/
+  /-- 作者有序列表(空 = 未署名)。canonical 始终是列表。 -/
   authors : List String
 
-/-- 撰写态的 `[info]`(`PINNED` 仅填写便利, ADR-0008)。`author` 用 `RawAuthor`
-(字符串或数组),`author` 缺省即未署名。此结构刻画"为便于填写而存在的 raw 形态",
-**不**是模型其余部分流通的形式——它经 `RawInfo.toInfo` 归一化为 canonical `Info`。 -/
+/-- 撰写态的 `[info]`(ADR-0008)。`author` 用 `RawAuthor`(字符串或数组),缺省即未署名。
+    此结构刻画"为便于填写而存在的 raw 形态",不是模型其余部分流通的形式——它经
+    `RawInfo.toInfo` 归一化为 canonical `Info`。 -/
 structure RawInfo where
   /-- 标题。 -/
   title : String
   /-- 作者 raw 形式(可选;缺省即未署名)。 -/
   author : Option RawAuthor
 
-/-- raw `[info]` 归一化为 canonical `Info`(`PINNED` 加载边界归一化, ADR-0008)。缺省
-author ⇒ 空列表,否则按 `RawAuthor.normalize`。raw 的"字符串或数组"二态在此被消解,
-**不**泄漏进 `Info`——canonical 接收端恒为 `List String`。 -/
+/-- raw `[info]` 归一化为 canonical `Info`(ADR-0008)。缺省 author ⇒ 空列表,否则按
+    `RawAuthor.normalize`。raw 的"字符串或数组"二态在此被消解,不泄漏进 `Info`——
+    canonical 接收端恒为 `List String`。 -/
 def RawInfo.toInfo (r : RawInfo) : Info :=
   { title := r.title
     authors := (r.author.map RawAuthor.normalize).getD [] }

spec/Spec/Courseware/Model/Lesson.lean

@@ -3,14 +3,14 @@ import Spec.Courseware.Model.Element
 /-!
 # Lesson —— 单节课工程文件
 
-ADR-0005:一个工程文件 = 一节课,是 element 实例的**有序序列**。课程/单元不是工程
-文件,而是 lesson 的编排(见 `Spec.Courseware.Course`,OPEN)。
+一个工程文件 = 一节课,是 element 实例的有序序列(ADR-0005)。课程、单元不是工程文件,
+而是 lesson 的编排(见 `Spec.Courseware.Course`,OPEN)。
 -/
 
 namespace Spec.Courseware
 
-/-- 一节课(`PINNED`, ADR-0005)。用 `List` 因为 **element 次序承载教学语义**(先讲
-定义再举例 ≠ 反过来);**不建模时长**——ADR-0005 决定 lesson 是内容编排而非时间轴。 -/
+/-- 一节课(ADR-0005)。用 `List` 因为 element 的次序承载教学语义(先讲定义再举例, ≠ 反过来)。
+    不建模时长——lesson 是内容编排,不是时间轴(ADR-0005)。 -/
 abbrev Lesson (P : Primitives) := List (Element P)
 
 end Spec.Courseware

spec/Spec/Courseware/Model/Primitives.lean

@@ -1,34 +1,26 @@
 /-!
-# Primitives —— Courseware 契约的留白基元
+# 基元
 
-课程工程文件模型(ADR-0005)依赖一组基元:element kind 怎么标识、某 kind 的数据
-schema 是什么、export target 怎么标识。收口成载体 `Primitives`,让模型在其上参数化
-——契约谈得了 element / lesson / 渲染**之间的关系**,而把每个基元的**内部表示**留给
-实现。注意:某基元语义已 PINNED(如 schema 形态由 ADR-0006 钉死)与其表示进 Lean
-是两回事——JSON Schema / typst 的内部结构属实现细节,不入 Lean,故基元在此仍以抽象
-类型承载。富内容的 prose 母本见 `Courseware.RichContent`。
+课程模型要谈"element、lesson、target 之间的关系",但每个基元本身(element kind
+怎么标识、kind 的数据 schema 长什么样、target 怎么标识)的内部表示是实现的事。
+这里把它们收成一组抽象基元,让模型在它们之上参数化。
+
+契约只钉基元之间的关系;基元内部用什么表示,留给实现。
 -/
 
 namespace Spec.Courseware
 
-/-- Courseware 契约基元载体(关系 `PINNED`, ADR-0005;各基元表示留给实现, ADR-0006)。 -/
+/-- 课程模型的一组抽象基元:关系已定,内部表示留给实现(ADR-0005、ADR-0006)。 -/
 structure Primitives where
-  /-- element kind 标识(`PINNED` **开放宇宙**, ADR-0005;表示 `OPEN`)。刻意用抽象
-      类型而非 `inductive`:ADR-0005 决定 kind 是开放可扩展宇宙(stdlib + 第三方),
-      封闭枚举会违背它——此处开放是**已决策的**(区别于 `RunState` 的"尚未封闭")。 -/
+  /-- element kind 的标识。kind 是开放宇宙:stdlib 加第三方都可加,不是封闭枚举
+      (ADR-0005)。表示方式留给实现。 -/
   KindId : Type
-  /-- 某 kind 的合法数据类型(`PINNED` 依赖关系, ADR-0005;schema 形态 `PINNED`
-      ADR-0006,表示仍抽象)。以 kind 为索引:`ElementData k` 即"符合 `k` schema 的
-      数据"。schema 形态(声明式 JSON Schema + `content` 叶子 = typst 源)是 ADR-0006
-      钉死的,但属 JSON/typst 内部结构、实现细节,不进 Lean;契约只锚定"数据符合
-      kind schema"这条关系,故此处仍是抽象类型。 -/
+  /-- 某 kind 的合法数据类型,以 kind 为索引:`ElementData k` 就是"符合 k 的 schema
+      的数据"。schema 用声明式 JSON Schema,带 content 叶子(ADR-0006);JSON Schema
+      的内部结构是实现细节,不进契约,契约只钉"数据要符合 kind 的 schema"这条关系。 -/
   ElementData : KindId → Type
-  /-- export target 标识(`PINNED` 角色, ADR-0005;表示 `OPEN`)。一个 target 是一次
-      build,产出对 lesson 的一种投影(讲义/教案/PPT/平台 archive…),见 `Render`。 -/
+  /-- export target 的标识。一个 target 是一次 build,产出对 lesson 的一种投影
+      (讲义、教案、PPT、平台归档等),见 Render。 -/
   TargetId : Type
 
--- 注:原 `RenderRule : Type` 已随 ADR-0011 移除。渲染的"how"不再是契约层 per-target
--- 载荷,而由 `Render.TargetSpec.steps` 里 `typstCompile` step 引用的**模板文件**承载;
--- 契约只保留覆盖声明 `TargetSpec.covers`(该 target 渲染哪些 kind),供种子诊断用。
-
 end Spec.Courseware

spec/Spec/Courseware/Model/RichContent.lean

@@ -1,44 +1,41 @@
 /-!
-# RichContent —— 富内容(ADR-0006 的 prose 母本)
+# 富内容
 
-ADR-0006:element schema 的"叶子"可以是 `content` 类型,其值是一段**源文本**,
-按其 **format** 决定语义(ADR-0015)。两种 format:
-- **typst** —— 一段 typst 源,语义取该源作为 module 求值后的 body content(讲义/教案面)。
-- **markdown** —— 一段**原样**的 markdown + KaTeX 源,**不经 typst 求值**(slides 大纲面 / 逐字稿口播面;
-  ADR-0015)。直接以 markdown 撰写**绕开** typst→markdown 的公式转换难题(ADR-0014 R2):公式一开始就是
-  KaTeX 源(`$…$`),没有"把 typst 公式转成 md"这一步。
+element schema 的叶子可以是 content 类型:一段源文本,按 format 决定语义
+(ADR-0006、ADR-0015)。
 
-关键约束(均 ADR-0006,源自 typst 源码事实):**typst** format 的富内容**不可无主**——typst 的源必须有
-`FileId`,否则 span 脱锚、相对 import 报"cannot access file system from here"。故每段 typst 富内容是 World 里
-的一等文件,坐落在一个**虚拟路径**上;相对 import 限本工程路径结构内 + `@package`(不跨工程)。markdown format
-的富内容不参与 typst 求值,但同样由一个虚拟路径定位(供 markdown 装配 step 按序读取,见 `Export/Render`)。
+两种 format:
 
-本模块只立 prose 锚点 + 最小抽象签名:typst 的 `Content`/`Module` 内部结构、JSON Schema 形状、format 的
-具体判别属实现细节,不进 Lean,只承诺"富内容由一个虚拟路径定位"+"叶子带 format"这两条关系。
+- typst:一段 typst 源,求值后得到讲义/教案用的内容。
+- markdown:一段 markdown + KaTeX 源,原样保留,不经 typst 求值(slides 大纲、
+  逐字稿口播)。直接用 markdown 写,公式一开始就是 KaTeX(`$…$`),绕开了
+  typst→markdown 的公式转换这个难题(ADR-0014)。
+
+约束:typst 内容必须挂在一个虚拟路径上(原因见 ADR-0006 的考据)。markdown 内容
+不经 typst 求值,但同样用虚拟路径定位,供 markdown 装配按序读取。
+
+本模块只钉两条关系:富内容由一个虚拟路径定位、叶子带 format。typst 的 Content/Module
+内部结构、JSON Schema 形状、format 怎么判别,都是实现细节,不进契约。
 -/
 
 namespace Spec.Courseware
 
-/-- 富内容在工程文件路径结构中的**虚拟路径**(`OPEN` 表示, ADR-0006)。把一段富内容
-定位为 World 里的一等文件(span 可解析、相对 import 可锚定)。落盘后即真实相对路径
-(ADR-0007),不在本层承诺,故 opaque。 -/
+/-- 富内容在工程文件里的虚拟路径(ADR-0006)。落盘后是真实相对路径(ADR-0007),
+    这层不承诺,所以 opaque。 -/
 opaque VPath : Type
 
-/-- 富内容的 **format**(`PINNED`, ADR-0015)。`content` 叶子带 format:typst 叶子被 typst 求值;
-markdown 叶子原样保留(markdown+KaTeX 源,不经求值)。 -/
+/-- 富内容的 format(ADR-0015)。 -/
 inductive ContentFormat where
-  /-- typst 源:求值为 typst `Content`(讲义/教案面)。 -/
+  /-- typst 源:求值后得到讲义/教案用的内容。 -/
   | typst
-  /-- markdown + KaTeX 源:原样保留,不经 typst 求值(slides 大纲面 / 逐字稿口播面;ADR-0015)。 -/
+  /-- markdown + KaTeX 源:原样保留,不经 typst 求值(slides、逐字稿)。 -/
   | markdown
 
-/-- 对一段富内容的**引用**:它坐落在某个虚拟路径上(`PINNED` 关系, ADR-0006),并带一个
-**format**(`PINNED`, ADR-0015)。刻意**不**建模源文本、不建模求值出的 `Content`(那是实现侧的事);
-只钉"富内容经由一个 `VPath` 定位 + 带 format",作为 `Primitives.ElementData` 里 `content` 叶子的语义锚点。 -/
+/-- 对一段富内容的引用:它挂在一个虚拟路径上(ADR-0006),带一个 format(ADR-0015)。
+    不建模源文本,也不建模求值出的内容——那是实现的事;这里只钉"富内容由虚拟路径定位
+    + 带 format",作为 ElementData 里 content 叶子的语义锚点。 -/
 structure RichContentRef where
-  /-- 该富内容所在的虚拟路径(ADR-0006;落盘后为真实相对路径, ADR-0007)。 -/
   vpath : VPath
-  /-- 该富内容的 format(ADR-0015)。 -/
   format : ContentFormat
 
 end Spec.Courseware

spec/Spec/Courseware/Open.lean

@@ -2,8 +2,8 @@ import Spec.Courseware.Open.QuestionBank
 import Spec.Courseware.Open.Course
 
 /-!
-# Courseware.Open —— 留白骨架(核心关系 OPEN)
+# Courseware.Open —— 留白骨架
 
-题库与 element 的关系(`QuestionBank`)、课程编排规则(`Course`)。两者均为已 surface
-但未决策的分歧点,按宪法第 2 条不臆造,待专门 ADR 落定。
+题库与 element 的关系(`QuestionBank`)、课程编排规则(`Course`)。两者都是已提出但
+未决策的分歧点,不臆造,待专门 ADR 落定。
 -/

spec/Spec/Courseware/Open/Course.lean

@@ -1,10 +1,10 @@
 /-!
-# Course —— 课程编排(骨架,规则 OPEN)
+# Course —— 课程编排(OPEN)
 
-ADR-0005:工程文件的粒度是**单节课**;course / 单元**不是**工程文件,而是 lesson 的
-**编排**。但"编排"的具体规则未决策:有序列表还是带层级(单元 → 课)的树?lesson 被
-引用还是被包含?跨 lesson 有无约束(目标覆盖、前后置)?这些都是 `OPEN`。
+工程文件的粒度是单节课(ADR-0005);course / 单元不是工程文件,而是 lesson 的编排。
+但"编排"的具体规则没定:有序列表,还是带层级(单元 → 课)的树?lesson 被引用还是被
+包含?跨 lesson 有无约束(目标覆盖、前后置)?这些都 OPEN。
 
-按宪法第 2 条本模块**不臆造**编排结构——不建 `Course := List Lesson`(那会偷偷承诺
-"扁平有序、无层级")。只在此 surface:课程编排待专门 ADR。本文件当前不引入任何承诺性声明。
+不臆造编排结构——不建 `Course := List Lesson`(那会偷偷承诺"扁平有序、无层级")。课程
+编排待专门 ADR。本文件不引入任何承诺性声明。
 -/

spec/Spec/Courseware/Open/QuestionBank.lean

@@ -1,10 +1,10 @@
 /-!
-# QuestionBank —— 题库(骨架,核心关系 OPEN)
+# QuestionBank —— 题库(OPEN)
 
-题库是与工程文件并列的资产(类比 DAW 的 sample library):有自身结构的实体,又是最
-典型的可复用单元,lesson 会引用它。但**题库与 element 的关系尚未决策**,且用户明确
-指出"纯引用可能不够"——element 内联题目数据 / lesson 持指向题库条目的引用 / 两者并存?
+题库是与工程文件并列的资产:有自身结构的实体,又是最典型的可复用单元,lesson 会引用它。
+但题库与 element 的关系没定,用户也指出"纯引用可能不够"——element 内联题目数据?lesson
+持指向题库条目的引用?两者并存?
 
-这是一个 `OPEN` 分歧点。按宪法第 2 条本模块**不替它选解**——不建 `QuestionRef` 也不建
-内联结构,只在此 surface。待专门 ADR 落定后再填。本文件当前不引入任何承诺性声明。
+这是 OPEN 分歧点。不替它选解——不建 `QuestionRef` 也不建内联结构,只在此提出。待专门
+ADR 落定后再填。本文件不引入任何承诺性声明。
 -/

spec/Spec/Prelude.lean

@@ -1,24 +1,23 @@
 /-!
 # Prelude —— System 层共享标识符
 
-平台层反复引用一组标识符(项目、run、session、principal)。其内部表示从未被决策
-(UUID / 复合键、principal 子类型学),也非分歧点,故收口成 opaque 载体
-`Identifiers`,System 各模块在其上参数化——契约谈得了"锁 owner 是哪个 run"这类
-**关系**,却不对标识符表示作承诺。
+平台层反复引用一组标识符(项目、run、session、principal)。它们的内部表示从未被决策
+(UUID / 复合键、principal 的子类型学),也不是分歧点,所以收成 opaque 载体
+`Identifiers`,System 各模块在它之上参数化——契约谈得了"锁 owner 是哪个 run"这类关系,
+不对标识符表示作承诺。
 -/
 
 namespace Spec.System
 
-/-- System 层标识符载体(关系结构 `PINNED`;各字段表示 `OPEN`)。 -/
+/-- System 层标识符载体:关系已定,各字段表示 OPEN。 -/
 structure Identifiers where
-  /-- 课程项目标识(`OPEN` 表示;聚合根,likec4 `Project`)。 -/
+  /-- 课程项目标识(聚合根;表示 OPEN)。 -/
   ProjectId : Type
-  /-- 一次 Claude 任务的标识(`OPEN` 表示;锁的 owner、审计主体,`AgentRun`)。 -/
+  /-- 一次 Claude 任务的标识(锁的 owner、审计主体;表示 OPEN)。 -/
   RunId : Type
-  /-- 长生命周期 Claude 会话标识(`OPEN` 表示;跨多 run 复用,ADR-0002)。 -/
+  /-- 长生命周期 Claude 会话标识(跨多 run 复用,ADR-0002;表示 OPEN)。 -/
   SessionId : Type
-  /-- 权限主体标识(`OPEN` 表示及其子类型学;ADR-0004 的 user/chat/department/…
-      子类型学未定且非本层分歧点,纯 plumbing,故只留 opaque 键)。 -/
+  /-- 权限主体标识(表示 OPEN)。 -/
   Principal : Type
 
 end Spec.System

spec/Spec/System.lean

@@ -1,19 +1,21 @@
 import Spec.System.Run
 import Spec.System.Lock
 import Spec.System.Permission
-import Spec.System.Audit
 
 /-!
 # System —— Hub 平台层契约
 
-协作与执行的平台:项目、飞书群、AgentRun、锁、权限、审计。likec4
-(`docs/architecture/likec4/`)已画出这一层的**结构**;本层只补 likec4 画不出的
-**语义分歧点**:
+这一层是产品里的协作与执行平台:项目、飞书群、AgentRun、锁、权限、审计。决策出处
+ADR-0001..0004。
 
-- `Run` —— AgentRun 状态与终止判定(状态集合完整性 OPEN)。
+现状:Hub 还没建、没有业务反馈,所以这一层多为 OPEN 占位,只钉少数已定且有语义分量的
+东西(锁 owner = run、持锁者必为非终止 run、角色三级)。其余等 Hub 真建起来、业务反馈
+来了再细化。做 SaaS 要的权限、LLM API 配置和用量、费用等管理概念,将来也落在这层。
+
+- `Run` —— AgentRun 的终止判定(状态集合 OPEN)。
 - `Lock` —— 锁 owner = run(ADR-0002),及"持锁者必为非终止 run"的核心不变式。
-- `Permission` —— read⊂edit⊂manage 角色格、能力推导、单调性;force-release 在格外。
-- `Audit` —— 有意从简(内容多为 plumbing,OPEN)。
+- `Permission` —— read ⊂ edit ⊂ manage 角色三级;force-release 在格外。
+- 审计以 run 为主体记录其生命周期事件;审计记录里装什么未定(OPEN)。
 
-标识符见 `Spec.Prelude`。决策出处:ADR-0001..0004。
+标识符见 `Spec.Prelude`。
 -/

spec/Spec/System/Audit.lean

@@ -1,22 +0,0 @@
-import Spec.Prelude
-
-/-!
-# Audit —— 审计日志(有意从简)
-
-likec4 把 `AuditLog` 列为实体(`AgentRun -> AuditLog 'records lifecycle events'`),
-但**审计记录里装什么**(事件 schema、保留策略、可查询维度)在任何 ADR / 散文里都
-未决策,且大多是 plumbing——按分歧点测试不入契约。故本模块刻意几乎为空:只固定
-"审计以 run 为主体记录其生命周期事件"这一条已决策关系,其余 `OPEN`(留白本身是
-契约的一部分:承诺此处尚无答案、勿填)。
--/
-
-namespace Spec.System
-
-/-- 审计条目的最小骨架(关系 `PINNED` / 内容 `OPEN`, likec4)。只承诺"一条审计记录
-关联到某个 run";事件类型、时间、actor、详情等字段 `OPEN`,待真实分歧点出现时由
-对应 ADR 落定。 -/
-structure AuditEntry (I : Identifiers) where
-  /-- 该审计条目所属的 run(`PINNED` 关系, likec4)。 -/
-  run : I.RunId
-
-end Spec.System

spec/Spec/System/Lock.lean

@@ -4,34 +4,29 @@ import Spec.System.Run
 /-!
 # Lock —— 项目锁与排他不变式
 
-ADR-0002 的核心:防止并发 Claude 同改一个项目,锁的 **owner 是当前 `AgentRun`**
-(不是 teacher / chat / session)。本模块把这条决策编码进类型,并钉死那条
-likec4 画不出的语义不变式——**持锁者必为非终止 run**。
+ADR-0002 的核心:防止并发 Claude 同改一个项目,锁的 owner 是当前 AgentRun(不是
+teacher / chat / session)。这条编码进类型,并钉住核心不变式:持锁者必为非终止 run。
 -/
 
 namespace Spec.System
 
 variable (I : Identifiers)
 
-/-- 项目级锁(`PINNED`, ADR-0002)。`owner : RunId`(非 SessionId/Principal)从类型
-上编码"lock owner = run_id":锁不可能被 session / teacher 持有。 -/
+/-- 项目级锁(ADR-0002)。`owner : RunId`(非 SessionId/Principal)从类型上编码
+    "lock owner = run":锁不可能被 session / teacher 持有。 -/
 structure ProjectAgentLock where
-  /-- 作用域:项目级(`PINNED`, ADR-0002 `scope = project_id`)。 -/
+  /-- 作用域:项目级(ADR-0002)。 -/
   scope : I.ProjectId
-  /-- 持有者:一个 run(`PINNED`, ADR-0002 `owner = run_id`)。 -/
+  /-- 持有者:一个 run(ADR-0002)。 -/
   owner : I.RunId
 
-/-- 锁表:每项目当前持锁 run(`PINNED` 排他性, ADR-0002)。`ProjectId → Option RunId`
-的结构**本身**即排他——不可能为同一项目登记两个并发 owner。 -/
+/-- 锁表:每项目当前持锁 run(ADR-0002 排他性)。`ProjectId → Option RunId` 的结构本身
+    即排他——不可能为同一项目登记两个并发 owner。 -/
 def LockTable := I.ProjectId → Option I.RunId
 
-/-- 锁表良构:**持锁者必为非终止 run**(`PINNED` 平台核心不变式, ADR-0002)。
-
-"锁在 run 终止时释放"的逻辑等价物:若 `p` 的锁被 `r` 持有,则 `r` 不在终止态。这条
-把 Lock 与 Run 耦合起来——likec4 能画"run owns lock while running",画不出"终止即
-必须释放"这个约束;它正是契约相对结构图的增量。 -/
-def LockTable.WellFormed
-    (lt : LockTable I) (statusOf : I.RunId → RunState) : Prop :=
-  ∀ p r, lt p = some r → ¬ (statusOf r).Terminal
+/-- 锁表良构:持锁者必为非终止 run(ADR-0002 核心不变式)。"锁在 run 终止时释放"
+    的等价物:若 `p` 的锁被 `r` 持有,则 `r` 不在终止态。 -/
+def LockTable.WellFormed (lt : LockTable I) : Prop :=
+  ∀ p r, lt p = some r → ¬ Terminal I r
 
 end Spec.System

spec/Spec/System/Permission.lean

@@ -1,66 +1,23 @@
 import Spec.Prelude
 
 /-!
-# Permission —— 角色、能力与授权
+# Permission —— 协作者角色
 
-ADR-0004:权限走"飞书云文档式"——grant(`resource + principal + role`)与 settings
-分离;role 取自封闭的 `read / edit / manage`,且 **read ⊂ edit ⊂ manage** 累积赋能;
-强制释放锁是 **admin-only**,在 role 体系之外。本模块把这套结构与"高 role 含低
-role 全部能力"的单调性钉死。
+ADR-0004:权限走"飞书云文档式"——grant(resource + principal + role)与 settings 分离;
+role 取自封闭的 read / edit / manage,且 read ⊂ edit ⊂ manage 累积赋能;强制释放锁是
+admin-only,在 role 体系之外。
+
+本模块钉角色三级与累积关系。具体哪些操作归哪级,见 ADR-0004,待业务反馈细化——所以这里
+不钉操作枚举,也不钉"哪个能力要求哪个 role"的映射。
 -/
 
 namespace Spec.System
 
-/-- 协作者角色(`PINNED` 封闭, ADR-0004 逐字 "roles are read, edit, or manage")。 -/
+/-- 协作者角色(ADR-0004:read / edit / manage)。read ⊂ edit ⊂ manage,高 role 含低 role
+    全部能力。强制释放锁不在这套体系里,是 admin-only override,由平台另行判定。 -/
 inductive Role where
   | read
   | edit
   | manage
 
-/-- 角色赋能层级(`PINNED` 序, ADR-0004 read⊂edit⊂manage 数值化)。仅服务于
-`Role.le` 与能力推导,不对外承诺"层级就是 `Nat`"。 -/
-def Role.level : Role → Nat
-  | .read => 0
-  | .edit => 1
-  | .manage => 2
-
-/-- 角色偏序:`r₁ ≤ r₂` 即 `r₁` 赋能不强于 `r₂`(`PINNED`, ADR-0004)。 -/
-def Role.le (r₁ r₂ : Role) : Prop := r₁.level ≤ r₂.level
-
-/-- 受 role 调控的操作能力(各项 `PINNED` 取自 ADR-0004;**枚举完整性 `OPEN`**——
-这是 ADR 当前点名的能力,不保证穷尽,新增产品操作时可能扩)。注意 force-release
-**不在此列**——它是 admin-only override,见 `RequiresAdmin`。 -/
-inductive Capability where
-  | view
-  | discussComment
-  | editArtifact
-  | triggerAgent
-  | answerChoiceCard
-  | manageCollaborators
-  | projectSettings
-  | groupBinding
-  | normalCancel
-
-/-- 某能力所**要求的最低角色**(`PINNED`, ADR-0004 各 role 能力展开)。授权判定
-`Role.can` 据此定义,"谁能做什么"只有这一处真相。 -/
-def Capability.requiredRole : Capability → Role
-  | .view => .read
-  | .discussComment | .editArtifact | .triggerAgent | .answerChoiceCard => .edit
-  | .manageCollaborators | .projectSettings | .groupBinding | .normalCancel => .manage
-
-/-- 角色 `r` **具备**能力 `c`(`PINNED`, ADR-0004)。定义为"`c` 的最低角色 ≤ `r`",
-这一处同时编码了 read⊂edit⊂manage 的累积性。 -/
-def Role.can (r : Role) (c : Capability) : Prop := c.requiredRole |>.le r
-
-/-- **单调性**:`r₁ ≤ r₂` 且 `r₁` 能做 `c` ⇒ `r₂` 也能(`PINNED` 定理, ADR-0004 累积
-赋能的形式化保证)。证明即偏序传递性,得益于 `can` 按"最低角色阈值"定义。 -/
-theorem Role.can_mono {r₁ r₂ : Role} {c : Capability}
-    (h : r₁.le r₂) (hc : r₁.can c) : r₂.can c :=
-  Nat.le_trans hc h
-
-/-- **强制释放锁**要求 admin,**在 role 体系之外**(`PINNED`, ADR-0004 admin-only
-override)。即便 `manage` 也不经 `Role.can` 获得它,故它不是 `Capability` 而是独立
-谓词;`isAdmin` 由平台另行判定(本层不建 admin 模型)。 -/
-def RequiresAdmin (isAdmin : Prop) : Prop := isAdmin
-
 end Spec.System

spec/Spec/System/Run.lean

@@ -1,28 +1,22 @@
-/-!
-# Run —— AgentRun 状态机
+import Spec.Prelude
 
-一次 `@Claude` 创建一个 `AgentRun`(ADR-0001),它在终止时释放项目锁(ADR-0002)。
-合法转移关系在任何 ADR / likec4 散文里都未定下,故本模块只刻画**状态**与**终止
-判定**(后者是 Lock 排他不变式的依赖),不臆造转移边。
+/-!
+# Run —— AgentRun 的终止判定
+
+一次 `@Claude` 创建一个 AgentRun(ADR-0001),它在终止时释放项目锁(ADR-0002)。
+
+run 的具体状态集合没定(OPEN):ADR-0001..0003 列了一些状态名,但从未声明"状态恰好
+这些",实现若需新状态(如 pending)要提出来,不要默认已穷尽。所以这里不钉状态枚举,
+只钉一条契约需要的事实:一个 run 是否处于终止态。终止态由实现判定(状态集合本身未定,
+没法在契约里算)。
 -/
 
 namespace Spec.System
 
-/-- AgentRun 运行状态(状态名 `PINNED`, ADR-0001..0003 + likec4;**完整性 `OPEN`**
-——散文从未声明"状态恰好这些";实现若需新状态(如 pending)须 surface,不得默认
-本枚举已穷尽)。终止态见 `RunState.Terminal`。 -/
-inductive RunState where
-  | active
-  | waitingForUser
-  | completed
-  | failed
-  | timedOut
-  | canceled
+variable (I : Identifiers)
 
-/-- run 处于**终止态**(`PINNED`, ADR-0002:锁在 completes/fails/timesOut/canceled
-时释放)。`active`/`waitingForUser` 非终止——后者仍占用项目(锁未释放)。 -/
-def RunState.Terminal : RunState → Prop
-  | .completed | .failed | .timedOut | .canceled => True
-  | .active | .waitingForUser => False
+/-- run 是否处于终止态(ADR-0002)。真值由实现给——状态集合未定(OPEN),故此处不钉
+    具体状态名,只钉"存在终止与否的判定"。锁在 run 终止时释放(见 `Lock`)。 -/
+opaque Terminal : I.RunId → Prop
 
 end Spec.System