deeplethe · WaylandYang · Sep 3, 2026 · Sep 3, 2026
diff --git a/crates/utopia-core/src/models.rs b/crates/utopia-core/src/models.rs
@@ -513,6 +513,13 @@ pub struct GraphEdge {
     pub valid_from: Option<DateTime<Utc>>,
     pub valid_to: Option<DateTime<Utc>>,
     pub confidence: f32,
+    /// 有争议（0017 §3）：有一条 open 的公理违规或时态冲突指着它。整条边画成
+    /// 警戒色——环在节点上、边还是灰的，余光分不出来
+    pub contested: bool,
+    /// 幽灵边（0017 §3）：一条**没有落地**的派生——推出来了却撞上断言。`id` 是那条
+    /// `derived_contradiction` 违规的 id，不是任何事实；`derived` 同时为 true，
+    /// 所以它跟着派生开关走
+    pub blocked: bool,
 }
 
 /// 实体详情页的事实行（时间线）。
@@ -549,6 +556,10 @@ pub struct EntityFact {
     pub corrected: bool,
     /// 证据集合里最新的文档时间——开放事实的"最后确认时间"（时效性透明化）
     pub last_evidence_time: Option<DateTime<Utc>>,
+    /// 有争议（0017 §3）：`{ kind, ref_id, derived? }`——哪一种（违规的 kind，或
+    /// `temporal_conflict`）、Review 里那一项的 id、派生撞断言时推出来的那句话。
+    /// 一条只报最新的一处；行**不压暗**，断言仍然活着
+    pub contested: Option<serde_json::Value>,
 }
 
 /// 实体的一次认知变更（记录时间轴上的事件，与 EntityFact 的有效时间轴正交）。
@@ -933,6 +944,30 @@ pub struct DerivedFactView {
     pub premises: Vec<String>,
 }
 
+/// 一条**没有落地**的派生（0017 §3）：推出来了，撞上一条断言，拦在图外。
+///
+/// 它没有 id——落库的才有。这里用那条 `derived_contradiction` 违规的 id 指它，
+/// 面板上的「没落地的」一档与图上的幽灵边都靠这个 id 对上 Review 里的卡片。
+#[derive(Debug, Clone, Serialize, sqlx::FromRow)]
+pub struct BlockedDerivation {
+    pub violation_id: Uuid,
+    pub subject_id: Uuid,
+    pub subject: String,
+    pub object_id: Uuid,
+    pub object: String,
+    pub predicate: String,
+    pub rule: String,
+    /// 声明所在的谓词
+    pub via_label: String,
+    pub valid_from: Option<DateTime<Utc>>,
+    pub valid_to: Option<DateTime<Utc>>,
+    /// 挡住它的那条断言，与它的三元组文本
+    pub against_fact: Uuid,
+    pub against_text: String,
+    /// 前提事实 id，按推导顺序——证明链从这里展开
+    pub premises: Vec<Uuid>,
+}
+
 /// 证明的一步：一条断言前提，连同它的证据（0002 R2）。
 ///
 /// 前提一律是断言（`fact_derivations` 不记派生），所以证明是一条链而不是一棵树：

diff --git a/crates/utopia-server/src/api/graph_routes.rs b/crates/utopia-server/src/api/graph_routes.rs
@@ -145,9 +145,12 @@ pub async fn entity_detail(
     // 只有先改一次名才够得着——而两个张伟并存是「宁分勿合」的正当产物，不是
     // 改名改出来的。合并入口该长在能看见同名的地方。
     let same_name = utopia_store::graph::same_name_peers(&state.pool, kb_id, entity_id).await?;
+    // 没落地的派生（0017 §3）也单独一个键：它们连 `derived_facts` 都不在
+    let blocked =
+        utopia_store::reasoning::blocked_for_entity(&state.pool, kb_id, entity_id).await?;
     Ok(Json(json!({
         "entity": entity, "facts": facts,
-        "derived": derived, "same_name": same_name,
+        "derived": derived, "blocked": blocked, "same_name": same_name,
     })))
 }
 
@@ -240,6 +243,18 @@ pub async fn derived_proof(
     Ok(Json(json!({ "proof": proof })))
 }
 
