diff --git a/spec/Spec/System/FeishuConnection.lean b/spec/Spec/System/FeishuConnection.lean
index 0b2f1d6..06d82df 100644
--- a/spec/Spec/System/FeishuConnection.lean
+++ b/spec/Spec/System/FeishuConnection.lean
@@ -1,21 +1,32 @@
 import Spec.Prelude
 
 /-!
-# FeishuConnection —— 组织飞书应用绑定
+# Feishu —— 组织飞书应用绑定与用户飞书信息
 
-一个组织绑定一个飞书企业应用(1:1, `Option` 结构自带)。用户经此应用登录、调飞书 API。
-绑定是组织级的;用户通过所属组织隐含获得绑定作用域。
+组织绑定一个飞书企业应用(1:1, `Option` 自带)。用户经此应用登录、调飞书 API。
+绑定是组织级;用户通过所属组织隐含获得绑定作用域。
 -/
 
 namespace Spec.System
 
 variable (I : Identifiers)
 
-/-- 组织的飞书应用绑定(`PINNED`, 1:1)。一个组织至多绑一个飞书企业应用。 -/
+/-- 组织的飞书应用绑定(`PINNED`, 1:1)。 -/
 structure FeishuAppBinding where
   /-- 飞书企业应用 app_id(`OPEN` 表示)。 -/
   appId : I.FeishuAppId
-  /-- 飞书企业应用 app_secret 的信封引用(`PINNED`, ADR-0024;明文不入契约)。 -/
+  /-- app_secret 信封引用(`PINNED`, ADR-0024)。 -/
   appSecretEnvelope : I.FeishuAppSecretRef
 
+/-- 用户的飞书信息(`PINNED`)。User 上的可选绑定载荷。 -/
+structure FeishuProfile where
+  /-- 应用内身份(`OPEN`);调 API 的直接句柄,换应用即变。 -/
+  openId : I.FeishuOpenId
+  /-- 租户内身份(`OPEN`);换应用不变,比 open_id 稳定。 -/
+  userId : I.FeishuUserId
+  /-- 显示名(`OPEN`)。 -/
+  name : Option String
+  /-- 头像 URL(`OPEN`)。 -/
+  avatarUrl : Option String
+
 end Spec.System
diff --git a/spec/Spec/System/Hierarchy.lean b/spec/Spec/System/Hierarchy.lean
index c327a75..a48a89c 100644
--- a/spec/Spec/System/Hierarchy.lean
+++ b/spec/Spec/System/Hierarchy.lean
@@ -31,7 +31,7 @@ structure Organization where
   /-- 飞书应用绑定(`PINNED`, 可选;1:1,每 org 至多一个)。 -/
   feishu : Option (FeishuAppBinding I)
 
-/-- 用户(`PINNED`, 租户层独立实体)。必属一个组织。飞书身份是绑定,见 `Spec.System.User`。 -/
+/-- 用户(`PINNED`, 租户层独立实体)。必属一个组织。飞书绑定见 `FeishuConnection`。 -/
 structure User where
   /-- 用户标识(`OPEN` 表示;组织内唯一,不可改;登录用)。 -/
   id : I.UserId
diff --git a/spec/Spec/System/User.lean b/spec/Spec/System/User.lean
index fb6d603..bcba36a 100644
--- a/spec/Spec/System/User.lean
+++ b/spec/Spec/System/User.lean
@@ -1,25 +1,12 @@
 import Spec.Prelude
 
 /-!
-# User —— 飞书绑定
+# User —— 用户创建路径
+
+用户实体见 `Hierarchy.User`;飞书绑定见 `Spec.System.FeishuConnection`。
 
-飞书身份是用户的绑定(登录途径),不是用户本体。用户实体见 `Hierarchy.User`。
 用户创建当前只钉管理员直接创建;飞书自助注册→管理员审批未钉死(`OPEN`)。
 -/
 
 namespace Spec.System
-
-variable (I : Identifiers)
-
-/-- 飞书用户信息(`PINNED`)。User 上的可选飞书绑定载荷。 -/
-structure FeishuProfile where
-  /-- 应用内身份(`OPEN` 表示);调飞书 API 的直接句柄,换应用即变。 -/
-  openId : I.FeishuOpenId
-  /-- 租户内身份(`OPEN` 表示);换应用不变,比 open_id 稳定。 -/
-  userId : I.FeishuUserId
-  /-- 飞书显示名(`OPEN`)。 -/
-  name : Option String
-  /-- 飞书头像 URL(`OPEN`)。 -/
-  avatarUrl : Option String
-
 end Spec.System