m0-04-product-deps

name	M0-04-product-deps
description	模块 0 构建 project_deps.json（文档级依赖图）时加载。涵盖两类边（statement_deps/proof_refs）的分段规则、两类连边依据（显式引用+结构性依赖）、dangling 三类处理、环的处理原则。

产物：project_deps.json

用途

记录 md 间直接依赖邻接表。模块 0 只产结构（节点+边+dangling），前台做拓扑排序、环检测、forward 回填。

两类边

边	引用所在段	下游用途
statement_deps	## Statement	陈述层拓扑排序 + import
proof_refs	## Proof	证明阶段 import 定位，不排序

引用/依赖落在哪个段就分入哪个字段——机械判断，看引用在 ## Statement 还是 ## Proof。

连边依据

(i) 显式引用

正文写了 "by Lemma 3.1" → 查 global_name_index.json（编号→id）→ 连边。

(ii) 结构性依赖

本块用到某上游 md 引入的符号/概念（如定理陈述用了极限符号 →、或用了"超距离空间"这个概念），即使没写 "by 定义 X" → 顺流水线往前判断：这个符号/概念是前面哪个 md 引入的，找到就连、找不到就不管交下游。

不由你判断"什么是基础符号/约定俗成"——论文里什么算基础太主观，你判不了也不该判。下游 agent 有数学知识，自然知道。

dangling

连不上的引用挂 dangling，带 ref（原文字面）/ type / status：

type	含义	处理
forward	编号明确但目标在后面还没处理	全书扫完后前台回填
vague	模糊回指（"by the above"），agent 尽力判断仍无法确定	留 dangling，下游形式化时 Lean 自然暴露缺依赖
external	指向系统外文献（"[4, Theorem 2.1]"）	不连边，标 external 交下游

字段

thm_00012:
  statement_deps: ["def_00007"]
  proof_refs: ["lem_00003"]
  dangling: []
thm_00015:
  statement_deps: []
  proof_refs: ["thm_00012"]
  dangling:
    - { ref: "定理 4.2", type: "forward", status: "unresolved" }
    - { ref: "combining the above", type: "vague", status: "unresolved" }
    - { ref: "[4, Theorem 2.1]", type: "external", status: "external" }

每个 md 在 deps 里有一个节点，即使没有任何边。

环

如实连边，不管环、不缩图、不删边。前台拓扑排序检测到环 → 上报。