+/// 没落地的派生的证明链（0017 §3）：前提在那条 `derived_contradiction` 违规的
+/// `path` 里，展开方式与落了地的一样。违规不存在时 `steps` 为 null
+pub async fn blocked_proof(
+    State(state): State<AppState>,
+    AuthUser(user): AuthUser,
+    Path((kb_id, violation_id)): Path<(Uuid, Uuid)>,
+) -> ApiResult<Json<serde_json::Value>> {
+    require_kb(&state, &user, kb_id, Role::Viewer).await?;
+    let steps = utopia_store::reasoning::blocked_proof(&state.pool, kb_id, violation_id).await?;
+    Ok(Json(json!({ "steps": steps })))
+}
+
 /// 手动触发抽取（failed 重试 / 补配模型后补抽）。
 pub async fn extract(
     State(state): State<AppState>,

diff --git a/crates/utopia-server/src/api/mod.rs b/crates/utopia-server/src/api/mod.rs
@@ -295,6 +295,11 @@ pub fn router(state: AppState, cfg: &AppConfig) -> Router {
             "/kbs/{id}/derived/{derived_id}/proof",
             get(graph_routes::derived_proof),
         )
+        // 没落地的派生的证明（0017 §3）：前提在违规的 path 里
+        .route(
+            "/kbs/{id}/violations/{violation_id}/proof",
+            get(graph_routes::blocked_proof),
+        )
         .route("/kbs/{id}/events", get(events_routes::kb_events))
         .route(
             "/kbs/{id}/sources",

diff --git a/crates/utopia-store/src/graph.rs b/crates/utopia-store/src/graph.rs
@@ -418,13 +418,29 @@ async fn edges_among(
     //
     // 图要它们，因为「这条边是推出来的」正是用户该看见的信息之一；`derived`
     // 那一位让界面画得出区别，也让人整体过滤掉。
+    //
+    // 第三段是**幽灵边**（0017 §3）：推出来却没落地的派生，住在 `axiom_violations`
+    // 的 `detail` 里。它的 id 是违规的 id；`derived` 与 `blocked` 同时为 true，
+    // 界面据此让它跟着派生开关走、画成争议色往背景混的那一档。
+    //
+    // 断言那一段多算一位 `contested`：有 open 的违规或时态冲突指着它。派生撞断言
+    // 时被撞的是 left；right 只是最后一条前提，它本身没有争议
     let edges: Vec<GraphEdge> = sqlx::query_as(
         "SELECT f.id, f.subject_id AS source, f.object_id AS target,
                 COALESCE(r.key, fact_surface_predicate(f.id)) AS predicate,
                 COALESCE(r.label, fact_surface_predicate(f.id)) AS label,
                 r.id IS NULL AS inferred, FALSE AS derived, NULL::text AS rule,
                 ARRAY[]::uuid[] AS premises,
-                f.valid_from, f.valid_to, f.confidence
+                f.valid_from, f.valid_to, f.confidence,
+                (EXISTS (SELECT 1 FROM axiom_violations v
+                          WHERE v.status = 'open'
+                            AND (v.left_fact = f.id
+                                 OR (v.right_fact = f.id AND v.kind <> 'derived_contradiction')))
+                 OR EXISTS (SELECT 1 FROM fact_conflicts c
+                             WHERE c.status = 'open'
+                               AND (c.old_fact_id = f.id OR c.new_fact_id = f.id))
+                ) AS contested,
+                FALSE AS blocked
          FROM facts f LEFT JOIN relation_types r ON r.id = f.predicate_id
          WHERE f.kb_id = $1 AND f.invalidated_at IS NULL AND f.object_id IS NOT NULL
            AND f.subject_id = ANY($2) AND f.object_id = ANY($2)
@@ -437,14 +453,35 @@ async fn edges_among(
                 FALSE AS inferred, TRUE AS derived, ru.kind AS rule,
                 ARRAY(SELECT fd.premise_fact_id FROM fact_derivations fd
                        WHERE fd.derived_fact_id = d.id ORDER BY fd.seq) AS premises,
-                d.valid_from, d.valid_to, d.confidence
+                d.valid_from, d.valid_to, d.confidence,
+                FALSE AS contested, FALSE AS blocked
          FROM derived_facts d JOIN relation_types r ON r.id = d.predicate_id
                               JOIN rules ru ON ru.id = d.rule_id
          WHERE d.kb_id = $1 AND d.invalidated_at IS NULL
            AND d.subject_id = ANY($2) AND d.object_id = ANY($2)
            AND ($3::timestamptz IS NULL
                 OR ((d.valid_from IS NULL OR d.valid_from <= $3)
-                    AND (d.valid_to IS NULL OR d.valid_to > $3)))",
+                    AND (d.valid_to IS NULL OR d.valid_to > $3)))
+         UNION ALL
+         SELECT v.id,
+                (v.detail->>'subject_id')::uuid AS source,
+                (v.detail->>'object_id')::uuid AS target,
+                v.detail->>'predicate' AS predicate, v.detail->>'predicate' AS label,
+                FALSE AS inferred, TRUE AS derived, v.detail->>'rule' AS rule,
+                v.path AS premises,
+                (v.detail->>'valid_from')::timestamptz AS valid_from,
+                (v.detail->>'valid_to')::timestamptz AS valid_to,
+                0::real AS confidence,
+                TRUE AS contested, TRUE AS blocked
+         FROM axiom_violations v
+         WHERE v.kb_id = $1 AND v.kind = 'derived_contradiction' AND v.status = 'open'
+           AND (v.detail->>'subject_id')::uuid = ANY($2)
+           AND (v.detail->>'object_id')::uuid = ANY($2)
+           AND ($3::timestamptz IS NULL
+                OR (((v.detail->>'valid_from')::timestamptz IS NULL
+                     OR (v.detail->>'valid_from')::timestamptz <= $3)
+                    AND ((v.detail->>'valid_to')::timestamptz IS NULL
+                         OR (v.detail->>'valid_to')::timestamptz > $3)))",
     )
     .bind(kb_id)
     .bind(ids)
@@ -568,7 +605,25 @@ pub async fn entity_detail(
                 (f.supersedes IS NOT NULL) AS corrected,
                 (SELECT MAX(COALESCE(d.doc_time, d.created_at))
                  FROM fact_evidence fe JOIN documents d ON d.id = fe.document_id
-                 WHERE fe.fact_id = f.id) AS last_evidence_time
+                 WHERE fe.fact_id = f.id) AS last_evidence_time,
+                COALESCE(
+                    (SELECT jsonb_build_object(
+                                'kind', v.kind, 'ref_id', v.id,
+                                'derived', CASE WHEN v.kind = 'derived_contradiction'
+                                    THEN (v.detail->>'subject') || ' · '
+                                         || (v.detail->>'predicate') || ' · '
+                                         || (v.detail->>'object') END)
+                       FROM axiom_violations v
+                      WHERE v.status = 'open'
+                        AND (v.left_fact = f.id
+                             OR (v.right_fact = f.id AND v.kind <> 'derived_contradiction'))
+                      ORDER BY v.detected_at DESC LIMIT 1),
+                    (SELECT jsonb_build_object('kind', 'temporal_conflict', 'ref_id', c.id)
+                       FROM fact_conflicts c
+                      WHERE c.status = 'open'
+                        AND (c.old_fact_id = f.id OR c.new_fact_id = f.id)
+                      ORDER BY c.created_at DESC LIMIT 1)
+                ) AS contested
          FROM facts f
          LEFT JOIN relation_types r ON r.id = f.predicate_id
          LEFT JOIN entities o

diff --git a/crates/utopia-store/src/reasoning.rs b/crates/utopia-store/src/reasoning.rs
@@ -1178,9 +1178,27 @@ pub async fn proof(
     let Some(derived) = derived_one(pool, kb_id, derived_id).await? else {
         return Ok(None);
     };
+    let premises: Vec<Uuid> = sqlx::query_scalar(
+        "SELECT premise_fact_id FROM fact_derivations WHERE derived_fact_id = $1 ORDER BY seq",
+    )
+    .bind(derived_id)
+    .fetch_all(pool)
+    .await?;
+    let steps = steps_for(pool, &premises).await?;
+    Ok(Some(utopia_core::models::Proof { derived, steps }))
+}
+
+/// 一串前提展开成证明的步：三元组、区间、撤没撤、证据。
+///
+/// 落了地的派生（`fact_derivations`）与没落地的（`axiom_violations.path`）都从这里
+/// 走——前提是同一种东西，证明链没有理由长两个样
+async fn steps_for(
+    pool: &PgPool,
+    premises: &[Uuid],
+) -> AppResult<Vec<utopia_core::models::ProofStep>> {
     #[allow(clippy::type_complexity)]
     let rows: Vec<(
-        i32,
+        i64,
         Uuid,
         Uuid,
         String,
@@ -1193,19 +1211,18 @@ pub async fn proof(
         f32,
         bool,
     )> = sqlx::query_as(
-        "SELECT fd.seq, f.id, f.subject_id, s.canonical_name,
+        "SELECT x.ord - 1, f.id, f.subject_id, s.canonical_name,
                 f.predicate_id, r.label, f.object_id, o.canonical_name,
                 f.valid_from, f.valid_to, f.confidence,
                 f.invalidated_at IS NOT NULL
-           FROM fact_derivations fd
-           JOIN facts f ON f.id = fd.premise_fact_id
+           FROM unnest($1::uuid[]) WITH ORDINALITY AS x(id, ord)
+           JOIN facts f ON f.id = x.id
            JOIN entities s ON s.id = f.subject_id
            LEFT JOIN relation_types r ON r.id = f.predicate_id
            LEFT JOIN entities o ON o.id = f.object_id
-          WHERE fd.derived_fact_id = $1
-          ORDER BY fd.seq",
+          ORDER BY x.ord",
     )
-    .bind(derived_id)
+    .bind(premises)
     .fetch_all(pool)
     .await?;
     let mut steps = Vec::with_capacity(rows.len());
@@ -1227,7 +1244,7 @@ pub async fn proof(
         // 一条链最多 MAX_DEPTH 步，逐条取证据是可数的几次往返
         let evidence = crate::graph::fact_evidence(pool, fact_id).await?;
         steps.push(utopia_core::models::ProofStep {
-            seq,
+            seq: seq as i32,
             fact_id,
             subject_id,
             subject,
@@ -1242,7 +1259,65 @@ pub async fn proof(
             evidence,
         });
     }
-    Ok(Some(utopia_core::models::Proof { derived, steps }))
+    Ok(steps)
+}
+
+/// 没落地的派生里，与这个实体有关的那些（0017 §3）——面板「推出来的」一档的
+/// 「没落地的」小节。
+pub async fn blocked_for_entity(
+    pool: &PgPool,
+    kb_id: Uuid,
+    entity_id: Uuid,
+) -> AppResult<Vec<utopia_core::models::BlockedDerivation>> {
+    Ok(sqlx::query_as(
+        "SELECT v.id AS violation_id,
+                (v.detail->>'subject_id')::uuid AS subject_id,
+                COALESCE(v.detail->>'subject', '?') AS subject,
+                (v.detail->>'object_id')::uuid AS object_id,
+                COALESCE(v.detail->>'object', '?') AS object,
+                COALESCE(v.detail->>'predicate', '?') AS predicate,
+                COALESCE(v.detail->>'rule', '?') AS rule,
+                COALESCE(v.detail->>'via_label', '?') AS via_label,
+                (v.detail->>'valid_from')::timestamptz AS valid_from,
+                (v.detail->>'valid_to')::timestamptz AS valid_to,
+                v.left_fact AS against_fact,
+                s.canonical_name || ' · '
+                  || COALESCE(r.label, fact_surface_predicate(f.id), '?') || ' · '
+                  || COALESCE(o.canonical_name, '?') AS against_text,
+                v.path AS premises
+           FROM axiom_violations v
+           JOIN facts f ON f.id = v.left_fact
+           JOIN entities s ON s.id = f.subject_id
+           LEFT JOIN relation_types r ON r.id = f.predicate_id
+           LEFT JOIN entities o ON o.id = f.object_id
+          WHERE v.kb_id = $1 AND v.kind = 'derived_contradiction' AND v.status = 'open'
+            AND (v.detail->>'subject_id' = $2::text OR v.detail->>'object_id' = $2::text)
+          ORDER BY v.detected_at DESC",
+    )
+    .bind(kb_id)
+    .bind(entity_id)
+    .fetch_all(pool)
+    .await?)
+}
+
+/// 没落地的派生的证明链：它的前提就在违规的 `path` 里。找不到那条违规时 `None`
+pub async fn blocked_proof(
+    pool: &PgPool,
+    kb_id: Uuid,
+    violation_id: Uuid,
+) -> AppResult<Option<Vec<utopia_core::models::ProofStep>>> {
+    let path: Option<(Vec<Uuid>,)> = sqlx::query_as(
+        "SELECT path FROM axiom_violations
+          WHERE id = $1 AND kb_id = $2 AND kind = 'derived_contradiction'",
+    )
+    .bind(violation_id)
+    .bind(kb_id)
+    .fetch_optional(pool)
+    .await?;
+    match path {
+        None => Ok(None),
+        Some((p,)) => Ok(Some(steps_for(pool, &p).await?)),
+    }
 }
 
 /// 按 id 取一条派生（失效的也取：证明要能回看）。

diff --git a/crates/utopia-store/tests/a_contradiction_points_upstream.rs b/crates/utopia-store/tests/a_contradiction_points_upstream.rs
@@ -225,6 +225,49 @@ async fn a_contradiction_points_upstream() -> anyhow::Result<()> {
         assert_eq!(card.hint.as_deref(), Some("stale"));
         assert_eq!(card.detail["subject"], "Mira");
 
+        // 争议在它坐的地方可见（0017 §3）：面板行挂 contested，图上有一条幽灵边，
+        // 「没落地的」一档有一行，它的证明链读得出前提
+        let (_, facts) = utopia_store::graph::entity_detail(&pool, f.kb, f.mira).await?;
+        let hit = facts
+            .iter()
+            .find(|x| x.id == old)
+            .expect("the assertion is on the panel");
+        let c = hit
+            .contested
+            .as_ref()
+            .expect("the hit assertion is contested");
+        assert_eq!(c["kind"], "derived_contradiction");
+        assert_eq!(c["ref_id"], serde_json::json!(vid));
+        assert!(
+            facts
+                .iter()
+                .find(|x| x.id == ceo)
+                .unwrap()
+                .contested
+                .is_none(),
+            "the premise is not the disputed one"
+        );
+        let (_, edges) = utopia_store::graph::neighborhood(&pool, f.kb, f.mira, 1, None).await?;
+        let ghost = edges
+            .iter()
+            .find(|e| e.blocked)
+            .expect("a ghost edge for the blocked derivation");
+        assert_eq!(ghost.id, *vid);
+        assert!(ghost.derived && ghost.contested);
+        assert_eq!((ghost.source, ghost.target), (f.mira, f.acme));
+        assert!(edges.iter().find(|e| e.id == old).unwrap().contested);
+        assert!(!edges.iter().find(|e| e.id == ceo).unwrap().contested);
+        let blocked = reasoning::blocked_for_entity(&pool, f.kb, f.acme).await?;
+        assert_eq!(blocked.len(), 1);
+        assert_eq!(blocked[0].violation_id, *vid);
+        assert_eq!(blocked[0].against_fact, old);
+        assert_eq!(blocked[0].premises, vec![ceo]);
+        let steps = reasoning::blocked_proof(&pool, f.kb, *vid)
+            .await?
+            .expect("the ghost has a proof");
+        assert_eq!(steps.len(), 1);
+        assert_eq!(steps[0].fact_id, ceo);
+
         // 重跑幂等：还是那一行
         reasoning::run(&pool, f.kb).await?;
         assert_eq!(open_contradictions(&pool, &f).await?.len(), 1);

diff --git a/docs/decisions/0016-close-the-open-seams-before-cutting-new-ones.md b/docs/decisions/0016-close-the-open-seams-before-cutting-new-ones.md
@@ -1,6 +1,6 @@
 # 0016 · Close the open seams before cutting new ones
 
-- **Status**: in progress · the first schedule after v0.1.0 · A1, A2, A3 done · B1 done (#227) · B2a done (#238, [0017](0017-a-contradiction-points-upstream.md)), B2b planned · B3: the signature half done (#190 / #196), cross-pack signatures and range-aware direction done (#233), `disjointWith` into resolution still open · D2's blank-base problem worked around with builtin `metric` / `dimension` classes (#231), the pack itself still planned · the lakehouse engines landed ahead of D4 (#239, [0018](0018-the-lakehouse-is-one-protocol-away.md))
+- **Status**: in progress · the first schedule after v0.1.0 · A1, A2, A3 done · B1 done (#227) · B2 done (#238 / #243, [0017](0017-a-contradiction-points-upstream.md)) · B3: the signature half done (#190 / #196), cross-pack signatures and range-aware direction done (#233), `disjointWith` into resolution still open · D2's blank-base problem worked around with builtin `metric` / `dimension` classes (#231), the pack itself still planned · the lakehouse engines landed ahead of D4 (#239, [0018](0018-the-lakehouse-is-one-protocol-away.md))
 - **Written**: 2026-09-02 · condensed into English 2026-09-03
 - **Related**: written after checking [0001](0001-ontology-import-and-governance.md) through [0015](0015-recording-a-sentence-is-not-asserting-a-fact.md) against the code; every item below has its source in those fifteen records, whose 2026-09-02 revision notes are the check's product. This record only orders them and says why this order.
 
@@ -44,8 +44,8 @@ A4 README against code, both languages: promise only what has landed.
 
 **B · Finish the reasoning engine**, after A, parallel with C. B1 the R2 proof chain (done,
 #227; a chain, not a tree — see [0002](0002-reasoning-engine.md)). B2 the derived-vs-asserted
-contradiction signal, `axiom_violations` kind `derived_contradiction` (B2a done; B2b, visibility
-on graph and panel, planned — 0017). B3 `classify_type_drift` reads `entity_type_disjoint`
+contradiction signal, `axiom_violations` kind `derived_contradiction` (done: B2a engine and
+queue #238, B2b visibility on graph and panel #243 — 0017). B3 `classify_type_drift` reads `entity_type_disjoint`
 instead of the hard-coded list, today's behavior when nothing is declared (class kinship from the
 hierarchy landed first, #226). B4 R3 incremental
 maintenance, deferred until a full re-derivation of `ai-timeline-ends` exceeds a threshold